A Verified Automatic Prover Based on Ordered Resolution
First-order theorem provers based on superposition, such as E, SPASS, and Vampire, play an important role in formal software verification. They are based on sophisticated logical calculi that combine ordered resolution and equality reasoning. They also employ advanced algorithms, data structures, and heuristics.
As a step towards verifying the correctness of state-of-the-art provers, we specify, using the Isabelle/HOL proof assistant, a purely functional ordered resolution prover and formally 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.
(See http://matryoshka.gforge.inria.fr/pubs/fun_rp_paper.pdf for details.)
Conference DayThu 22 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:40 - 17:20
|Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory|
|A Verified Automatic Prover Based on Ordered Resolution|
|Type Systems with Constraints for ML Type Inference with the Implementation in Haskell|
Alen ArslanagićUniversity of Groningen
|Improving pattern matching style|
Alejandro SerranoUtrecht University, Netherlands