2026-07-25T00:18:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24620 2025-12-12T15:10:02Z ddc:004 open_access

Formalizing Splitting in Isabelle/HOL Bergeron, Ghilain Krasnopol, Florent Tourret, Sophie Isabelle/HOL saturation-based calculi splitting We describe the 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. We focus here on the simplest splitting model and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ghilain Bergeron and Florent Krasnopol and Sophie Tourret 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.22 urn:nbn:de:0030-drops-246208 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.22 eng https://creativecommons.org/licenses/by/4.0/legalcode