Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, and Stephan Schulz. New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log., 10(1):4:1-4:51, 2009.
Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauß, and Klaus U. Schulz. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001.
Clark W. Barrett, Igor Shikanian, and Cesare Tinelli. An abstract decision procedure for a theory of inductive data types. Journal on Satisfiability, Boolean Modeling and Computation, 3(1-2):21-46, 2007.
Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB Standard: Version 2.0. In A. Gupta and D. Kroening, editors, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), 2010.
Maria Paola Bonacina and Mnacho Echenim. Rewrite-based satisfiability procedures for recursive data structures. Electron. Notes Theor. Comput. Sci., 174(8):55-70, 2007.
Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. Politeness and combination methods for theories with bridging functions. J. Autom. Reasoning, 64(1):97-134, 2020.
Raúl Gutiérrez and José Meseguer. Variant-based decidable satisfiability in initial algebras with predicates. In Fabio Fioravanti and John P. Gallagher, editors, Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers, volume 10855 of Lecture Notes in Computer Science, pages 306-322. Springer, 2017.
Hossein Hojjat and Philipp Rümmer. Deciding and interpolating algebraic data types by reduction. In Tudor Jebelean, Viorel Negru, Dana Petcu, Daniela Zaharie, Tetsuo Ida, and Stephen M. Watt, editors, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, September 21-24, 2017, pages 145-152. IEEE Computer Society, 2017.
Dejan Jovanovic and Clark W. Barrett. Polite theories revisited. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 402-416. Springer, 2010. Extended technical report is available at http://theory.stanford.edu/~barrett/pubs/JB10-TR.pdf.
Laura Kovács, Simon Robillard, and Andrei Voronkov. Coming to terms with quantified reasoning. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 260-270. ACM, 2017.
José Meseguer. Variant-based satisfiability in initial algebras. Sci. Comput. Program., 154:3-41, 2018.
Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1(2):245-257, 1979.
Silvio Ranise, Christophe Ringeissen, and Calogero G. Zarba. Combining data structures with nonstably infinite theories using many-sorted logic. In Bernhard Gramlich, editor, Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings, volume 3717 of Lecture Notes in Computer Science, pages 48-64. Springer, 2005. Extended technical report is available at https://hal.inria.fr/inria-00070335/.
Andrew Reynolds and Jasmin Christian Blanchette. A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reasoning, 58(3):341-362, 2017.
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark W. Barrett. Datatypes with shared selectors. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 591-608. Springer, 2018.
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark W. Barrett. Politeness for the theory of algebraic datatypes. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 238-255. Springer, 2020.
