Given Clause Loops (Q7361273)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Given_Clause_Loops
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Given Clause Loops |
AFP entry Given_Clause_Loops |
Statements
25 January 2023
0 references
Jasmin Christian Blanchette
0 references
Qi Qiu
0 references
Sophie Tourret
0 references
Given Clause Loops (English)
0 references
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.
0 references
