If you'd like to read more background material, here are some recommended texts and papers:

Blog Posts


"A proof procedure for the logic of Hereditary Harrop formulas", by Gopalan Nadathur. This paper covers the basics of universes, environments, and Lambda Prolog-style proof search. Quite readable.

"A new formulation of tabled resolution with delay", by Theresa Swift. This paper gives a kind of abstract treatment of the SLG formulation that is the basis for our on-demand solver.


  • "Introduction to Formal Logic", Peter Smith
  • "Handbook of Practical Logic and Automated Reasoning", John Harrison
  • "Types and Programming Languages", Benjamin C. Pierce
  • Programming with Higher-order Logic, by Dale Miller and Gopalan Nadathur, covers the key concepts of Lambda prolog. Although it's a slim little volume, it's the kind of book where you learn something new every time you open it.