A Comprehensive Framework for Saturation Theorem Proving

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2022-11, Vol.66 (4), p.499-539
Main Authors: Waldmann, Uwe, Tourret, Sophie, Robillard, Simon, Blanchette, Jasmin
Format: Article
Language:English
Subjects:
Artificial Intelligence
Automation
Calculi
Calculus
Completeness
Computer Science
Criteria
Logic in Computer Science
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Redundancy
Saturation
Symbolic and Algebraic Manipulation
Theorem proving
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
1573-0670
DOI:10.1007/s10817-022-09621-7