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 https://www.mat.ufrn.br/~LSFA2015/preproceedings.pdf.
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 https://www.mat.ufrn.br/~LSFA2015/preproceedings.pdf.
F. Baader & T. Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press,
doi:10.1017/CBO9781139172752.
M. Bezem, J.W. Klop & R. de Vrijer (2003):
Term Rewriting Systems by TeReSe.
Cambridge Tracts in Theoretical Computer Science 55.
Cambridge University Press.
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.
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.
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.
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.
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.
eptcs@eptcs.org