Extensions to the Comprehensive Framework for Saturation Theorem Proving

Title:	Extensions to the Comprehensive Framework for Saturation Theorem Proving
Authors:	Jasmin Blanchette and Sophie Tourret
Submission date:	2020-08-25
Abstract:	This Isabelle/HOL formalization extends the AFP entry Saturation_Framework with the following contributions: an application of the framework to prove Bachmair and Ganzinger's resolution prover RP refutationally complete, which was formalized in a more ad hoc fashion by Schlichtkrull et al. in the AFP entry Ordered_Resultion_Prover; generalizations of various basic concepts formalized by Schlichtkrull et al., which were needed to verify RP and could be useful to formalize other calculi, such as superposition; alternative proofs of fairness (and hence saturation and ultimately refutational completeness) for the given clause procedures GC and LGC, based on invariance.
BibTeX:	@article{Saturation_Framework_Extensions-AFP, author = {Jasmin Blanchette and Sophie Tourret}, title = {Extensions to the Comprehensive Framework for Saturation Theorem Proving}, journal = {Archive of Formal Proofs}, month = aug, year = 2020, note = {\url{http://isa-afp.org/entries/Saturation_Framework_Extensions.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	First_Order_Terms, Ordered_Resolution_Prover, Saturation_Framework, 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.