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
