A modular Isabelle framework for verifying saturation provers

Sophie Tourret; Jasmin Blanchette

doi:10.1145/3437992.3439912

A modular Isabelle framework for verifying saturation provers

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-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 language	English
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
Pages	224-237
Number of pages	14
ISBN (Electronic)	9781450382991
DOIs	https://doi.org/10.1145/3437992.3439912
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

Conference	10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021
Country/Territory	Denmark
City	Virtual, Online
Period	17/01/21 → 19/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

Access to Document

10.1145/3437992.3439912

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{96d23a1e70f1402ab0ad38f9bdd309ba,

title = "A modular Isabelle framework for verifying saturation provers",

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. ",

keywords = "Automatic theorem provers, First-order logic, Proof assistants",

author = "Sophie Tourret and Jasmin Blanchette",

note = "Funding Information: Blanchette{\textquoteright}s research has received funding from the European Research Council (ERC) under the European Union{\textquoteright}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: {\textcopyright} 2021 Owner/Author. Copyright: Copyright 2021 Elsevier B.V., All rights reserved.; 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 ; Conference date: 17-01-2021 Through 19-01-2021",

year = "2021",

month = jan,

doi = "10.1145/3437992.3439912",

language = "English",

pages = "224--237",

editor = "Catalin Hritcu and Andrei Popescu",

booktitle = "CPP 2021",

publisher = "Association for Computing Machinery, Inc",

}

Tourret, S & Blanchette, J 2021, A modular Isabelle framework for verifying saturation provers. in C Hritcu & A Popescu (eds), CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, Inc, pp. 224-237, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021, Virtual, Online, Denmark, 17/01/21. https://doi.org/10.1145/3437992.3439912

A modular Isabelle framework for verifying saturation provers. / Tourret, Sophie; Blanchette, Jasmin.
CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. ed. / Catalin Hritcu; Andrei Popescu. Association for Computing Machinery, Inc, 2021. p. 224-237.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A modular Isabelle framework for verifying saturation provers

AU - Tourret, Sophie

AU - Blanchette, Jasmin

N1 - 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.

PY - 2021/1

Y1 - 2021/1

N2 - 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.

AB - 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.

KW - Automatic theorem provers

KW - First-order logic

KW - Proof assistants

UR - http://www.scopus.com/inward/record.url?scp=85100523401&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85100523401&partnerID=8YFLogxK

U2 - 10.1145/3437992.3439912

DO - 10.1145/3437992.3439912

M3 - Conference contribution

AN - SCOPUS:85100523401

SP - 224

EP - 237

BT - CPP 2021

A2 - Hritcu, Catalin

A2 - Popescu, Andrei

PB - Association for Computing Machinery, Inc

T2 - 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021

Y2 - 17 January 2021 through 19 January 2021

ER -

A modular Isabelle framework for verifying saturation provers

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this