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

62 Downloads (Pure)


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
Number of pages19
ISBN (Electronic)9783030510749
ISBN (Print)9783030510732
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


Conference10th International Joint Conference on Automated Reasoning, IJCAR 2020
CityVirtual, Online


We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, Mathias Fleury and Christian Sternagel for their help with the Isabelle development, and 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 hasreceivedfundingfromtheNWOundertheVidiprogram(projectNo.016.Vidi.189.037, Lean Forward).

FundersFunder number
Horizon 2020 Framework Programme713999
European Research Council
Nederlandse Organisatie voor Wetenschappelijk Onderzoek


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

    Cite this