POPL 2021 (series) / CPP 2021 (series) / Certified Programs and Proofs /
A Modular Isabelle Framework for Verifying Saturation Provers
We present a formalization in Isabelle/HOL of a comprehensive framework for proving the completeness of automatic theorem provers based on resolution, superposition, or other saturation calculi. The framework helps calculus designers and prover developers derive, from the completeness of a calculus, the completeness of prover architectures implementing the calculus. It also helps derive the completeness of calculi obtained by lifting ground (i.e., variable-free) calculi. As a case study, we re-verified Bachmair and Ganzinger’s resolution prover RP to show the benefits of modularity.
Conference DayTue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:45 - 17:30 | Rewriting and Automated ReasoningCPP at CPP Chair(s): Cyril CohenUniversité Côte d’Azur, Inria, France Streamed session: https://youtu.be/TVqCuMMTuos?t=2806 | ||
16:45 15mTalk | A Modular Isabelle Framework for Verifying Saturation Provers CPP Pre-print Media Attached | ||
17:00 15mTalk | An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR CPP Pre-print Media Attached | ||
17:15 15mTalk | A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems CPP Alexander LochmannUniversity of Innsbruck, Aart MiddeldorpUniversity of Innsbruck, Fabian MitterwallnerUniversity of Innsbruck, Bertram Felgenhauer Pre-print Media Attached | ||