### Abstract

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.

### License

BSD License

### Topics

- Logic/General logic/Classical first-order logic

### 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. https://doi.org/10.1007/s10817-022-09621-7

### Session Given_Clause_Loops

- Given_Clause_Loops_Util
- More_Given_Clause_Architectures
- DISCOUNT_Loop
- Prover_Queue
- Fair_DISCOUNT_Loop
- Otter_Loop
- Fair_Otter_Loop_Def
- iProver_Loop
- Fair_iProver_Loop
- Fair_Otter_Loop_Complete
- Zipperposition_Loop
- Prover_Lazy_List_Queue
- Fair_Zipperposition_Loop
- Fair_Zipperposition_Loop_without_Ghosts
- Given_Clause_Loops

### Depends on

- A Comprehensive Framework for Saturation Theorem Proving
- A Formalization of Weighted Path Orders and Recursive Path Orders

## Cite

×

Given_Clause_Loops-AFP

    @article{Given_Clause_Loops-AFP,
      author  = {Jasmin Christian Blanchette and Qi Qiu and Sophie Tourret},
      title   = {Given Clause Loops},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Given_Clause_Loops.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Jan 31, 2023 : Isabelle2022