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
|09:00 - 10:00|
Jasmin Christian BlanchetteVrije Universiteit AmsterdamDOI
|10:00 - 10:30|
Anders SchlichtkrullTechnical University of Denmark, Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH ZurichDOI