
A
Comprehensive
Framework
for
Saturation
Theorem
Proving
Title: 
A Comprehensive Framework for Saturation Theorem Proving 
Author:

Sophie Tourret

Submission date: 
20200409 
Abstract: 
This Isabelle/HOL formalization is the companion of the technical
report “A comprehensive framework for saturation theorem proving”,
itself companion of the eponym IJCAR 2020 paper, written by Uwe
Waldmann, Sophie Tourret, Simon Robillard and Jasmin Blanchette. It
verifies a framework for formal refutational completeness proofs of
abstract provers that implement saturation calculi, such as ordered
resolution or superposition, and allows 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 using a variant of
the given clause loop. The technical report “A comprehensive
framework for saturation theorem proving” is available on
the Matryoshka website. The names of the Isabelle lemmas and
theorems corresponding to the results in the report are indicated in
the margin of the report. 
BibTeX: 
@article{Saturation_FrameworkAFP,
author = {Sophie Tourret},
title = {A Comprehensive Framework for Saturation Theorem Proving},
journal = {Archive of Formal Proofs},
month = apr,
year = 2020,
note = {\url{http://isaafp.org/entries/Saturation_Framework.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Lambda_Free_RPOs, Ordered_Resolution_Prover, Well_Quasi_Orders 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

