Skip to Main content Skip to Navigation
Conference papers

A modular Isabelle framework for verifying saturation provers

Sophie Tourret 1, 2, 3 Jasmin Blanchette 4, 1 
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Monday, October 4, 2021 - 12:58:31 PM
Last modification on : Monday, February 14, 2022 - 7:58:22 PM
Long-term archiving on: : Wednesday, January 5, 2022 - 6:30:16 PM


Files produced by the author(s)




Sophie Tourret, Jasmin Blanchette. A modular Isabelle framework for verifying saturation provers. CPP 2021 - 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2021, Virtual, Denmark. pp.224-237, ⟨10.1145/3437992.3439912⟩. ⟨hal-03364015⟩



Record views


Files downloads