A Comprehensive Framework for Saturation Theorem Proving
- 24 June 2020
- book chapter
- Published by Springer Nature
- Vol. 12166, 316-334
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 or Open image in new window loop. Our framework is mechanized in Isabelle/ Open image in new window .Keywords
This publication has 26 references indexed in Scilit:
- Labelled splittingAnnals of Mathematics and Artificial Intelligence, 2009
- Superposition with simplification as a decision procedure for the monadic class with equality2005
- The Next Waldmeister LoopLecture Notes in Computer Science, 2002
- Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)Journal of Symbolic Computation, 2002
- Combining Superposition, Sorts and Splitting2001
- Resolution Theorem Proving2001
- Theorem Proving with Ordering and Equality Constrained ClausesJournal of Symbolic Computation, 1995
- Rewrite-based Equational Theorem Proving with Selection and SimplificationJournal of Logic and Computation, 1994
- Refutational theorem proving for hierarchic first-order theoriesApplicable Algebra in Engineering, Communication and Computing, 1994
- On restrictions of ordered paramodulation with simplification1990