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.
|Title of host publication||CPP 2021|
|Subtitle of host publication||Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs|
|Editors||Catalin Hritcu, Andrei Popescu|
|Publisher||Association for Computing Machinery, Inc|
|Number of pages||14|
|Publication status||Published - Jan 2021|
|Event||10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 - Virtual, Online, Denmark|
Duration: 17 Jan 2021 → 19 Jan 2021
|Conference||10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021|
|Period||17/01/21 → 19/01/21|
Bibliographical noteFunding Information:
Blanchette’s research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). He has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).
© 2021 Owner/Author.
Copyright 2021 Elsevier B.V., All rights reserved.
- Automatic theorem provers
- First-order logic
- Proof assistants