Jürgen Avenhaus (2004):
Efficient Algorithms for Computing Modulo Permutation Theories.
In: David Basin & Michaël Rusinowitch: Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4–8.
Springer,
Berlin, Heidelberg,
pp. 415–429,
doi:10.1007/978-3-540-25984-8_31.
Jürgen Avenhaus & David A. Plaisted (2001):
General Algorithms for Permutations in Equational Inference.
Journal of Automated Reasoning 26(3),
pp. 223–268,
doi:10.1023/A:1006439522342.
Franz Baader & Deepak Kapur (2020):
Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols.
In: Nicolas Peltier & Viorica Sofronie-Stokkermans: Automated Reasoning.
Springer International Publishing,
Cham,
pp. 163–180,
doi:10.1007/978-3-030-51074-9_10.
Franz Baader & Tobias Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press,
Cambridge, UK,
doi:10.1017/CBO9781139172752.
Leo Bachmair (1991):
Canonical Equational Proofs.
Birkhäuser,
Boston,
doi:10.1007/978-1-4684-7118-2.
Leo Bachmair, IV Ramakrishnan, Ashish Tiwari & Laurent Vigneron (2000):
Congruence Closure Modulo Associativity and Commutativity.
In: Hélène Kirchner & Christophe Ringeissen: Frontiers of Combining Systems.
Springer,
Berlin, Heidelberg,
pp. 245–259,
doi:10.1007/10720084_16.
Leo Bachmair, Ashish Tiwari & Laurent Vigneron (2003):
Abstract congruence closure.
Journal of Automated Reasoning 31(2),
pp. 129–168,
doi:10.1023/B:JARS.0000009518.26415.49.
Clark Barrett & Cesare Tinelli (2018):
Satisfiability Modulo Theories,
pp. 305–343.
Springer International Publishing,
Cham,
doi:10.1007/978-3-319-10575-8_11.
David Cyrluk, Sreeranga Rajan, Natarajan Shankar & Mandayam K. Srivas (1995):
Effective theorem proving for hardware verification.
In: Ramayya Kumar & Thomas Kropf: Theorem Provers in Circuit Design.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 203–222,
doi:10.1007/3-540-59047-1_50.
Leonardo De Moura & Nikolaj Bjørner (2011):
Satisfiability modulo theories: introduction and applications.
Communications of the ACM 54(9),
pp. 69–77,
doi:10.1145/1995376.1995394.
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.
Peter J. Downey, Ravi Sethi & Robert Endre Tarjan (1980):
Variations on the Common Subexpression Problem.
J. ACM 27(4),
pp. 758771,
doi:10.1145/322217.322228.
Deepak Kapur (1997):
Shostak's Congruence Closure as Completion.
In: Hubert Comon: Rewriting Techniques and Applications.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 23–37,
doi:10.1007/3-540-62950-5_59.
Deepak Kapur (2019):
Conditional Congruence Closure over Uninterpreted and Interpreted Symbols.
Journal of Systems Science and Complexity 32,
pp. 317–355,
doi:10.1007/s11424-019-8377-8.
Deepak Kapur (2021):
A Modular Associative Commutative (AC) Congruence Closure Algorithm.
In: 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina (Virtual Conference), July 17–24 195.
LIPIcs,
pp. 15:1–15:21,
doi:10.4230/LIPIcs.FSCD.2021.15.
Dohan Kim & Christopher Lynch (2021):
An RPO-based ordering modulo permutation equations and its applications to rewrite systems.
In: 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina (Virtual Conference), July 17–24 195.
LIPIcs,
pp. 19:1–19:17,
doi:10.4230/LIPIcs.FSCD.2021.19.
Dexter Kozen (1977):
Complexity of Finitely Presented Algebras.
In: John E. Hopcroft, Emily P. Friedman & Michael A. Harrison: Proceedings of the 9th Annual ACM Symposium on Theory of Computing, May 4-6, 1977, Boulder, Colorado, USA.
ACM,
pp. 164–177,
doi:10.1145/800105.803406.
Greg Nelson & Derek C. Oppen (1980):
Fast Decision Procedures Based on Congruence Closure.
J. ACM 27(2),
pp. 356364,
doi:10.1145/322186.322198.
Vilhelm Sjöberg & Stephanie Weirich (2015):
Programming up to Congruence.
SIGPLAN Not. 50(1),
pp. 369382,
doi:10.1145/2676726.2676974.
eptcs@eptcs.org