1. W. Ackermann (1954): Solvable cases of the decision problem. Studies in logic and the foundations of mathematics. North-Holland Pub. Co..
  2. 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
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. John W. Lloyd (1987): Foundations of Logic Programming, 2nd Edition. Springer, doi:10.1007/978-3-642-83189-8.
  9. 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.
  10. M.J. Maher (1988): Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. Technical Report. IBM T.J. Watson Research Center.
  11. 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.
  12. 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.
  13. Derek C. Oppen (1980): Reasoning About Recursively Defined Data Structures. J. ACM 27(3), pp. 403–411, doi:10.1145/322203.322204.
  14. 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.
  15. 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.
  16. David Turner (1987): An overview of Miranda. Bulletin of the EATCS 33, pp. 103–114.
  17. 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.
  18. Fabian Zaiser (2020): Artifact for "The Extended Theory of Trees and Algebraic (Co)datatypes", doi:10.5281/zenodo.3828522.

Comments and questions to:
For website issues: