Abstract
The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.
Original language | English |
---|---|
Title of host publication | Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs |
Editors | Assia Mahboubi, Magnus O. Myreen |
Publisher | Association for Computing Machinery |
Publication date | 14 Jan 2019 |
Pages | 152-165 |
ISBN (Electronic) | 9781450362221 |
DOIs | |
Publication status | Published - 14 Jan 2019 |
Event | 8th ACM SIGPLAN International Conference on Certified Programs and Proofs - Cascais, Portugal Duration: 14 Jan 2019 → 15 Jan 2019 Conference number: 8 |
Conference
Conference | 8th ACM SIGPLAN International Conference on Certified Programs and Proofs |
---|---|
Number | 8 |
Country/Territory | Portugal |
City | Cascais |
Period | 14/01/2019 → 15/01/2019 |
Sponsor | Association for Computing Machinery |
Keywords
- Automatic theorem provers
- First-order logic
- Proof assistants
- Stepwise refinement