A modular isabelle framework for verifying saturation provers

Sophie Tourret, Jasmin Blanchette

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publicationCPP 2021
Subtitle of host publicationProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs
EditorsCatalin Hritcu, Andrei Popescu
PublisherAssociation for Computing Machinery, Inc
Pages224-237
Number of pages14
ISBN (Electronic)9781450382991
DOIs
Publication statusPublished - Jan 2021
Event10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 - Virtual, Online, Denmark
Duration: 17 Jan 202119 Jan 2021

Conference

Conference10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021
CountryDenmark
CityVirtual, Online
Period17/01/2119/01/21

Bibliographical note

Funding 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).

Publisher Copyright:
© 2021 Owner/Author.

Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.

Keywords

  • Automatic theorem provers
  • First-order logic
  • Proof assistants

Fingerprint Dive into the research topics of 'A modular isabelle framework for verifying saturation provers'. Together they form a unique fingerprint.

Cite this