Date: Thursday, October 16 2025 – 13h00
Place: A008
Title: Formalizing Splitting in Isabelle/HOL
In this talk, I will present a formalization in Isabelle/HOL of 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. This work focuse on the simplest splitting model and it provides an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR. This is joint work with two former interns, now PhD students in VeriDis: Ghilain Bergeron and Florent Krasnopol that was presented at ITP 2026.