**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

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

### License

### Topics

### Session Saturation_Framework_Extensions

- Soundness
- Standard_Redundancy_Criterion
- Clausal_Calculus
- FO_Ordered_Resolution_Prover_Revisited
- Given_Clause_Architectures_Revisited