1. 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.
  2. F. Baader & T. Nipkow (1998): Term Rewriting and All That. Cambridge University Press.
  3. M. Bezem, J.W. Klop & R. de Vrijer (2003): Term Rewriting Systems by TeReSe. Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press.
  4. 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
  5. A. Bove (1999): Martin-Löf Type Theory: Unification - A non-trivial Example. Chalmers University of Technology. Licentiate thesis.
  6. S. N. Burris (1998): Logic for Mathematics and Computer Science. Prentice Hall.
  7. 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.
  8. J. Corbin & M. Bidoit (1983): A Rehabilitation of Robinson's Unification Algorithm. In: IFIP Congress, pp. 909–914.
  9. H. D. Ebbinghaus, J. Flum & W. Thomas (1984): Mathematical Logic. Springer.
  10. 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.
  11. 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.
  12. 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.
  13. J.R. Hindley (1969): The principal type-scheme of an object in combinatory logic. Trans. American Mathematical Society 146, pp. 29–60.
  14. J.R. Hindley (1997): Basic Simple Type Theory. Cambridge Tracts in Theo. Computer Science 42. CUP.
  15. 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..
  16. 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.
  17. J. W. Lloyd (1987): Foundations of Logic Programming, second edition, Symbolic Computation – Artificial Intelligence. Springer.
  18. Lawrence C. Paulson (1985): Verifying the Unification Algorithm in LCF. Science of Computer Programming 5(2), pp. 143–169.
  19. 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.
  20. J. Rouyer (1992): Développement de l'Algorithme d'Unification dans le Calcul des Constructions. Technical Report 1795. INRIA.
  21. 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.

Comments and questions to:
For website issues: