A Modular Splitting Framework for Saturation Theorem Proving (Q7361910)
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 Splitting_Framework
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Modular Splitting Framework for Saturation Theorem Proving |
AFP entry Splitting_Framework |
Statements
18 June 2025
0 references
Ghilain Bergeron
0 references
Florent Krasnopol
0 references
Sophie Tourret
0 references
A Modular Splitting Framework for Saturation Theorem Proving (English)
0 references
We formalize in Isabelle/HOL a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model described in details in the first three sections of "Unifying Splitting" by Gabriel Ebner, Jasmin Blanchette and Sophie Tourret and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR. A paper describing the present formalization has been accepted at ITP'25.
0 references
