@inproceedings(AMARG2010,
author = "A. B. Avelar and F.L.C. de Moura and A. L. Galdino and M. Ayala-Rinc{\'o}n",
year = "2010",
title = "{Verification of the Completeness of Unification Algorithms {\`a} la Robinson}",
booktitle = "Proc. 17th Int. Workshop on Logic, Language, Information and Computation (WoLLIC)",
series = "LNCS",
volume = "6188",
publisher = "Springer",
pages = "110--124",
doi = "10.1007/978-3-642-13824-9\_10",
)
@book(BaNi98,
author = "F. Baader and T. Nipkow",
year = "1998",
title = "{Term Rewriting and {\em All That}}",
publisher = "Cambridge University Press",
)
@book(Te2003,
editor = "M. Bezem and J.W. Klop and R. de Vrijer",
year = "2003",
title = "{Term Rewriting Systems by TeReSe}",
series = "Cambridge Tracts in Theoretical Computer Science",
volume = "55",
publisher = "Cambridge University Press",
)
@unpublished(BlKo2011,
author = "F. Blanqui and A. Koprowski",
year = "2011",
title = "CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates",
note = "Available at {\tt http://color.inria.fr}",
)
@phdthesis(Bove1999,
author = "A. Bove",
year = "1999",
title = "Martin-L\"of Type Theory: Unification - A non-trivial Example",
school = "Chalmers University of Technology",
note = "Licentiate thesis",
)
@book(Bu98,
author = "S. N. Burris",
year = "1998",
title = "{Logic for Mathematics and Computer Science}",
publisher = "Prentice Hall",
)
@article(Constable09,
author = "R. Constable and W. Moczydlowski",
year = "2009",
title = "Extracting the resolution algorithm from a completeness proof for the propositional calculus",
journal = "Ann. of Pure and Appl. Logic",
volume = "161",
number = "3",
pages = "337--348",
doi = "10.1007/978-3-540-72734-7\_11",
)
@inproceedings(CoBi83,
author = "J. Corbin and M. Bidoit",
year = "1983",
title = "{A Rehabilitation of Robinson's Unification Algorithm}",
booktitle = "IFIP Congress",
pages = "909--914",
)
@book(EbFlTh84,
author = "H. D. Ebbinghaus and J. Flum and W. Thomas",
year = "1984",
title = "{Mathematical Logic}",
publisher = "Springer",
)
@article(GaAR2008c,
author = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
year = "2008",
title = "{A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language}",
journal = "Journal of Formalized Reasoning",
volume = "1",
number = "1",
pages = "39--50",
)
@inproceedings(GaAR2008b,
author = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
year = "2009",
title = "{A PVS \emph {Theory} for Term Rewriting Systems}",
booktitle = "Proceedings of the Third Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2008",
series = "Electronic Notes in Theoretical Computer Science",
volume = "247",
pages = "67--83",
doi = "10.1016/j.entcs.2009.07.049",
)
@article(GaAR2010,
author = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
year = "2010",
title = "{A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem}",
journal = "J. Auto. Reas.",
volume = "45",
number = "3",
pages = "301--325",
doi = "10.1007/s10817-010-9165-2",
)
@article(Hi69,
author = "J.R. Hindley",
year = "1969",
title = "{The principal type-scheme of an object in combinatory logic}",
journal = "Trans. American Mathematical Society",
volume = "146",
pages = "29--60",
)
@book(Hi97,
author = "J.R. Hindley",
year = "1997",
title = "{Basic Simple Type Theory}",
series = "Cambridge Tracts in Theo. Computer Science",
volume = "42",
publisher = "CUP",
)
@inbook(KnBe70,
author = "D. E. Knuth and P. B. Bendix",
year = "1970",
title = "{Computational Problems in Abstract Algebra}",
chapter = "Simple Words Problems in Universal Algebras",
pages = "263--297",
publisher = "J. Leech, ed. Pergamon Press, Oxford, U. K.",
)
@inproceedings(KoCa2009,
author = "S. Kothari and J. Caldwell",
year = "2009",
title = "{A Machine Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction}",
booktitle = "23th Int. Workshop on Unification UNIF2009",
pages = "17--31",
)
@book(Llo87,
author = "J. W. Lloyd",
year = "1987",
title = "{Foundations of Logic Programming}",
edition = "second",
series = "Symbolic Computation -- Artificial Intelligence",
publisher = "Springer",
)
@article(Pa1985,
author = "Lawrence C. Paulson",
year = "1985",
title = "{Verifying the Unification Algorithm in LCF}",
journal = "Science of Computer Programming",
volume = "5",
number = "2",
pages = "143--169",
)
@article(Ro65,
author = "J. A. Robinson",
year = "1965",
title = "{A Machine-oriented Logic Based on the Resolution Principle}",
journal = "Journal of the ACM",
volume = "12",
number = "1",
pages = "23--41",
doi = "10.1145/321250.321253",
)
@techreport(Rou1992,
author = "J. Rouyer",
year = "1992",
title = "D\'eveloppement de l'Algorithme d'Unification dans le Calcul des Constructions",
type = "Technical Report",
number = "1795",
institution = "INRIA",
)
@article(RRMMAH2006,
author = "J.-L. Ruiz-Reina and F.-J. Mart\'{\i }n-Mateos J.-A. Alonso and M.-J. Hidalgo",
year = "2006",
title = "{Formal Correctness of a Quadratic Unification Algorithm}",
journal = "J. of Auto. Reas.",
volume = "37",
number = "1-2",
pages = "67--92",
doi = "10.1007/s10817-006-9030-5",
)