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