# Extensions to the Comprehensive Framework for Saturation Theorem Proving

25 August 2020

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