Alessandro Armando, Silvio Ranise & Michael Rusinowitch (2003):
A rewriting approach to satisfiability procedures.
Information and Computation 183(2),
pp. 140 – 164,
doi:10.1016/S0890-5401(03)00020-8.
Franz Baader & Tobias Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press,
Cambridge, UK,
doi:10.1017/CBO9781139172752.
Leo Bachmair & Harald Ganzinger (1994):
Rewrite-based Equational Theorem Proving with Selection and Simplification.
J. Log. Comput. 4(3),
pp. 217–247,
doi:10.1093/logcom/4.3.217.
Leo Bachmair & Harald Ganzinger (1995):
Associative-commutative superposition.
In: Nachum Dershowitz & Naomi Lindenstrauss: Conditional and Typed Rewriting Systems.
Springer,
Berlin, Heidelberg,
pp. 1–14,
doi:10.1007/3-540-60381-6_1.
Leo Bachmair & Harald Ganzinger (1998):
Equational Reasoning in Saturation-Based Theorem Proving.
In: Wolfgang Bibel & Peter H. Schmitt: Automated Deduction. A basis for applications, chapter 11,
Volume I.
Kluwer,
Dordrecht, Netherlands,
pp. 353–397,
doi:10.1007/978-94-017-0437-3.
Clark Barrett, Roberto Sebastiani, Sanjit A Seshia & Cesare Tinelli (2009):
Satisfiability Modulo Theories.
In: Handbook of satisfiability,
Frontiers in Artificial Intelligence and Applications 185.
IOS Press,
pp. 825–885,
doi:10.3233/978-1-58603-929-5-825.
Ronald V. Book & Colm P. O'Dunlaing (1981):
Testing for the Church-Rosser property.
Theoretical Computer Science 16(2),
pp. 223–229,
doi:10.1145/321850.321862.
Ronald V. Book & Friedrich Otto (1993):
String-Rewriting Systems.
Springer,
New York, NY,
doi:10.1007/978-1-4613-9771-7.
Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest & Clifford Stein (2001):
Introduction to Algorithms,
second edition.
The MIT Press.
Robert Cremanns & Friedrich Otto (2002):
A Completion Procedure for Finitely Presented Groups That Is Based on Word Cycles.
J. Autom. Reason. 28(3),
pp. 235–256,
doi:10.1023/A:1015741511536.
Thomas Deiß (1992):
Conditional Semi-Thue systems for Presenting Monoids.
In: Annual Symposium on Theoretical Aspects of Computer Science, STACS 1992.
Springer, Berlin, Heidelberg,
pp. 557–565,
doi:10.1007/3-540-55210-3_212.
Nachum Dershowitz (1991):
Canonical sets of Horn clauses.
In: Javier Leach Albert, Burkhard Monien & Mario Rodríguez Artalejo: Automata, Languages and Programming.
Springer Berlin Heidelberg,
pp. 267–278,
doi:10.1007/3-540-54233-7_140.
Nachum Dershowitz & David A. Plaisted (2001):
Rewriting.
In: Handbook of Automated Reasoning, chapter 9,
Volume I.
Elsevier,
Amsterdam,
pp. 535 – 610,
doi:10.1016/b978-044450813-3/50011-4.
David B. A. Epstein, Mike Paterson, James W. Cannon, Derek F. Holt, Silvio V. F. Levy & William Thurston (1992):
Word Processing in Groups.
A. K. Peters, Ltd.,
Natick, MA,
doi:10.1201/9781439865699.
Qing Guo, Paliath Narendran & David A. Wolfram (1996):
Unification and matching modulo nilpotence.
In: Michael A. McRobbie & John K. Slaney: The 13th International Conference on Automated Deduction (CADE-13),
Lecture Notes in Computer Science 1104.
Springer,
Berlin, Heidelberg,
pp. 261–274,
doi:10.1007/3-540-61511-3_90.
Derek F. Holt, Bettina Eick & Eamonn A. O'Brien (2005):
Handbook of computational group theory.
CRC Press,
Boca Raton, FL,
doi:10.1201/9781420035216.
Deepak Kapur & Paliath Narendran (1985):
The Knuth-Bendix Completion Procedure and Thue Systems.
SIAM Journal on Computing 14(4),
pp. 1052–1072,
doi:10.1137/0214073.
Dohan Kim & Christopher Lynch (2021):
Equational Theorem Proving Modulo.
In: The 28th International Conference on Automated Deduction (CADE-28),
Lecture Notes in Computer Science 12699.
Springer,
pp. 166–182,
doi:10.1007/978-3-030-79876-5_10.
Temur Kutsia (2002):
Theorem Proving with Sequence Variables and Flexible Arity Symbols.
In: Matthias Baaz & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings,
Lecture Notes in Computer Science 2514.
Springer,
pp. 278–291,
doi:10.1007/3-540-36078-6_19.
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett & Morgan Deters (2016):
An Efficient SMT Solver for String Constraints.
Form. Methods Syst. Des. 48(3),
pp. 206–234,
doi:10.1007/s10703-016-0247-6.
Klaus Madlener, Paliath Narendran & Friedrich Otto (1991):
A Specialized Completion Procedure for Monadic String-Rewriting Systems Presenting Groups.
In: Javier Leach Albert, Burkhard Monien & Mario Rodríguez-Artalejo: Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings,
Lecture Notes in Computer Science 510.
Springer,
pp. 279–290,
doi:10.1007/3-540-54233-7_141.
Robert Nieuwenhuis & Albert Rubio (2001):
Paramodulation-based theorem proving.
In: Handbook of Automated Reasoning, chapter 7,
Volume I.
Elsevier,
Amsterdam,
pp. 371–443,
doi:10.1016/b978-044450813-3/50009-6.
Friedrich Otto, Masashi Katsura & Yuji Kobayashi (1997):
Cross-Sections for Finitely Presented Monoids with Decidable Word Problems.
In: Hubert Comon: Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings,
Lecture Notes in Computer Science 1232.
Springer,
pp. 53–67,
doi:10.1007/3-540-62950-5_61.
Giles Reger, Nikolaj Bjøner, Martin Suda & Andrei Voronkov (2016):
AVATAR Modulo Theories.
In: Christoph Benzmüller, Geoff Sutcliffe & Raul Rojas: GCAI 2016. 2nd Global Conference on Artificial Intelligence,
EPiC Series in Computing 41,
pp. 39–52,
doi:10.29007/k6tp.
José Carlos Rosales, Pedro A. García-Sánchez & Juan M. Urbano-Blanco (1999):
On Presentations of Commutative Monoids.
International Journal of Algebra and Computation 09(05),
pp. 539–553,
doi:10.1142/S0218196799000333.
Albert Rubio (1996):
Theorem Proving modulo Associativity.
In: Hans Kleine Büning: Computer Science Logic.
Springer,
Berlin, Heidelberg,
pp. 452–467,
doi:10.1007/3-540-61377-3_53.
eptcs@eptcs.org