Extensions to the Comprehensive Framework for Saturation Theorem Proving

Jasmin Christian Blanchette 🌐 and Sophie Tourret 🌐

August 25, 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.

License

BSD License

Topics

Session Saturation_Framework_Extensions

Depends on

Used by

Cite

× 
@article{Saturation_Framework_Extensions-AFP,
  author  = {Jasmin Christian Blanchette and Sophie Tourret},
  title   = {Extensions to the Comprehensive Framework for Saturation Theorem Proving},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Saturation_Framework_Extensions.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: