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
Fingerprint
Dive into the research topics of 'A verified prover based on ordered resolution'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver