Email Gateway (Jun 26 2025 at 13:29): Email Gateway (Jun 26 2025 at 13:29):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m getting even more happy by announcing another new AFP entry today:
A Modular Splitting Framework for Saturation Theorem Proving
by Ghilain Bergeron, Florent Krasnopol and Sophie Tourret
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.
https://www.isa-afp.org/entries/Splitting_Framework.html
Enjoy,
René
Last updated: Jul 02 2025 at 04:31 UTC