Extensions to the Comprehensive Framework for Saturation Theorem Proving (Q7361753)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Saturation_Framework_Extensions
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Extensions to the Comprehensive Framework for Saturation Theorem Proving |
AFP entry Saturation_Framework_Extensions |
Statements
25 August 2020
0 references
Jasmin Christian Blanchette
0 references
Sophie Tourret
0 references
Extensions to the Comprehensive Framework for Saturation Theorem Proving (English)
0 references
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.
0 references
