Reseña: A comprehensive framework for saturation theorem proving
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre lógica titulado A comprehensive framework for saturation theorem proving.
Sus autores son
- Uwe Waldmann (del grupo Automation of Logic en el Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Alemania),
- Sophie Tourret (del grupo Automation of Logic en el Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Alemania),
- Simon Robillard (del IMT Atlantique, Nantes, Francia)) y
- Jasmin Blanchette (del grupo Theoretical Computer Science en la Vrije Universiteit Amsterdam, Netherlands).
Su resumen es
One of the indispensable operations of realistic saturation theorem provers is (backward and forward) deletion of subsumed formu- las. In presentations of proof calculi, however, this is usually discussed only informally, and in the rare cases where there is a formal exposition, it is typically clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but using a standard notion of redundancy, a clause C does not make an instance Cσ redundant.
We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It permits us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of, e.g., an Otter or DISCOUNT loop prover implementing the calculus. Our framework is mechanized in Isabelle/HOL.
El trabajo es parte del proyecto Matryoshka (Fast interactive verification through strong higher-order automation)
El código está incluido en el repositorio IsaFoL (Isabelle Formalization of Logic).