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

32 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


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

Cite this