Building Theorem Provers

Citation

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. https://doi.org/10.1007/978-3-642-02959-2_24

Abstract

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.

Keywords

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

Read more from SRI