Email Gateway (Jan 31 2023 at 15:59): Email Gateway (Jan 31 2023 at 15:59):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new and substantial AFP entry, Given Clause Loops, by Jasmin Christian Blanchette, Qi Qiu and Sophie Tourret.
This Isabelle/HOL formalization extends the Saturation_Framework and Saturation_Framework_Extensions entries of the Archive of Formal Proofs with the specification and verification of four semiabstract given clause procedures, or "loops": the DISCOUNT, Otter, iProver, and Zipperposition loops. For each loop, (dynamic) refutational completeness is proved under the assumption that the underlying calculus is (statically) refutationally complete and that the used queue data structures are fair. The formalization is inspired by the proof sketches found in the article "A comprehensive framework for saturation theorem proving" by Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette (Journal of Automated Reasoning 66(4): 499-539, 2022). A paper titled "Verified given clause procedures" about the present formalization is in the works.
It is now on-line at https://www.isa-afp.org/entries/Given_Clause_Loops.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC