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 proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationAutomated Reasoning
Subtitle of host publication10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
EditorsNicolas Peltier, Viorica Sofronie-Stokkermans
PublisherSpringer
Pages316-334
Number of pages19
Volume1
ISBN (Electronic)9783030510749
ISBN (Print)9783030510732
DOIs
Publication statusPublished - 2020
Event10th International Joint Conference on Automated Reasoning, IJCAR 2020 - Virtual, Online
Duration: 1 Jul 20204 Jul 2020

Publication series

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

Conference

Conference10th International Joint Conference on Automated Reasoning, IJCAR 2020
CityVirtual, Online
Period1/07/204/07/20

Fingerprint Dive into the research topics of 'A Comprehensive Framework for Saturation Theorem Proving'. Together they form a unique fingerprint.

  • 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