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