Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a first-order resolution prover, an imperative SAT solver, and generalized term or- ders for λ-free higher-order logic.
Tue 15 JanDisplayed time zone: Belfast change
09:00 - 10:30
|Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
Jasmin Blanchette Vrije Universiteit AmsterdamDOI
|A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull Technical University of Denmark, Jasmin Blanchette Vrije Universiteit Amsterdam, Dmitriy Traytel ETH ZurichDOI