1. M. Ayala-Rincón, M. Fernández, M. J. Gabbay & A. C. Rocha Oliveira (2015): Checking Overlaps of Nominal Rewriting Rules. In: Pre-proc. LSFA, pp. 199–2014. Available at
  2. M. Ayala-Rincón, M. Fernández & A. C. Rocha Oliveira (2015): Completeness in PVS of a Nominal Unification Algorithm. In: Pre-proc. LSFA, pp. 19–34. Available at
  3. F. Baader & T. Nipkow (1998): Term Rewriting and All That. Cambridge University Press, doi:10.1017/CBO9781139172752.
  4. M. Bezem, J.W. Klop & R. de Vrijer (2003): Term Rewriting Systems by TeReSe. Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press.
  5. 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, doi:10.6092/issn.1972-5787/1347.
  6. A. L. Galdino & M. Ayala-Rincón (2010): A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. J. of Automated Reasoning 45(3), pp. 301–325, doi:10.1007/s10817-010-9165-2.
  7. G. Huet (1981): A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and Systems Sciences 23(1), pp. 11–21, doi:10.1016/0022-0000(81)90002-7.
  8. 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., doi:10.1016/B978-0-08-012975-4.50028-X.
  9. M. H. A. Newman (1942): On theories with a combinatorial definition of ``equivalence''. Ann. of Math. 43(2), pp. 223–243, doi:10.2307/1968867.
  10. A. C. Rocha Oliveira & M. Ayala-Rincón (2013): Formalizing the Confluence of Orthogonal Rewriting Systems. CoRR abs/1303.7335, doi:10.4204/EPTCS.113.14. Available at
  11. B. K. Rosen (1973): Tree-Manipulating Systems and Church-Rosser Theorems. J. of the ACM 20(1), pp. 160–187, doi:10.1145/321738.321750.

Comments and questions to:
For website issues: