@article(Armando2003,
 author       = {Alessandro Armando and Silvio Ranise and Michael Rusinowitch},
 year         = {2003},
 title        = {A rewriting approach to satisfiability procedures},
 journal      = {Information and Computation},
 volume       = {183},
 number       = {2},
 pages        = {140 -- 164},
 doi          = {10.1016/S0890-5401(03)00020-8},
)
@book(Baader1998,
 author       = {Franz Baader and Tobias Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 address      = {Cambridge, UK},
 doi          = {10.1017/CBO9781139172752},
)
@article(Bachmair1994,
 author       = {Leo Bachmair and Harald Ganzinger},
 year         = {1994},
 title        = {{Rewrite-based {E}quational {T}heorem {P}roving with {S}election and {S}implification}},
 journal      = {J. Log. Comput.},
 volume       = {4},
 number       = {3},
 pages        = {217--247},
 doi          = {10.1093/logcom/4.3.217},
)
@inproceedings(Bachmair1995,
 author       = {Leo Bachmair and Harald Ganzinger},
 year         = {1995},
 title        = {Associative-commutative superposition},
 editor       = {Nachum Dershowitz and Naomi Lindenstrauss},
 booktitle    = {Conditional and Typed Rewriting Systems},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {1--14},
 doi          = {10.1007/3-540-60381-6\_1},
)
@incollection(Bachmair1998,
 author       = {Leo Bachmair and Harald Ganzinger},
 year         = {1998},
 title        = {Equational {R}easoning in {S}aturation-{B}ased {T}heorem {P}roving},
 editor       = {Wolfgang Bibel and Peter H. Schmitt},
 booktitle    = {Automated Deduction. A basis for applications},
 chapter      = {11},
 series       = {Volume I},
 publisher    = {Kluwer},
 address      = {Dordrecht, Netherlands},
 pages        = {353–397},
 doi          = {10.1007/978-94-017-0437-3},
)
@incollection(Barrett2009,
 author       = {Clark Barrett and Roberto Sebastiani and Sanjit A Seshia and Cesare Tinelli},
 year         = {2009},
 title        = {Satisfiability {M}odulo {T}heories},
 booktitle    = {Handbook of satisfiability},
 series       = {Frontiers in Artificial Intelligence and Applications},
 volume       = {185},
 publisher    = {IOS Press},
 pages        = {825--885},
 doi          = {10.3233/978-1-58603-929-5-825},
)
@article(Book1981,
 author       = {Ronald V. Book and Colm P. O'Dunlaing},
 year         = {1981},
 title        = {Testing for the {C}hurch-{R}osser property},
 journal      = {Theoretical Computer Science},
 volume       = {16},
 number       = {2},
 pages        = {223--229},
 doi          = {10.1145/321850.321862},
)
@book(Book1993,
 author       = {Ronald V. Book and Friedrich Otto},
 year         = {1993},
 title        = {String-{R}ewriting {S}ystems},
 publisher    = {Springer},
 address      = {New York, NY},
 doi          = {10.1007/978-1-4613-9771-7},
)
@book(Cormen2001,
 author       = {Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and Clifford Stein},
 year         = {2001},
 title        = {Introduction to Algorithms},
 edition      = {second},
 publisher    = {The MIT Press},
)
@article(Cremanns2002,
 author       = {Robert Cremanns and Friedrich Otto},
 year         = {2002},
 title        = {A Completion {P}rocedure for Finitely Presented Groups That Is Based on Word Cycles},
 journal      = {J. Autom. Reason.},
 volume       = {28},
 number       = {3},
 pages        = {235--256},
 doi          = {10.1023/A:1015741511536},
)
@inproceedings(Deiss1992,
 author       = {Dei{\ss}, Thomas},
 year         = {1992},
 title        = {Conditional {S}emi-{T}hue {s}ystems for {P}resenting {M}onoids},
 booktitle    = {Annual Symposium on Theoretical Aspects of Computer Science, STACS 1992},
 publisher    = {Springer, Berlin, Heidelberg},
 pages        = {557--565},
 doi          = {10.1007/3-540-55210-3\_212},
)
@inproceedings(Dershowitz1991,
 author       = {Nachum Dershowitz},
 year         = {1991},
 title        = {Canonical sets of {H}orn clauses},
 editor       = {Javier Leach Albert and Burkhard Monien and Mario Rodr{\'i}guez Artalejo},
 booktitle    = {Automata, Languages and Programming},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {267--278},
 doi          = {10.1007/3-540-54233-7\_140},
)
@incollection(Dershowitz2001,
 author       = {Nachum Dershowitz and David A. Plaisted},
 year         = {2001},
 title        = {Rewriting},
 booktitle    = {Handbook of Automated Reasoning},
 chapter      = {9},
 series       = {Volume I},
 publisher    = {Elsevier},
 address      = {Amsterdam},
 pages        = {535 -- 610},
 doi          = {10.1016/b978-044450813-3/50011-4},
)
@book(Epstein1992,
 author       = {David B. A. Epstein and Mike Paterson and James W. Cannon and Derek F. Holt and Silvio V. F. Levy and William Thurston},
 year         = {1992},
 title        = {Word Processing in {G}roups},
 publisher    = {A. K. Peters, Ltd.},
 address      = {Natick, MA},
 doi          = {10.1201/9781439865699},
)
@inproceedings(Guo1996,
 author       = {Qing Guo and Paliath Narendran and David A. Wolfram},
 year         = {1996},
 title        = {Unification and matching modulo nilpotence},
 editor       = {Michael A. McRobbie and John K. Slaney},
 booktitle    = {The 13th International Conference on Automated Deduction (CADE-13)},
 series       = {Lecture Notes in Computer Science},
 volume       = {1104},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {261--274},
 doi          = {10.1007/3-540-61511-3\_90},
)
@book(Holt2005,
 author       = {Derek F. Holt and Bettina Eick and Eamonn A. O'Brien},
 year         = {2005},
 title        = {Handbook of computational group theory},
 publisher    = {CRC Press},
 address      = {Boca Raton, FL},
 doi          = {10.1201/9781420035216},
)
@article(Kapur1985,
 author       = {Deepak Kapur and Paliath Narendran},
 year         = {1985},
 title        = {The {K}nuth-{B}endix {C}ompletion {P}rocedure and {T}hue Systems},
 journal      = {SIAM Journal on Computing},
 volume       = {14},
 number       = {4},
 pages        = {1052--1072},
 doi          = {10.1137/0214073},
)
@inproceedings(Kim2021,
 author       = {Dohan Kim and Christopher Lynch},
 year         = {2021},
 title        = {Equational {T}heorem {P}roving {M}odulo},
 booktitle    = {The 28th International Conference on Automated Deduction (CADE-28)},
 series       = {Lecture Notes in Computer Science},
 volume       = {12699},
 publisher    = {Springer},
 pages        = {166--182},
 doi          = {10.1007/978-3-030-79876-5\_10},
)
@inproceedings(Kutsia2002,
 author       = {Temur Kutsia},
 year         = {2002},
 title        = {Theorem Proving with Sequence Variables and Flexible Arity Symbols},
 editor       = {Matthias Baaz and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, {LPAR} 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2514},
 publisher    = {Springer},
 pages        = {278--291},
 doi          = {10.1007/3-540-36078-6\_19},
)
@article(Liang2016,
 author       = {Tianyi Liang and Andrew Reynolds and Nestan Tsiskaridze and Cesare Tinelli and Clark Barrett and Morgan Deters},
 year         = {2016},
 title        = {An {E}fficient {SMT} {S}olver for {S}tring {C}onstraints},
 journal      = {Form. Methods Syst. Des.},
 volume       = {48},
 number       = {3},
 pages        = {206–234},
 doi          = {10.1007/s10703-016-0247-6},
)
@inproceedings(Madlener1991,
 author       = {Klaus Madlener and Paliath Narendran and Friedrich Otto},
 year         = {1991},
 title        = {A {S}pecialized {C}ompletion {P}rocedure for {M}onadic {S}tring-{R}ewriting {S}ystems {P}resenting {G}roups},
 editor       = {Javier Leach Albert and Burkhard Monien and Rodr{\'{\i}}guez{-}Artalejo, Mario},
 booktitle    = {Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {510},
 publisher    = {Springer},
 pages        = {279--290},
 doi          = {10.1007/3-540-54233-7\_141},
)
@incollection(Nieuwenhuis2001,
 author       = {Robert Nieuwenhuis and Albert Rubio},
 year         = {2001},
 title        = {Paramodulation-based theorem proving},
 booktitle    = {Handbook of Automated Reasoning},
 chapter      = {7},
 series       = {Volume I},
 publisher    = {Elsevier},
 address      = {Amsterdam},
 pages        = {371--443},
 doi          = {10.1016/b978-044450813-3/50009-6},
)
@inproceedings(Otto1997,
 author       = {Friedrich Otto and Masashi Katsura and Yuji Kobayashi},
 year         = {1997},
 title        = {Cross-Sections for Finitely Presented Monoids with Decidable Word Problems},
 editor       = {Hubert Comon},
 booktitle    = {Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1232},
 publisher    = {Springer},
 pages        = {53--67},
 doi          = {10.1007/3-540-62950-5\_61},
)
@inproceedings(Reger2016,
 author       = {Giles Reger and Bj{\o}ner, Nikolaj and Martin Suda and Andrei Voronkov},
 year         = {2016},
 title        = {AVATAR {M}odulo {T}heories},
 editor       = {Christoph Benzm{\"{u}}ller and Geoff Sutcliffe and Raul Rojas},
 booktitle    = {GCAI 2016. 2nd Global Conference on Artificial Intelligence},
 series       = {EPiC Series in Computing},
 volume       = {41},
 pages        = {39--52},
 doi          = {10.29007/k6tp},
)
@article(Rosales1999,
 author       = {Jos{\'{e}} Carlos Rosales and Garc{\'{\i}}a{-}S{\'{a}}nchez, Pedro A. and Urbano{-}Blanco, Juan M.},
 year         = {1999},
 title        = {On {P}resentations of {C}ommutative {M}onoids},
 journal      = {International Journal of Algebra and Computation},
 volume       = {09},
 number       = {05},
 pages        = {539--553},
 doi          = {10.1142/S0218196799000333},
)
@inproceedings(Rubio1996,
 author       = {Albert Rubio},
 year         = {1996},
 title        = {Theorem {P}roving modulo {A}ssociativity},
 editor       = {Hans Kleine B{\"{u}}ning},
 booktitle    = {Computer Science Logic},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {452--467},
 doi          = {10.1007/3-540-61377-3\_53},
)