A Comprehensive Framework for Saturation Theorem Proving

Uwe Waldmann; Sophie Tourret; Simon Robillard; Jasmin Blanchette

doi:10.1007/s10817-022-09621-7

A Comprehensive Framework for Saturation Theorem Proving

Uwe Waldmann^*, Sophie Tourret, Simon Robillard, Jasmin Blanchette

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance Cσ redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.

Original language	English
Pages (from-to)	499-539
Number of pages	41
Journal	Journal of Automated Reasoning
Volume	66
Issue number	4
Early online date	7 Jun 2022
DOIs	https://doi.org/10.1007/s10817-022-09621-7
Publication status	Published - Nov 2022

Bibliographical note

Funding Information:
We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem 50. We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

Funding Information:
We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem . We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

Publisher Copyright:
© 2022, The Author(s).

Funding

We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem 50. We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem . We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

Funders	Funder number
European Research Council
Mathias Fleury
Not added	016.Vidi.189.037, 016
Horizon 2020 Framework Programme	713999

Keywords

Automated theorem proving
Prover architectures
Redundancy
Resolution calculus
Saturation
Superposition calculus

Access to Document

10.1007/s10817-022-09621-7

Persistent URL (handle)

Persistent link

Cite this

@article{04fbca2ac66f4ceea1a1bca932a6ff60,

title = "A Comprehensive Framework for Saturation Theorem Proving",

abstract = "A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance Cσ redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.",

keywords = "Automated theorem proving, Prover architectures, Redundancy, Resolution calculus, Saturation, Superposition calculus",

author = "Uwe Waldmann and Sophie Tourret and Simon Robillard and Jasmin Blanchette",

note = "Funding Information: We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem 50. We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Funding Information: We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem . We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Publisher Copyright: {\textcopyright} 2022, The Author(s).",

year = "2022",

month = nov,

doi = "10.1007/s10817-022-09621-7",

language = "English",

volume = "66",

pages = "499--539",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "4",

}

TY - JOUR

T1 - A Comprehensive Framework for Saturation Theorem Proving

AU - Waldmann, Uwe

AU - Tourret, Sophie

AU - Robillard, Simon

AU - Blanchette, Jasmin

N1 - Funding Information: We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem 50. We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Funding Information: We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem . We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions. 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 also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Publisher Copyright: © 2022, The Author(s).

PY - 2022/11

Y1 - 2022/11

N2 - A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance Cσ redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.

AB - A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance Cσ redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.

KW - Automated theorem proving

KW - Prover architectures

KW - Redundancy

KW - Resolution calculus

KW - Saturation

KW - Superposition calculus

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

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

U2 - 10.1007/s10817-022-09621-7

DO - 10.1007/s10817-022-09621-7

M3 - Article

AN - SCOPUS:85131558134

SN - 0168-7433

VL - 66

SP - 499

EP - 539

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 4

ER -

A Comprehensive Framework for Saturation Theorem Proving

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this