POPL 2019 (series) / CPP 2019 (series) / CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 14-15 2019 /
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 ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract specification of a nondeterministic prover, 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.
Tue 15 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Tue 15 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 10:00 Talk | Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL CPP Jasmin BlanchetteVrije Universiteit Amsterdam DOI | ||
10:00 - 10:30 Research paper | A Verified Prover Based on Ordered Resolution CPP Anders SchlichtkrullTechnical University of Denmark, Jasmin BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich DOI |