Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 10:00 - 10:30 at Sala XII - Keynote 2 and Research Paper Chair(s): Assia Mahboubi

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

Displayed time zone: Belfast change

09:00 - 10:30
Keynote 2 and Research PaperCPP at Sala XII
Chair(s): Assia Mahboubi INRIA
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
Jasmin Blanchette Vrije Universiteit Amsterdam
Research paper
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull Technical University of Denmark, Jasmin Blanchette Vrije Universiteit Amsterdam, Dmitriy Traytel ETH Zurich