@inproceedings(Avenhaus2004,
 author       = {J{\"u}rgen Avenhaus},
 year         = {2004},
 title        = {Efficient {A}lgorithms for {C}omputing {M}odulo {P}ermutation {T}heories},
 editor       = {David Basin and Micha{\"e}l Rusinowitch},
 booktitle    = {Automated Reasoning - Second International Joint Conference, {IJCAR} 2004, Cork, Ireland, July 4--8},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {415--429},
 doi          = {10.1007/978-3-540-25984-8\_31},
)
@article(Avenhaus2001,
 author       = {J{\"u}rgen Avenhaus and David A. Plaisted},
 year         = {2001},
 title        = {General Algorithms for Permutations in Equational Inference},
 journal      = {Journal of Automated Reasoning},
 volume       = {26},
 number       = {3},
 pages        = {223--268},
 doi          = {10.1023/A:1006439522342},
)
@inproceedings(Baader2020,
 author       = {Franz Baader and Deepak Kapur},
 year         = {2020},
 title        = {Deciding the {W}ord {P}roblem for {G}round {I}dentities with {C}ommutative and {E}xtensional {S}ymbols},
 editor       = {Nicolas Peltier and Sofronie-Stokkermans, Viorica},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {163--180},
 doi          = {10.1007/978-3-030-51074-9\_10},
)
@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},
)
@book(Bachmair1991c,
 author       = {Leo Bachmair},
 year         = {1991},
 title        = {Canonical {E}quational {P}roofs},
 publisher    = {Birkh{\"a}user},
 address      = {Boston},
 doi          = {10.1007/978-1-4684-7118-2},
)
@inproceedings(Bachmair2000,
 author       = {Leo Bachmair and IV Ramakrishnan and Ashish Tiwari and Laurent Vigneron},
 year         = {2000},
 title        = {Congruence {C}losure {M}odulo {A}ssociativity and {C}ommutativity},
 editor       = {H{\'e}l{\`e}ne Kirchner and Christophe Ringeissen},
 booktitle    = {Frontiers of Combining Systems},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {245--259},
 doi          = {10.1007/10720084\_16},
)
@article(Tiwari2003,
 author       = {Leo Bachmair and Ashish Tiwari and Laurent Vigneron},
 year         = {2003},
 title        = {Abstract congruence closure},
 journal      = {Journal of Automated Reasoning},
 volume       = {31},
 number       = {2},
 pages        = {129--168},
 doi          = {10.1023/B:JARS.0000009518.26415.49},
)
@inbook(Barrett2018,
 author       = {Clark Barrett and Cesare Tinelli},
 year         = {2018},
 title        = {Satisfiability {M}odulo {T}heories},
 pages        = {305--343},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-10575-8\_11},
)
@inproceedings(Cyrluk1995,
 author       = {David Cyrluk and Sreeranga Rajan and Natarajan Shankar and Mandayam K. Srivas},
 year         = {1995},
 title        = {Effective theorem proving for hardware verification},
 editor       = {Ramayya Kumar and Thomas Kropf},
 booktitle    = {Theorem Provers in Circuit Design},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {203--222},
 doi          = {10.1007/3-540-59047-1\_50},
)
@article(Moura2011,
 author       = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 year         = {2011},
 title        = {Satisfiability modulo theories: introduction and applications},
 journal      = {Communications of the ACM},
 volume       = {54},
 number       = {9},
 pages        = {69--77},
 doi          = {10.1145/1995376.1995394},
)
@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},
)
@article(Downey1980,
 author       = {Peter J. Downey and Ravi Sethi and Robert Endre Tarjan},
 year         = {1980},
 title        = {Variations on the {C}ommon {S}ubexpression {P}roblem},
 journal      = {J. ACM},
 volume       = {27},
 number       = {4},
 pages        = {758\IeC{\textendash}771},
 doi          = {10.1145/322217.322228},
)
@book(Hungerford1980,
 author       = {Thomas W. Hungerford},
 year         = {1980},
 title        = {Algebra},
 publisher    = {Springer},
 address      = {New York, NY},
 doi          = {10.1007/978-1-4612-6101-8},
)
@inproceedings(Kapur1997,
 author       = {Deepak Kapur},
 year         = {1997},
 title        = {Shostak's {C}ongruence {C}losure as {C}ompletion},
 editor       = {Hubert Comon},
 booktitle    = {Rewriting Techniques and Applications},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {23--37},
 doi          = {10.1007/3-540-62950-5\_59},
)
@article(Kapur2019,
 author       = {Deepak Kapur},
 year         = {2019},
 title        = {{C}onditional {C}ongruence {C}losure over {U}ninterpreted and {I}nterpreted {S}ymbols},
 journal      = {Journal of Systems Science and Complexity},
 volume       = {32},
 pages        = {317--355},
 doi          = {10.1007/s11424-019-8377-8},
)
@inproceedings(Kapur2021,
 author       = {Deepak Kapur},
 year         = {2021},
 title        = {A {M}odular {A}ssociative {C}ommutative ({AC}) {C}ongruence {C}losure {A}lgorithm},
 booktitle    = {6th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2021, Buenos Aires, Argentina (Virtual Conference), July 17--24},
 volume       = {195},
 publisher    = {LIPIcs},
 pages        = {15:1--15:21},
 doi          = {10.4230/LIPIcs.FSCD.2021.15},
)
@inproceedings(Kim2021,
 author       = {Dohan Kim and Christopher Lynch},
 year         = {2021},
 title        = {An {RPO}-based ordering modulo permutation equations and its applications to rewrite systems},
 booktitle    = {6th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2021, Buenos Aires, Argentina (Virtual Conference), July 17--24},
 volume       = {195},
 publisher    = {LIPIcs},
 pages        = {19:1--19:17},
 doi          = {10.4230/LIPIcs.FSCD.2021.19},
)
@inproceedings(Kozen1977,
 author       = {Dexter Kozen},
 year         = {1977},
 title        = {Complexity of {F}initely {P}resented {A}lgebras},
 editor       = {John E. Hopcroft and Emily P. Friedman and Michael A. Harrison},
 booktitle    = {Proceedings of the 9th Annual {ACM} Symposium on Theory of Computing, May 4-6, 1977, Boulder, Colorado, {USA}},
 publisher    = {{ACM}},
 pages        = {164--177},
 doi          = {10.1145/800105.803406},
)
@article(Nelson1980,
 author       = {Greg Nelson and Derek C. Oppen},
 year         = {1980},
 title        = {Fast Decision Procedures Based on Congruence Closure},
 journal      = {J. ACM},
 volume       = {27},
 number       = {2},
 pages        = {356\IeC{\textendash}364},
 doi          = {10.1145/322186.322198},
)
@article(Sjoberg2015,
 author       = {Vilhelm Sj\"{o}berg and Stephanie Weirich},
 year         = {2015},
 title        = {Programming up to {C}ongruence},
 journal      = {SIGPLAN Not.},
 volume       = {50},
 number       = {1},
 pages        = {369\IeC{\textendash}382},
 doi          = {10.1145/2676726.2676974},
)