Given Clause Loops

Jasmin Christian Blanchette 📧, Qi Qiu 📧 and Sophie Tourret 📧

January 25, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Related publications

  • Waldmann, U., Tourret, S., Robillard, S., & Blanchette, J. (2022). A Comprehensive Framework for Saturation Theorem Proving. Journal of Automated Reasoning, 66(4), 499–539.

Session Given_Clause_Loops