A Verified Prover Based on Ordered Resolution

Anders Schlichtkrull (1) , Jasmin Christian Blanchette (2, 3, 4, 5) , Dmitriy Traytel (6)

1 DTU - Danmarks Tekniske Universitet = Technical University of Denmark
2 VU - Vrije Universiteit Amsterdam [Amsterdam]
3 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
5 MPII - Max-Planck-Institut für Informatik
6 ETH Zürich - Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich]

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 de-terministic 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.

Mots clés: proof assistants; first-order logic; stepwise refinement; automatic theorem provers

Domaines: Logique en informatique [cs.LO]

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel. A Verified Prover Based on Ordered Resolution. CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. ⟨10.1145/3293880.3294100⟩. ⟨hal-01937141⟩