A modular Isabelle framework for verifying saturation provers

Sophie Tourret (1, 2, 3) , Jasmin Blanchette (4, 1)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
2 Max Planck Institute for Informatics [Saarbrücken]
3 MOSEL - Proof-oriented development of computer-based systems
4 Computer Systems Section - Vrije Universiteit Amsterdam

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.

Mots clés: automatic theorem provers; proof assistants; first-order logic

Domaines: Logique en informatique [cs.LO]

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⟩