Conference paper
A verified prover based on ordered resolution
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.
Language: | English |
---|---|
Publisher: | Association for Computing Machinery |
Year: | 2019 |
Pages: | 152-165 |
Proceedings: | 8th ACM SIGPLAN International Conference on Certified Programs and Proofs |
Journal subtitle: | Proceedings of the 8th Acm Sigplan International Conference on Certified Programs and Proofs |
ISBN: | 1450362222 and 9781450362221 |
Types: | Conference paper |
DOI: | 10.1145/3293880.3294100 |
ORCIDs: | Schlichtkrull, Anders |