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

https://hal.inria.fr/hal-03364015
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

File

satur_isa_paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

25

Files downloads

24