@inproceedings(ARFeGaRO2015,
 author       = {Ayala-Rinc{\'o}n, M. and M. Fern\'{a}ndez and M. J. Gabbay and Rocha Oliveira, A. C.},
 year         = {2015},
 title        = {{Checking Overlaps of Nominal Rewriting Rules}},
 booktitle    = {Pre-proc. LSFA},
 pages        = {199--2014},
 url          = {https://www.mat.ufrn.br/~LSFA2015/preproceedings.pdf},
)
@inproceedings(ROFeAR2015,
 author       = {Ayala-Rinc{\'o}n, M. and M. Fern\'{a}ndez and Rocha Oliveira, A. C.},
 year         = {2015},
 title        = {{Completeness in PVS of a Nominal Unification Algorithm}},
 booktitle    = {Pre-proc. LSFA},
 pages        = {19--34},
 url          = {https://www.mat.ufrn.br/~LSFA2015/preproceedings.pdf},
)
@book(BaNi98,
 author       = {F. Baader and T. Nipkow},
 year         = {1998},
 title        = {{Term Rewriting and {\em All That}}},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139172752},
)
@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},
)
@article(GaAR2008c,
 author       = {A. L. Galdino and Ayala-Rinc{\'o}n, M.},
 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},
 doi          = {10.6092/issn.1972-5787/1347},
)
@article(GaAR2010,
 author       = {A. L. Galdino and Ayala-Rinc{\'o}n, M.},
 year         = {2010},
 title        = {{A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem}},
 journal      = {J. of Automated Reasoning},
 volume       = {45},
 number       = {3},
 pages        = {301--325},
 doi          = {10.1007/s10817-010-9165-2},
)
@article(Huet81,
 author       = {G. Huet},
 year         = {1981},
 title        = {{A complete proof of correctness of the Knuth-Bendix completion algorithm}},
 journal      = {Journal of Computer and Systems Sciences},
 volume       = {23},
 number       = {1},
 pages        = {11--21},
 doi          = {10.1016/0022-0000(81)90002-7},
)
@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.},
 doi          = {10.1016/B978-0-08-012975-4.50028-X},
)
@article(newman,
 author       = {M. H. A. Newman},
 year         = {1942},
 title        = {{On theories with a combinatorial definition of ``equivalence''}},
 journal      = {Ann. of Math.},
 volume       = {43(2)},
 pages        = {223--243},
 doi          = {10.2307/1968867},
)
@article(ROAR2013,
 author       = {Rocha Oliveira, A. C. and Ayala-Rinc{\'o}n, M.},
 year         = {2013},
 title        = {Formalizing the Confluence of Orthogonal Rewriting Systems},
 journal      = {CoRR},
 volume       = {abs/1303.7335},
 doi          = {10.4204/EPTCS.113.14},
 url          = {http://arxiv.org/abs/1303.7335},
)
@article(Ro1973,
 author       = {B. K. Rosen},
 year         = {1973},
 title        = {Tree-Manipulating Systems and Church-Rosser Theorems},
 journal      = {J. of the ACM},
 volume       = {20},
 number       = {1},
 pages        = {160--187},
 doi          = {10.1145/321738.321750},
)