A Comprehensive Framework for Saturation Theorem Proving

Uwe Waldmann; Sophie Tourret; Simon Robillard; Jasmin Blanchette

doi:10.1007/978-3-030-51074-9_18

A Comprehensive Framework for Saturation Theorem Proving

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

^*Corresponding author for this work

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

26 Downloads (Pure)

Abstract

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus, for instance within an Otter orloop. Our framework is mechanized in Isabelle/.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
Editors	Nicolas Peltier, Viorica Sofronie-Stokkermans
Publisher	Springer
Pages	316-334
Number of pages	19
Volume	1
ISBN (Electronic)	9783030510749
ISBN (Print)	9783030510732
DOIs	https://doi.org/10.1007/978-3-030-51074-9_18
Publication status	Published - 2020
Event	10th International Joint Conference on Automated Reasoning, IJCAR 2020 - Virtual, Online Duration: 1 Jul 2020 → 4 Jul 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12166 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Joint Conference on Automated Reasoning, IJCAR 2020
City	Virtual, Online
Period	1/07/20 → 4/07/20

Access to Document

10.1007/978-3-030-51074-9_18

Waldmann2020_Chapter_AComprehensiveFrameworkForSaturationFinal published version, 445 KBLicence: Article 25fa Dutch Copyright Act

Cite this

Waldmann, U., Tourret, S., Robillard, S., & Blanchette, J. (2020). A Comprehensive Framework for Saturation Theorem Proving. In N. Peltier, & V. Sofronie-Stokkermans (Eds.), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I (Vol. 1, pp. 316-334). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12166 LNAI). Springer. https://doi.org/10.1007/978-3-030-51074-9_18

Waldmann, Uwe ; Tourret, Sophie ; Robillard, Simon ; Blanchette, Jasmin. / A Comprehensive Framework for Saturation Theorem Proving. Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. editor / Nicolas Peltier ; Viorica Sofronie-Stokkermans. Vol. 1 Springer, 2020. pp. 316-334 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{f5d02447d88c41c2a049f4c14b00d590,

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

abstract = "We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus, for instance within an Otter orloop. Our framework is mechanized in Isabelle/.",

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

year = "2020",

doi = "10.1007/978-3-030-51074-9_18",

language = "English",

isbn = "9783030510732",

volume = "1",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "316--334",

editor = "Nicolas Peltier and Viorica Sofronie-Stokkermans",

booktitle = "Automated Reasoning",

note = "10th International Joint Conference on Automated Reasoning, IJCAR 2020 ; Conference date: 01-07-2020 Through 04-07-2020",

}

Waldmann, U, Tourret, S, Robillard, S & Blanchette, J 2020, A Comprehensive Framework for Saturation Theorem Proving. in N Peltier & V Sofronie-Stokkermans (eds), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. vol. 1, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12166 LNAI, Springer, pp. 316-334, 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Virtual, Online, 1/07/20. https://doi.org/10.1007/978-3-030-51074-9_18

A Comprehensive Framework for Saturation Theorem Proving. / Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin.

Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. ed. / Nicolas Peltier; Viorica Sofronie-Stokkermans. Vol. 1 Springer, 2020. p. 316-334 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12166 LNAI).

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

TY - GEN

T1 - A Comprehensive Framework for Saturation Theorem Proving

AU - Waldmann, Uwe

AU - Tourret, Sophie

AU - Robillard, Simon

AU - Blanchette, Jasmin

PY - 2020

Y1 - 2020

N2 - We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus, for instance within an Otter orloop. Our framework is mechanized in Isabelle/.

AB - We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus, for instance within an Otter orloop. Our framework is mechanized in Isabelle/.

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

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

U2 - 10.1007/978-3-030-51074-9_18

DO - 10.1007/978-3-030-51074-9_18

M3 - Conference contribution

AN - SCOPUS:85088256622

SN - 9783030510732

VL - 1

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 316

EP - 334

BT - Automated Reasoning

A2 - Peltier, Nicolas

A2 - Sofronie-Stokkermans, Viorica

PB - Springer

T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020

Y2 - 1 July 2020 through 4 July 2020

ER -

Waldmann U, Tourret S, Robillard S, Blanchette J. A Comprehensive Framework for Saturation Theorem Proving. In Peltier N, Sofronie-Stokkermans V, editors, Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. Vol. 1. Springer. 2020. p. 316-334. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-51074-9_18

A Comprehensive Framework for Saturation Theorem Proving

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this