W. Ackermann (1954):
Solvable cases of the decision problem.
Studies in logic and the foundations of mathematics.
North-Holland Pub. Co..
Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017):
The SMT-LIB Standard: Version 2.6.
Technical Report.
Department of Computer Science, The University of Iowa.
Available at http://www.smt-lib.org.
Clark Barrett, Igor Shikanian & Cesare Tinelli (2007):
An Abstract Decision Procedure for a Theory of Inductive Data Types.
Journal on Satisfiability, Boolean Modeling and Computation 3(12),
pp. 21–46,
doi:10.3233/SAT190028.
Hubert Comon & Pierre Lescanne (1989):
Equational Problems and Disunification.
J. Symb. Comput. 7(3/4),
pp. 371–425,
doi:10.1016/S0747-7171(89)80017-3.
Khalil Djelloul, Thi-Bich-Hanh Dao & Thom W. Frühwirth (2008):
Theory of finite or infinite trees revisited.
TPLP 8(4),
pp. 431–489,
doi:10.1017/S1471068407003171.
Jean-Pierre Jouannaud & Emmanuel Kounalis (1986):
Automatic Proofs by Induction in Equational Theories Without Constructors.
In: Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986,
pp. 358–366.
Daniel Kroening & Ofer Strichman (2016):
Decision Procedures – An Algorithmic Point of View, Second Edition.
Texts in Theoretical Computer Science. An EATCS Series.
Springer,
doi:10.1007/978-3-662-50497-0.
John W. Lloyd (1987):
Foundations of Logic Programming, 2nd Edition.
Springer,
doi:10.1007/978-3-642-83189-8.
Michael J. Maher (1988):
Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees.
In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988,
pp. 348–357,
doi:10.1109/LICS.1988.5132.
M.J. Maher (1988):
Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees.
Technical Report.
IBM T.J. Watson Research Center.
C.-H. Luke Ong & Dominik Wagner (2019):
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories.
In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019.
IEEE,
pp. 1–14,
doi:10.1109/LICS.2019.8785784.
Luke Ong (2015):
Higher-Order Model Checking: An Overview.
In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015,
pp. 1–15,
doi:10.1109/LICS.2015.9.
Derek C. Oppen (1980):
Reasoning About Recursively Defined Data Structures.
J. ACM 27(3),
pp. 403–411,
doi:10.1145/322203.322204.
Emil L. Post (1946):
A variant of a recursively unsolvable problem.
Bulletin of the American Mathematical Society 52(4),
pp. 264–269,
doi:10.1090/s0002-9904-1946-08555-9.
Andrew Reynolds & Jasmin Christian Blanchette (2017):
A Decision Procedure for (Co)datatypes in SMT Solvers.
J. Autom. Reasoning 58(3),
pp. 341–362,
doi:10.1007/s10817-016-9372-6.
David Turner (1987):
An overview of Miranda.
Bulletin of the EATCS 33,
pp. 103–114.
Sergei G. Vorobyov (1996):
An Improved Lower Bound for the Elementary Theories of Trees.
In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings,
pp. 275–287,
doi:10.1007/3-540-61511-3_91.
Fabian Zaiser (2020):
Artifact for "The Extended Theory of Trees and Algebraic (Co)datatypes",
doi:10.5281/zenodo.3828522.
eptcs@eptcs.org