A Modular Splitting Framework for Saturation Theorem Proving

Ghilain Bergeron, Florent Krasnopol and Sophie Tourret 📧

June 18, 2025

Abstract

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.

License

BSD License

Topics

Related publications

Session Splitting_Framework

Depends on

Cite

× 
@article{Splitting_Framework-AFP,
  author  = {Ghilain Bergeron and Florent Krasnopol and Sophie Tourret},
  title   = {A Modular Splitting Framework for Saturation Theorem Proving},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Splitting_Framework.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download