Building Theorem Provers


Stickel, M.E. (2009). Building Theorem Provers. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg.


This talk discusses some of the challenges of building a usable theorem prover. These include the chasm between theory and code, conflicting requirements, feature interaction, and competitive performance. The talk draws on the speaker’s experiences with devising extensions of resolution and building theorem provers that have been used as embedded reasoners in various systems.


  • Theorem Prover
  • Automate Reasoning
  • Model Elimination
  • Program Synthesis
  • Single Axiom

Read more from SRI