TY - GEN
T1 - A Comprehensive Framework for Saturation Theorem Proving
AU - Waldmann, Uwe
AU - Tourret, Sophie
AU - Robillard, Simon
AU - Blanchette, Jasmin
PY - 2020
Y1 - 2020
N2 - 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/.
AB - 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/.
UR - http://www.scopus.com/inward/record.url?scp=85088256622&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85088256622&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-51074-9_18
DO - 10.1007/978-3-030-51074-9_18
M3 - Conference contribution
AN - SCOPUS:85088256622
SN - 9783030510732
VL - 1
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 316
EP - 334
BT - Automated Reasoning
A2 - Peltier, Nicolas
A2 - Sofronie-Stokkermans, Viorica
PB - Springer
T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020
Y2 - 1 July 2020 through 4 July 2020
ER -