Email Gateway (Aug 23 2022 at 08:53): Email Gateway (Aug 23 2022 at 08:53):From: Tobias Nipkow <nipkow@in.tum.de>
A Comprehensive Framework for Saturation Theorem Proving
Sophie Tourret
This Isabelle/HOL formalization is the companion of the technical report “A
comprehensive framework for saturation theorem proving”, itself companion of the
eponym IJCAR 2020 paper, written by Uwe Waldmann, Sophie Tourret, Simon
Robillard and Jasmin Blanchette. It verifies a framework for formal refutational
completeness proofs of abstract provers that implement saturation calculi, such
as ordered resolution or superposition, and allows to model entire prover
architectures in such a way that the static refutational completeness of a
calculus immediately implies the dynamic refutational completeness of a prover
implementing the calculus using a variant of the given clause loop. The
technical report “A comprehensive framework for saturation theorem proving” is
available on the Matryoshka website. The names of the Isabelle lemmas and
theorems corresponding to the results in the report are indicated in the margin
of the report.
https://www.isa-afp.org/entries/Saturation_Framework.html
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC