# Formalizing Splitting in Isabelle/HOL

Ghilain Bergeron, Florent Krasnopol, Sophie Tourret

► To cite this version:

Ghilain Bergeron, Florent Krasnopol, Sophie Tourret. Formalizing Splitting in Isabelle/HOL. ITP 2025 - 16th International Conference on Interactive Theorem Proving, Sep 2025, Reykjavik, Iceland. 10.4230/LIPIcs.ITP.2025.22 . hal-05329260

HAL Id: hal-05329260

https://inria.hal.science/hal-05329260v1

Submitted on 24 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Formalizing Splitting in Isabelle/HOL

Ghilain Bergeron

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

Inria, Loria, CNRS, Lorraine Univ., Nancy, France

Florent Krasnopol

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

ENS Paris-Saclay, France

Sophie Tourret<fnref n="1" />

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

Inria, Loria, CNRS, Lorraine Univ., Nancy, France

Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany

## Abstract

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.

**2012 ACM Subject Classification** Computing methodologies → Theorem proving algorithms

**Keywords and phrases** Isabelle/HOL, saturation-based calculi, splitting

**Digital Object Identifier** 10.4230/LIPIcs.ITP.2025.22

**Funding** Sophie Tourret: supported by the ANR project BLaSST (ANR-21-CE25-0010).

**Acknowledgements** Asta Halkjær From contributed the theory Lazy_List_Limsup to the framework. Jasmin Blanchette and the anonymous reviewers suggested many improvements to the text. We thank them all.

## 1 Introduction

Saturation-based calculi, such as resolution, are implemented in theorem provers to establish the satisfiability of sets of formulas in various logics. For example, consider the first-order set of formulas $\{P(x) \lor Q(y, b), \neg P(a), \neg Q(z, z)\}$ where $x$, $y$ and $z$ are implicitly universally quantified. Resolution can prove this set of formulas unsatisfiable in two steps: first derive $Q(y, b)$ from $\neg P(a)$ and $P(x) \lor Q(y, b)$ by unifying $x$ with $a$ and resolving on $P(a)$; then derive $\perp$ from $Q(y, b)$ and $\neg Q(z, z)$ by unifying $y$ and $z$ with $b$ and resolving on $Q(b, b)$. Since the pivots of the resolutions, resp. $P(a)$ and $Q(b, b)$, and the variables involved, resp. $x$ and $\{y, z\}$, have nothing to do with each other, these inferences should also have nothing to do with each other. However, the output of the first inference is used as input in the second inference. Thus, there is a dependency in the proof. The order of the inferences can be swapped, but this just reverses the dependency. In the general case, the order in which inferences are done can have a major impact on the performance of the prover.

Splitting is a technique that lets calculi, and thus provers, draw such inferences without interfering with each other. As the name indicates, its main action is to split formulas in independent pieces. This introduces a form of branching in these otherwise monolithic calculi. In our example, $P(x) \lor Q(y, b)$ can be split as $P(x)$ in one branch and $Q(y, b)$ in the other. The unsatisfiability of the formula is then established by closing the two branches independently. In practice, this is achieved by annotating each part of the split clause with a fresh propositional variable. In our example $P(x) \lor p$ and $Q(y, b) \lor q$ are produced. A

<figure><img src="image_8.png" /></figure>

© Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret; licensed under Creative Commons License CC-BY 4.0

16th International Conference on Interactive Theorem Proving (ITP 2025).

Editors: Yannick Forster and Chantal Keller; Article No. 22; pp. 22:1–22:19

<figure><img src="image_9.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

<footnote n="1">¹ corresponding author</footnote>
22:2 Formalizing Splitting in Isabelle/HOL

propositional clause must be added to preserve the satisfiability of the formula, as $\neg p \lor \neg q$
in our case. Closing the branches in any order derives $p$ and $q$ and together with $\neg p \lor \neg q$,
this raises a contradiction.

Around ten years ago, Voronkov introduced the AVATAR splitting technique [20] that drastically increased the efficiency of saturation-based theorem provers. However, this technique came without the usual theoretical guarantee of completeness, which ensures that all unsatisfiable sets of formulas will be found unsatisfiable by the technique in a finite amount of time. More than five years later, Ebner, Blanchette and Tourret introduced a theoretical framework providing conditions under which AVATAR is provably complete [7]. This framework is intended to be as general as possible and work in both first- and higher-order logic, for various saturation-based calculi. It was strongly inspired by a previous framework by Waldmann, Tourret, Robillard and Blanchette [22] for saturation-based calculi, to lift calculi to more expressive logics (e.g., to add universally quantified variables or, as here, to add annotations to formulas) while preserving completeness. This earlier framework is versatile. It keeps logic and calculus fully abstract and offers many options to adapt to as many existing calculi as possible. However, it does not cover splitting.

We will refer to the work by Ebner, Blanchette and Tourret [7] as "Unifying Splitting" while the Isabelle/HOL formalization described here will be referred to as the *splitting framework*. The framework by Waldmann et al., also of use here, in particular its Isabelle/HOL formalization [19], will be referred to as the *saturation framework*. Our splitting framework formalizes Sec. 2 and 3 of "Unifying Splitting". It is able to model in a modular way some forms of splitting that preceded AVATAR. The splitting framework is available in the *Archive of Formal Proofs*<fnref n="2" /> (AFP) [3], the main repository of the Isabelle/HOL community. This work is also part of the IsaFoL effort<fnref n="3" />, that hosts various Isabelle/HOL formalizations related to automated reasoning. The Isabelle theory files `Disjunctive_Consequence_Relations.thy` and `Calculi_And_Annotations.thy` cover Sec. 2 of "Unifying Splitting", while the file `Modular_Splitting_Calculus.thy` covers Sec. 3. In addition, the file `Lightweight_Avatar.thy` provides an instance of the resolution calculus extended to splitting along the lines of Sec. 7.1. These are our central contributions. In the current paper, Sec. 2 introduces preliminary notions, including disjunctive consequence relations, calculi and annotations. Section 3 presents the core of the splitting calculus, which is shown to preserve completeness, while Sec. 4 introduces optional rules modularly. These rules are not necessary for completeness but are useful in practice. Splitting is among them. Section 5 presents a concrete instance of the framework that extends ordered resolution to a variant of splitting called Lightweight AVATAR.

2 Design of the Preliminary Notions

Section 2 of “Unifying Splitting” introduces abstract notions of formulas, consequence relations, calculi and annotations over formulas. It proposes annotated notions of consequence relation and calculi by extending non-annotated ones. In this section, we present our Isabelle/HOL equivalents of these notions and salient associated results.

<footnote n="2">² https://www.isa-afp.org/</footnote>

<footnote n="3">³ https://github.com/IsaFoL/IsaFoL</footnote>
## 2.1 Disjunctive Consequence Relations

We start with plain formulas that are kept fully abstract as a type 'f. We go on to define a notion of disjunctive consequence relation as a locale. A locale is the Isabelle version of a context, fixing parameters and assumptions that can be used in the locale's body. The definitions and the results proved in the locale can only be accessed from the outside when the locale is instantiated, i.e., its parameters are provided and the associated assumptions discharged. It is possible to define a locale by combining and extending other locales with new parameters and assumptions. Locales can be used inside other locales by declaring sub locales or interpretations [2].

The locale `consequence_relation` introduces a consequence relation, denoted $|=$, as well as the falsehood, denoted $⊥$. Note that we take some liberties with the Isabelle/HOL syntax in the paper for the sake of readability.

locale consequence_relation =

fixes

$$⊥ ::= 'f$$

$$(|) ::= 'f set \Rightarrow 'f set \Rightarrow \mathbf{bool}$$

assumes

$$(D1) \text{ bot_entails_empty: } \{⊥\} \models \emptyset$$

$$(D2) \text{ entails_reflexive: } \{C\} \models \{C\}$$

$$(D3) \text{ entails_subsets: } M' \subseteq M \implies N' \subseteq N \implies M' \models N' \implies M \models N$$

$$(D4) \text{ entails_cut: } M \models N \cup \{C\} \implies M' \cup \{C\} \models N' \implies M \cup M' \models N \cup N'$$

$$(D5) \text{ entails_compactness: } M \models N \implies \exists M' N'. (M' \subseteq M \land N' \subseteq N \land \text{finite } M' \land \text{finite } N' \land M' \models N')$$

Notably our disjunctive notion has a cut property (D4) as well as compactness (D5) but it is not transitive. Intuitively, $M \models N$ should be understood as “M entails one of the formulas in N” instead of the usual “M entails all the formulas in N”. It is possible to define a conjunctive consequence relation $|=$n from $|=$ such that $M \models_n \{C\} \leftrightarrow M \models \{C\}$ in the following way: $M \models_n N \leftrightarrow \forall C \in N. M \models \{C\}$.

During the inception of the splitting framework, several versions of this locale were considered. The Isabelle formalization played a key role in detecting problematic assumptions to be removed, relaxed or strengthened. One such former assumption, called `entails_supsets`, became Lemma 5 in “Unifying Splitting”, and is Lemma 1 here.

► **Lemma 1** (*entails_supsets*). For *M* and *N* two sets of formulas,

$$(\forall M' N'. (M' \supseteq M \land N' \supseteq N \land M' \cup N' = \text{UNIV}) \rightarrow M' \models N') \implies M \models N$$

To prove Lemma 1, we relied on Zorn's lemma [23], which asserts the existence of a maximal element in a set if every totally ordered subset admits an upper bound. Fortunately, Zorn's lemma is readily available in Isabelle/HOL and can be used in the proof by considering the set $A = \{(M', N')\}$. $M' \subseteq M \land N' \subseteq N \land \neg M' \models N'$} \text{ and the relation } zorn_relation = \{(C_1, C_2) \in A \times A. C_1 \preceq_s C_2\} \text{ where } (M, N) \preceq_s (M', N') \text{ if and only if } M \subseteq M' \text{ and } N \subseteq N'$. However, proving the premises of Zorn's lemma is not trivial. The corresponding two lines of text in “Unifying Splitting” amount to around 500 lines of Isabelle proof to show that all subsets of *A* totally ordered with *zorn_relation* admit an upper bound.

This notion of consequence relation is further extended to *negated* formulas, defined inductively in “Unifying Splitting” as $F^\sim = F \cup \{\sim C \mid C \in F^\sim\}$ where *F* is the set of formulas. This could be modeled faithfully with an inductive definition, but this is unneeded since $\sim\sim C = C$ is enforced. Hence, we introduce instead the following simpler datatype:
datatype 'a sign = Pos 'a | Neg 'a

along with a function neg for negation:

$$ \text{neg} (\text{Pos } C) = \text{Neg } C \mid \text{neg} (\text{Neg } C) = \text{Pos } C $$

This choice lets us reuse the same abstract datatype for annotations in Sec. 2.3. This simplifies the proofs since they contain many conversions between signed formulas and annotations.

The extension of $|\models$ to $|\models_{\sim}$ on signed formulas (of type 'f sign set) is defined directly in the locale consequence_relation.

$$ M \models_{\sim} N \equiv \{C. \text{Pos } C \in M\} \cup \{C. \text{Neg } C \in N\} \models \{C. \text{Pos } C \in N\} \cup \{C. \text{Neg } C \in M\} $$

We prove that it is indeed a consequence relation.

► Lemma 2 (ext_cons_rel). consequence_relation (Pos $\perp$) ($|\models$)

## 2.2 Calculi

Calculi are axiomatized as a locale named calculus by combining two locales:

- an inference system, i.e., a set of inferences Inf, where an inference $l = Infer P C$ with

- premises prems_of $l = P$, a list of formulas, and

- a conclusion concl_of $l = C$, a formula;

- a disjunctive consequence relation as described in the previous section;

adding as two arguments a redundancy criterion, i.e., a pair of functions (*Red*<sub>*F*</sub>, *Red*<sub>*I*</sub>) where

- *Red*<sub>*F*</sub> *N* is the set of redundant formulas with respect to the set of formulas *N* and

- *Red*<sub>*I*</sub> *N* is the set of redundant inferences with respect to *N*.

Inferences are introduced in the Calculus theory from the saturation framework. We import that theory, so we can directly make use of the definition of inferences. The redundancy criterion must respect the following assumptions:

(R0) Red_I_to_Inf: Red_I N ⊆ Inf

(R1) Red_F_Bot: N $|\models$ {} $\Rightarrow$ N - Red_F N $|\models$ {}

(R2) Red_F_of_subset: N $\subseteq$ N' $\Rightarrow$ Red_F N $\subseteq$ Red_F N'

(R3) Red_I_of_subset: N $\subseteq$ N' $\Rightarrow$ Red_I N $\subseteq$ Red_I N'

(R3) Red_F_of_Red_F_subset: N' $\subseteq$ Red_F N $\Rightarrow$ Red_F N $\subseteq$ Red_F (N - N')

(R3) Red_I_of_Red_F_subset: N' $\subseteq$ Red_F N $\Rightarrow$ Red_I N $\subseteq$ Red_I (N - N')

(R4) Red_I_of_Inf_to_N: $l \in Inf \Rightarrow \text{concl\_of } l \in N \Rightarrow l \in Red_I N$

The numbering follows that of “Unifying Splitting”, except for (R0) which is only implicitly present in the definition of *Red*<sub>*I*</sub>. In the splitting framework, we must be explicit because we chose not to represent *Inf* as a type but as a set.

We axiomatize a sound calculus similarly as a locale sound_calculus by replacing the inference system with a sound inference system, i.e., an inference system that is equipped with an additional consequence relation $|\models_s$ that verifies the soundness assumption. It ensures that formulas derived using inferences are consequences of the input, so that a contradiction cannot be obtained from a satisfiable set of formulas.

$$ \text{sound: } l \in \text{Inf} \Rightarrow \text{set } (\text{prems\_of } l) \models_s \{\text{concl\_of } l\} $$

In simple cases, one relation can play the role of both the standard and the sound consequence relation, but this is not true in general. For example, theory superposition and constraint superposition both require two distinct relations to fit in this kind of framework [22].
A set of formulas $N$ is *saturated* when $Inf\_from N \subseteq Red_I N$, where $Inf\_from$ is the set of inferences in $Inf$ where all premises belong to $N$. Saturation lets us define static completeness, one of the two main properties of interest in this work. A calculus is called *statically complete* when *saturated* $N \Longrightarrow N \models \{\perp\} \Longrightarrow \perp \in N$. This property ensures that if there are only redundant inferences left to perform in $N$ then it is very easy to know if $N$ is unsatisfiable since then $\perp$ must belong to $N$.

Dynamic completeness, the second main property of interest, ensures the derivability of $\perp$ in unsatisfiable sets during a fair saturation process. To properly state this notion, we first need to define *derivations*, i.e., sequences of sets of formulas. In contrast to the saturation framework, “Unifying Splitting” considers only infinite sequences. There is no loss of generality since it is always possible to extend a finite sequence by repeating the last state, or stuttering, infinitely. Several Isabelle/HOL theories can model infinite sequences, e.g., lazy lists (*LList*), infinite lists (*Coinductive_list*), streams (*HOL-Library.Stream*). It is also possible to use a function from the naturals to sets of formulas, or define an abstract type. In the AFP, the saturation framework and the RP prover [16, 17] use the lazy list codatatype, which also allows finite sequences. These two AFP entries are used in the splitting framework. For their smooth integration we use lazy lists too, but only those of infinite length.

```c
typedef 'a infinite_llist = {l :: 'a llist. llength l = ∞}
```

Using sequences, we define *derivations*, i.e., sequences $Ns = (N_i)_{i \in \mathbb{N}}$ such that $N_i \succ N_{i+1}$ for any $i$, where $M \succ N \equiv (M - N \subseteq Red_F N)$. Note that $\succ$ is left generic, and that in particular any transformation that preserves soundness is allowed, not limited to the inferences of the calculus. $\succ$ does not enforce soundness itself because some useful transformations are not sound by default, like Skolemization. Only one ingredient is missing to state dynamic completeness: the notion of *fairness*. Intuitively, fairness ensures that all inferences in $Inf$ that can be performed at some point in the sequence are eventually performed or become redundant. “Unifying Splitting” introduces two such notions in Sec. 2, a *weak* and a *strong* fairness. Both can be used to ensure saturation in a derivation. However, only weak fairness is used subsequently in Sec. 3 so this is what we use too in the splitting framework. A calculus is *dynamically complete* when *is_derivation* ($\succ$) $Ns \Longrightarrow$ *fair Ns* $\Longrightarrow$ *llhd Ns* $\models \{\perp\}$ $\Longrightarrow$ $\exists i. \perp \in llnth Ns i$, where *llhd Ns* returns the first element of $Ns$ and *llnth Ns* its nth element. Both statically and dynamically complete calculi are introduced as locales extending a calculus with the corresponding property.

## 2.3 Annotations

To add splitting on top of a calculus, formulas are annotated – becoming **A**-formulas – to keep track of the branches created by the splits. To that aim we introduce an abstract but countable type 'v to represent propositional variables distinct from formulas. Annotations are finite sets of 'v sign elements. The overall type for annotated formulas is as follows:

```c
datatype ('f, 'v::countable) AF = Pair (F_of: 'f) (A_of: 'v sign fset)
```

This definition ensures the existence of functions $F_{of}$ and $A_{of}$ to access the formula and annotation, respectively. We abuse this notation by applying $F_{of}$ also to inferences on **A**-formulas, to strip them from all annotations. We write an **A**-formula $C$ as $(F_{of} C) \leftarrow (A_{of} C)$. For example, the bottom element of **A**-formulas, denoted $\perp_{AF}$, is $\perp \leftarrow \emptyset$. The splitting framework also relies on a notion of propositional interpretation on annotations. In “Unifying Splitting” a propositional interpretation is a set of annotations such that for
every variable $v$ of type '$v$, exactly one of $\text{Pos } v$ or $\text{Neg } v$ belongs to the interpretation. In Isabelle, we define propositional interpretations as a type '$v \ \text{total\_interpretation}$ to avoid repeating this property as a premise in all lemmas using this notion.

We lay the groundwork for annotating a calculus, identified as the *base calculus*, in the locale *calculus_with_annotated_consrel* by adding two parameters to the locale *sound_calculus*. These are the functions *fm1* :: '$v \Rightarrow f$' and *asn* :: '$f \text{ sign} \Rightarrow v \text{ sign set}$ that respectively turns an annotation to an equivalent formula and returns all signed annotations equivalent to a given signed formula. This equivalence is guaranteed by the first two assumptions of the locale, and a third one ensures that each formula has at least one equivalent annotation. The annotation of the two consequence relations $\models$ and $\models_s$ of a sound calculus leads to several complex proofs. It defines the *annotated consequence relations* $\models_{AF}$ and $\models_{sAF}$. A salient point in this part of the formalization is that we rely on the compactness of propositional logic to prove (D5) for $\models_{AF}$ and $\models_{sAF}$. The compactness of propositional logic states that all finite subsets of a satisfiable set of propositional formulas are also satisfiable. Rather than re-prove this result in our setting, we rely on an existing AFP entry on propositional proof systems [10, 11]. To do so we create translation functions for formulas and interpretations, to express propositional modelhood using notions provided by the proof system. We also define another notion of propositional modelhood without relying on the AFP entry. With it, a propositional interpretation $\mathcal{J}$ is a propositional model of a set of A-formulas $\mathcal{N}$, denoted $\mathcal{J} \models_p \mathcal{N}$, when $(\mathcal{N}_{\perp})_{\mathcal{J}} = \emptyset$. It relies on the splitting framework's projection mechanism, including the *enabled projection* $\mathcal{N}_{\mathcal{J}} = \{F_{\text{of }} C \mid C \in \mathcal{N} \wedge A_{\text{of }} C \subseteq \mathcal{J}\}$ that filters formulas in a set $\mathcal{N}$ depending on whether their annotation agrees with a given propositional interpretation $\mathcal{J}$, and the *propositional projection* $\mathcal{N}_{\perp} = \{C \in \mathcal{N} \mid F_{\text{of }} C = \perp\}$. The latter only keeps the *propositional clauses* in $\mathcal{N}$. Annotated formulas of the form $\perp \leftarrow \{a_i\}_{i \in 1..n}$ are called thus because any annotated formula $C \leftarrow \{a_i\}_{i \in 1..n}$ can be interpreted as $C \vee \bigvee_{i=1}^n \neg a_i$ and if $C = \perp$ then the remaining $\bigvee_{i=1}^n \neg a_i$ is a clause in propositional logic. A set of propositional clauses $\mathcal{N}_{\perp}$ without a propositional model is *propositionally unsatisfiable*, which is equivalent to $\mathcal{N}_{\perp} \models_{AF} \{\perp_{AF}\}$. We prove that the two notions of propositional modelhood are equivalent to bring the compactness result from the AFP over to our formalization.

### 3 Annotating a Calculus while Preserving Completeness

In this section, we present the backbone of the splitting framework: the annotation of a base calculus. The resulting annotated calculus does not include splitting, but it preserves the completeness of the base calculus through the annotation.

#### 3.1 Calculus

We start by defining a locale to annotate calculi, that extends the base calculus of Sec. 2.2 to A-formulas with extra assumptions. It contains all notions introduced in this section.

locale annotated_calculus =
calculus_with_annotated_consrel $\perp$ Inf ($\models$) ($\models_s$) Red<sub>I</sub> Red<sub>F</sub> fm1 asn
+ assumes
entails_nontrivial: $\neg \emptyset \models \emptyset$
reducedness: Inf_from UNIV (Red<sub>F</sub> N) $\subseteq$ Red<sub>I</sub> N
complete: $\perp \notin$ Red<sub>F</sub> N
all_red_to_\perp: C $\neq$ \perp $\Rightarrow$ C $\in$ Red<sub>F</sub> $\{\perp\}$
where Inf_from U V is all inferences with at least a premise in V and all premises in U ∪ V. Since our entailment is interpreted as disjunctive on the right-hand side, M |= ∅ is true if and only if M is propositionally unsatisfiable. Because ∅ is never propositionally unsatisfiable, we require that ∅ ̸|= ∅. We could also have required the same for the consequence relation |=<sub>s</sub>, as was done originally in “Unifying Splitting”, but this turned out not to be needed. Furthermore, we require that the set of inferences with at least a premise in Red<sub>F</sub> N is a subset of all inferences that are redundant with respect to N. We also require that ⊥ is never redundant with respect to any N. Otherwise, we would be able to remove ⊥ from N by redundancy deletion, which is erroneous. Finally, we require that any F-formula not equal to ⊥ is redundant with respect to ⊥.

3.1.1 Inference Rules

The mandatory inference rules to annotate base calculi are presented in Figure 1. BASE performs a single inference step of the base calculus while propagating all annotations from premises to conclusion, and UNSAT produces ⊥<sub>AF</sub> if a set of propositional clauses is unsatisfiable. In Isabelle/HOL, we follow the convention that X_pre and X_inf are abbreviations that denote respectively the preconditions of the inference rule X, and the inference rule X itself. For BASE and UNSAT this means the following, where L is a list of A-formulas, N is a set of A-formulas and D is an F-formula.

$$
\begin{align*}
\mathit{base\_pre} \mathcal{L} \ D &\equiv \mathit{Infer} \ (\mathit{map} \ \mathcal{F}_{\mathit{of}} \ \mathcal{L}) \ D \in \mathit{Inf} \\
\mathit{base\_inf} \mathcal{L} \ D &\equiv \mathit{Infer} \ \mathcal{L} \ (D \leftarrow \bigcup (\mathit{map} \ \mathcal{A}_{\mathit{of}} \ \mathcal{L})) \\
\mathit{unsat\_pre} \ \mathcal{N} &\equiv (\forall x \in \mathcal{N}. \ \mathcal{F}_{\mathit{of}} \ x = \bot) \ \wedge \ \mathcal{N}_{\bot} \models_{AF} \{\bot\} \ \wedge \ \mathcal{N} \neq \emptyset \\
\mathit{unsat\_inf} \ \mathcal{L} &\equiv \mathit{Infer} \ \mathcal{L} \ \bot_{AF}
\end{align*}
$$

SInf is the set of inferences corresponding to these rules, defined inductively as

$$
\begin{array}{l}
\mathit{base:} \ \mathit{base\_pre} \ \mathcal{M} \ D \implies \mathit{base\_inf} \ \mathcal{M} \ D \in \mathit{SInf} \\
\mathit{| unsat:} \ \mathit{unsat\_pre} \ (\mathit{set} \ \mathcal{M}) \implies \mathit{unsat\_inf} \ \mathcal{M} \in \mathit{SInf}
\end{array}
$$

This calculus is not able to branch since BASE only propagates annotations, but if branches exist beforehand and all of them are closed during a derivation, the precondition of UNSAT is triggered and the false formula is derived. With resolution in first-order logic as the base calculus – returning to the example that opened this paper – the annotated calculus can prove {P(x) ∨ Q(y, b), ¬P(a), ¬Q(z, z)} unsatisfiable just with BASE if all clauses have empty annotations. It can also derive false starting from {P(x) ← {p}, Q(y, b) ← {q}, ⊥ ← {¬p, ¬q}, ¬P(a), ¬Q(z, z)} by two BASE inferences producing ⊥ ← {p} and ⊥ ← {q} resp., followed by an UNSAT inference on the three propositional clauses. Note the independence of the two BASE inferences from each other.

We prove that our inference rules are sound (Th. 14 in “Unifying Splitting”).

► **Theorem 3** (*SInf\_sound\_wrt\_entails\_sound*). *ι ∈ SInf ⇒ prems ι |=<sub>SAF</sub> {concl ι}*

$(C_i \leftarrow A_i)_{i=1}^n \quad \text{BASE} \\ D \leftarrow A_1 \cup \dots \cup A_n$

■ if Infer [*C*₁, ..., *C*ₙ] *D* is an inference of
the base calculus

$(\bot \leftarrow A_i)_{i=1}^n \quad \text{UNSAT} \\ \bot_{AF}$

■ if $(\bot \leftarrow A_i)_{i=1}^n \models_{AF} \{\bot_{AF}\}$

<caption>Figure 1 Mandatory inference rules.</caption>
### 3.1.2 Redundancy Criterion

Like any calculus as defined in Sec. 2.2, the annotated calculus is equipped with a redundancy criterion: $(SRed_I, SRed_F)$. Here we show how it is defined from $(Red_I, Red_F)$.

$$SRed_F \mathcal{N} = \{C \leftarrow A \mid \forall \mathcal{J}. \mathcal{J} \supseteq A \rightarrow C \in Red_F (\mathcal{N}_{\mathcal{J}})\} \\ \cup \{C \leftarrow A \mid \exists C \in \mathcal{N}. F_{of} C = C \wedge A_{of} C \subset A\}$$

$$SRed_I \mathcal{N} = \{\text{base\_inf } \mathcal{M} \ C \mid \text{base\_pre } \mathcal{M} \ C \wedge \\ (\forall \mathcal{J}. \{\text{base\_inf } \mathcal{M} \ C\}_{\mathcal{J}} \subseteq Red_I (\mathcal{N}_{\mathcal{J}}))\} \\ \cup \{\text{unsat\_inf } \mathcal{M} \mid \text{unsat\_pre } \mathcal{M} \wedge \perp_{AF} \in \mathcal{N}\}$$

The redundancy criterion for A-formulas $SRed_F$ states that an A-formula $C \leftarrow A$ is redundant with respect to a set $\mathcal{N}$ either if $C$ is redundant with respect to the enabled projection $\mathcal{N}_{\mathcal{J}}$ for every $\mathcal{J}$ for which $C \leftarrow A$ is enabled (i.e., $A \subseteq \mathcal{J}$), or if there exists a formula $C \leftarrow B$ in $\mathcal{N}$ strictly more general than $C \leftarrow A$ (i.e., $B \subset A$).

The redundancy criterion $SRed_I$ reflects the inference rules that underlie $SInf$. An inference $\iota \in SRed_I$ is redundant with respect to a set of formulas $\mathcal{N}$ if its preconditions hold and either if $\iota$ is a BASE inference then $F_{of} \iota$ is redundant with respect to $\mathcal{N}_{\mathcal{J}}$ for every $\mathcal{J}$ in which all premises of $\iota$ are enabled, or if $\iota$ is an UNSAT inference then $\perp_{AF}$ is in $\mathcal{N}$.

To prove that $SRed$ is a redundancy criterion in Isabelle/HOL, we proceed in two steps. First we restrict $SInf$ and $SRed_I$ to BASE inferences only, defining $AInf$ and $ARed_I$ and we show that $ARed = (ARed_I, SRed_F)$ is a redundancy criterion. Second we show that $SRed$ as a whole is a redundancy criterion.

To prove that $ARed$ is a redundancy criterion, we use locales from the saturation framework. However, the *tiebreaker_lifting* locale from the saturation framework is too restrictive – as pointed out in “Unifying Splitting” [7, proof of Lemma 18]. One of the assumptions of this locale is not met in our case. Fortunately, this assumption is not needed to prove the properties of a redundancy criterion. Hence, we make a copy of the locale named *light_tiebreaker_lifting*, where we remove the unmet assumption along with the results that subsequently become invalid. This is one of the most technical parts of the framework. Several notions need to be defined to interpret the saturation framework’s locales to obtain an appropriate redundancy criterion, and then this criterion must be proved equivalent to $ARed$. Among other technicalities, the saturation framework needs a conjunctive consequence relation for the base calculus. We provide $\models \emptyset$, the one described in Sec. 2.1. The saturation framework defines an annotated consequence relation from it, and we show that it agrees with $\models_{AF}$ on singletons as the base relations do. Since (R1), the only property of a redundancy criterion to use the consequence relation, only has it occurring with a singleton on the right-hand side, we are able to transfer the equivalent of (R1) provided by the saturation framework to $\models_{AF}$.

Having proven that $ARed$ is a redundancy criterion for the inference system $AInf$, we then turn our attention to $SRed$ and $SInf$, and subsequently instantiate the locale *calculus*.

interpretation $S\_calculus: calculus \perp_{AF} SInf (\models_{AF}) SRed_I SRed_F$

## 3.2 Completeness

In what follows we show the completeness of $S\_calculus$. We first consider the usual notions of completeness and then we consider strengthened ones more suited to splitting calculi.
$$
\begin{align*}
\texttt{locally\_saturated} \quad \mathcal{N} &\equiv \perp_{AF} \in \mathcal{N} \lor (\exists \mathcal{J} . \mathcal{J} \models_p \mathcal{N} \land \text{\texttt{saturated}} (\mathcal{N}_{\mathcal{J}})) \\
\texttt{locally\_fair} \quad \mathcal{N}_s &\equiv (\exists i . \perp_{AF} \in (\texttt{llnth} i \ \mathcal{N}_s)) \lor \\
&\phantom{\equiv} (\exists \mathcal{J} . \mathcal{J} \models_p \mathcal{N}_{s\infty} \land \text{\texttt{Inf\_from}} ((\mathcal{N}_{s\infty})_{\mathcal{J}}) \subseteq (\bigcup i . \text{\texttt{Red}}_i ((\texttt{llnth} i \ \mathcal{N}_s)_{\mathcal{J}})))
\end{align*}
$$

Then we prove the results transferring completeness from base calculi to annotated calculi
(Th. 24 and 28 in “Unifying Splitting”):

► **Theorem 7** (*S_calculus_strong_statically_complete*).

assumes

$F_{\text{statically\_complete}}: \text{statically\_complete\_calculus} \perp \text{Inf} (\models) \text{Red}_I \text{Red}_F$

$\mathcal{N}_{\text{locally\_saturated}}: \text{locally\_saturated} \mathcal{N}$

$\mathcal{N}_{\text{entails\_bot}}: \mathcal{N} \models_{AF} \{\perp_{AF}\}$

shows $\perp_{AF} \in \mathcal{N}$

► **Theorem 8** (*S_calculus_strong_dynamically_complete*).

assumes

$F_{\text{statically\_complete}}: \text{statically\_complete\_calculus} \perp \text{Inf} (\models) \text{Red}_I \text{Red}_F$

$\mathcal{N}_{i\_is\_derivation}: is\_derivation (\triangleright) \mathcal{N}_s$

$\mathcal{N}_{i\_is\_locally\_fair}: locally\_fair \mathcal{N}_s$

$\mathcal{N}_{i0\_entails\_bot}: \mathcal{N}_{s_0} \models_{AF} \{\perp_{AF}\}$

shows $\exists i. \perp_{AF} \in \mathcal{N}_{s_i}$

4 Optional Rules

Two kinds of optional rules can be added to an annotated calculus: inferences and simplifications. Optional inference rules offer alternatives to produce new consequences from the known ones, including more possibilities to exploit the power of annotations than allowed by the mandatory rules. Simplification rules produce conclusions that make their premises redundant so that these can automatically be erased. Splitting belongs to the latter category.

4.1 A Modular Architecture for Optional Rules

A primary concern in this work is to keep the architecture of the splitting framework modular,
so that users can combine optional rules as needed for the calculus they want to model.
Adding optional rules in a modular way is a challenging task: these rules are defined at the
level of A-formulas and thus cannot be annotated like the rules of the base calculus, but
they still make use of notions introduced to annotate the base calculus. Defining them in
annotated_calculus is possible, but this weakens the modularity because combinations of
optional rules must then be handled on a case by case basis.

To reconcile these aspects, we create *AF_calculus*, a locale for sound calculi over **A**-formulas and we extend it with a set of simplifications and a set of optional inferences in a locale *AF_calculus_extend*.

locale AF_calculus = sound_calculus ⊥_{AF} SInf ::= AF ::= s_{AF} SRed_I SRed_F

locale AF_calculus_extend = AF_calculus ⊥_{AF} SInf ::= AF ::= s_{AF} SRed_I SRed_F

+ fixes

Simps :: ('f, 'v) AF simplification set

OptInfs :: ('f, 'v) AF inference set

assumes

infs\_sound: l \in OptInfs \Rightarrow set (prems\_of l) ::= s {concl\_of l}

simps\_sound: δ ∈ Simps \Rightarrow ∀C ∈ S\_to δ. S\_from δ ::= s {C}

simps\_simp: δ ∈ Simps \Rightarrow (S\_from δ - S\_to δ) ⊆ Red_F (S\_to δ)
Simplifications need their own datatype since they have a set of conclusions that replaces the premises instead of a single conclusion that is added to the premises. This lets them remove formulas in addition to adding them. It also explains why optional inferences and simplifications are kept in different sets in the locale `AF_calculus_extend`.

datatype 'f simplification = Simplify (S_from: 'f set) (S_to: 'f set)

Like inference rules, simplifications must only add consequences of their premises (S_from) to the set of formulas. Moreover, the removed formulas must be redundant with respect to the resulting set of formulas (S_to). This is guaranteed respectively by assumptions `simps` and `simps_simp` of locale `AF_calculus_extend`. The soundness of optional inferences is guaranteed by `infsoc` . Thanks to these assumptions, any simplification and optional inference rule can take part in the derivation without interfering with completeness, as stated in the following lemma.

► Lemma 9 (simp_in_derivations and opt_infs_in_derivations) .

$$
\delta \in \mathcal{S} \Rightarrow (\mathcal{N} \cup \mathcal{S}_{\text{from}} \delta) \triangleright (\mathcal{N} \cup \mathcal{S}_{\text{to}} \delta)
$$

$$
\iota \in \mathit{OptInfs} \Rightarrow
$$

$$
(\mathcal{N} \cup \mathcal{S} \text{set } (\text{prems\_of } \iota)) \triangleright (\mathcal{N} \cup \mathcal{S} \text{set } (\text{prems\_of } \iota) \cup \{\text{concl\_of } \iota\})
$$

The locale `AF_calculus_extend` ensures in particular that all extra rules are sound and that simplification rules really are simplifications. However, because this locale operates purely at the level of A-formulas like `AF_calculus`, it does not allow access to the base calculus and the functions `fm1` and `asn`. Hence, everything in the extra rules using these notions must be abstracted over.

Each extra rule, inference or simplification, is defined in a locale `AF_calculus_with_XYZ` where `XYZ` is the name of the rule. These locales are defined from `AF_calculus_extend` and are themselves (with `XYZ`) also instances of it, which is proved via the sublocale mechanism. Thus, all of them can be stacked in any order like paper cups. The abstracted parts of the definitions are specified in a locale `splitting_calculus` that extends the locale `annotated_calculus`. We add the following sublocale in `splitting_calculus`, defining an `AF_calculus` with empty simplifications and optional rules to serve as the foundation of all extensions:

sublocale empty_simps:

$$
AF\_calculus\_extended \perp_{AF} SInf (\models_{AF}) (\models_{sAF}) SRed_I SRed_F \emptyset \emptyset
$$

as well as a lemma of the following form for each extra rule `XYZ`:

► Lemma 10 (extend_OPT_with_XYZ) .

assumes

$$
AF\_calculus\_extended \perp_{AF} SInf (\models_{AF}) (\models_{sAF}) SRed_I SRed_F Simps OptInfs
$$

shows

$$
AF\_calculus\_with\_XYZ \perp_{AF} SInf (\models_{AF}) (\models_{sAF}) SRed_I SRed_F Simps' OptInfs' [OPT_PARAM]
$$

where `OPT` is either `infs` for optional inferences or `simps` for simplification rules. In the first case `Simps'` = `Simps` and `OptInfs'` = `OptInfs_with_XYZ` and in the second case `Simps'` = `Simps_with_XYZ` and `OptInfs'` = `OptInfs`. Furthermore `OPT_PARAM` is a predicate specific to the `XYZ` rule that may or may not be present.

Put together, these provide everything needed to easily obtain an interpretation – or a
sublocale – of the annotated calculus extended with any subset of extra rules.
<figure><img src="image_10.png" /><figcaption>Figure 2 Optional inference rules.</figcaption></figure>

## 4.2 Optional Inference Rules

The optional rules presented in “Unifying Splitting” are described in Figure 2. The inference rule TAUTO inserts A-formulas in the formula set, provided that the formula C and the annotation A correspond to each other such that C ← A is a tautology for the sound consequence relation. The inference rule APPROX approximates an F-formula by one of its associated assertions a ∈ A. Finally, the rule STRONGUNSAT is as UNSAT but uses $|=_{sAF}$ instead of $|=_{AF}$ in its precondition, deciding a form of sound propositional unsatisfiability. This is usually more expensive to decide than propositional unsatisfiability (and may even be undecidable) so it is rarely used in practice.

In “Unifying Splitting” the soundness of these rules is asserted in Th. 14 and the proof blends concerns relative to the base calculus and its annotation with concerns relative to the level of A-formulas. In Isabelle/HOL, we follow the architecture outlined in Sec. 4.1 that enforces a clear separation between these concerns. For example, the rule APPROX becomes the `AF_calculus_with_aprox` locale. It includes abbreviations following the same convention as in `annotated_calculus`:

$$ \begin{align*} \texttt{approx\_pre} \ a \ C &\equiv \texttt{approximates} \ a \ C \\ \texttt{approx\_inf} \ C \ a &\equiv \texttt{Infer} \ [C] \ (\texttt{Pair} \ \perp \ (\{\texttt{neg} \ a\} \cup (A\_of \ C))) \end{align*} $$

where the precondition $a \in \text{asn } C$ has been abstracted by the predicate `approximates`, the `OPT_PARAM` of this locale. The fact that `approximates` operates on the A-formula `C` rather than on an F-formula is compensated in the definition of `approximates`, defined in `splitting_calculus` as:

$$ \texttt{approximates} \ a \ C \equiv a \in \text{asn} \ (\texttt{Pos} \ (F\_of \ C)) $$

This is needed because an `AF_calculus` does not know about the `asn` function. In addition `AF_calculus_with_aprox` has an assumption to ensure that `approximates` behaves in a way that preserves soundness, i.e.,

$$ \texttt{approx\_sound:} \ \texttt{approximates} \ a \ C \implies \{C\} \models_{sAF} \{\texttt{Pair} \ (\perp) \ (\{\texttt{neg} \ a\} \cup (A\_of \ C))\} $$

Thus, after extending `OptInfs` into `OptInfs_with_aprox` in the following way:

$$ \begin{array}{l} \texttt{approx:} \ approx\_pre \ a \ C \implies approx\_inf \ C \ a \in OptInfs\_with\_approx \\ | \ from\_OptInfs: \ i \in OptInfs \implies i \in OptInfs\_with\_approx \end{array} $$

we verify the soundness of `APPROX` with the theorem:

**Theorem 11** (`OptInfs_with_aprox\_sound\_wrt\_entails\_sound`).

$i \in OptInfs\_with\_approx \implies \text{set} \ (\text{prems\_of} \ i) \models_{sAF} \{\text{concl\_of} \ i\}

We can now declare `AF_calculus_extended` as a sublocale of `AF_calculus_with_aprox` as wanted. In `splitting_calculus`, in addition to defining `approximates` as above, the lemma `approx\_sound` is stated and proved such that overall the proof of soundness of `APPROX` as presented in Th. 14 in “Unifying Splitting” is now complete although divided over two locales. This lets us prove the lemma `extend\_infs\_with\_approx` as explained at the end of Sec. 4.1.
$$ \begin{array}{c} C \leftarrow A \\ \hline \bot \leftarrow \{\neg a_1, \dots, \neg a_n\} \cup A \quad (C_i \leftarrow \{a_i\})_{i=1}^n \\ \hline \text{SPLIT} \\ \text{if } C \neq \bot; C \text{ is splittable into } C_1, \dots, C_n; \text{ and for each } i, a_i \in \text{asn } C_i \\ \text{if } \{\bot \leftarrow A_i\}_{i=1}^n \models_{AF} \{\bot \leftarrow A\}; \text{ and } C \neq \bot \quad \text{if } C \neq \bot; A \cap B = \emptyset; A \neq \emptyset; \text{ and } \{\bot \leftarrow A_i\}_{i=1}^n \cup \\ \phantom{\text{if } C \neq \bot; A \cap B = \emptyset; } \{\bot \leftarrow A\} \models_{sAF} \{\bot \leftarrow B\} \end{array} $$

$$ \frac{\frac{(\bot \leftarrow A_i)_{i=1}^n \quad C \leftarrow A}{(\bot \leftarrow A_i)_{i=1}^n} \quad \text{COLLECT}}{\text{TRIM}} $$

Figure 3 Optional simplification rules.

The constraints of both `STRONGUNSAT` and `TAUTO` can be expressed directly in locales extending `AF_calculus`. Neither rule needs a predicate `OPT_PARAM` or extra assumptions. Otherwise, their proofs follow the same scheme as described for `APPROX`. None of these proofs are involved, making the division almost effortless (~ 275 lines of Isabelle/HOL).

## 4.3 Splitting and Other Simplifications

The simplifications introduced in "Unifying Splitting" are presented in Figure 3. A formula $C$ is *splittable* into formulas $C_1, \dots, C_n$ if there are at least two formulas in the set — otherwise, splitting would serve no purpose — and if $C \models_s \{C_1, \dots, C_n\}$ and $C \in \text{Red}_F \{C_i\}$ for each $i$. Thus, the rule `SPLIT` performs a case analysis on $C$. The conclusion $\bot \leftarrow \{\neg a_1, \dots, \neg a_n\} \cup A$ expresses exhaustiveness of the cases and every other conclusion expresses one case. In our small resolution-based example, the `SPLIT` rule is what can turn $\{P(x) \lor Q(y, b), \neg P(a), \neg Q(z, z)\}$ into $\{P(x) \leftarrow \{p\}, Q(y, b) \leftarrow \{q\}, \bot \leftarrow \{\neg p, \neg q\}, \neg P(a), \neg Q(z, z)\}$. `COLLECT` is similar in behavior to a garbage collection mechanism, as it removes $A$-formulas whose assertion cannot be satisfied by any model of the propositional clauses in the set. `TRIM` simplifies the assertion set of a given formula by removing assertions that must be true anyway because they are entailed by propositional clauses in the set.

The preconditions of `COLLECT` and `TRIM` do not match those from "Unifying Splitting" as issues that led to minor corrections were detected during the formalization, but too late to be integrated into "Unifying Splitting". An addendum was made from our discoveries. It is available online.<fnref n="4" /> Briefly, the precondition of `COLLECT` in "Unifying Splitting" uses $\models_{sAF}$ rather than $\models_{AF}$. However, this prevents the derivation of a contradiction in the proof (by refutation) that `COLLECT` is a simplification. Similarly, to prove that `TRIM` is a simplification, we need the annotation of the conclusion to be a subset of the annotation of the right-most premise. Our version of `TRIM` guarantees this while preventing many obviously redundant inferences contrarily to the original one.

For `SPLIT`, we introduce *splittable* as the `OPT_PARAM` of `AF_calculus_with_split` and add the soundness and simplification properties of this rule as assumptions of the locale:

$$ \texttt{split\_sound1: splittable C Cs} \implies \{C\} \models_{sAF} \{\texttt{Pair} \perp A \cup \} $$

$$ \texttt{split\_sound2: splittable C Cs} \implies \forall C' \in \texttt{fset Cs}. \{C\} \models_{sAF} \{C'\} $$

$$ \texttt{split\_simp: splittable C Cs} \implies C \in \texttt{SRed}_F \{\texttt{Pair} \perp A \cup \} $$

<footnote n="4">⁴ https://matryoshka-project.github.io/#Publications</footnote>
22:14 Formalizing Splitting in Isabelle/HOL

where $A_\cup$, of type `fset` (for finite sets) in the Isabelle/HOL formalization, is defined as
$A_\cup = \bigcup_{C' \in C_s} \{\text{neg } a \mid a \in A_{\text{of } C'}\} \cup A_{\text{of } C}$. At this point, the conditions on `SPLIT` as
defined in Fig. 3 are not enforced since `splittable` is abstracted in the locale. The locale's
assumptions only ensure that `SPLIT` is sound and a simplification rule.

`AF_calculus_with_split` defines the abbreviations

- `split_pre`, abstracted by `splittable`,

- `split_res`, including all the formulas in `fset Cs` as well as `Pair ⊥ A_\cup`, and

- `split_simp`, such that `split_simp C Cs ≡ Simplify {C} (split_res C Cs)` to augment `Simps` with the `SPLIT` inferences:

```
split: split_pre C Cs =⇒ split_simp C Cs ∈ Simps_with_Split
| other: simp ∈ Simps =⇒ simp ∈ Simps_with_Split
```

We make use of the soundness and simplification assumptions above to show that soundness and simplification are preserved in `Simps_with_Split`, proving part of Th. 14 and 19 of "Unifying Splitting". Then we declare `AF_calculus_extended ⊥_AF SInf |=AF |=sAF OptInfs Simps_with_Split` as a sublocale. Returning to the context of `splitting_calculus` we give `splittable` a concrete definition. In a slight departure from "Unifying Splitting", we integrate the condition $C \neq \perp$ to the `splittable` predicate, while $a_i \in \text{asn } C_i$ for each $i$ is enforced by construction. Then, we prove that the assumptions of `AF_calculus_with_split` for soundness and simplification hold. Subsequently, we prove the lemma `extend_infs_with_split`.

The process is the same for the rules `COLLECT` and `TRIM` but with much simpler proofs. Thanks to the formalization, we discovered that the pen-and-paper proofs of soundness for `COLLECT` and `TRIM` in "Unifying Splitting" are slightly flawed. For `COLLECT`, there is in fact nothing to prove, as no formula is added to the formula set (the pen-and-paper proof for soundness had been misplaced in the completeness proof). For `TRIM`, the proof used notations that were not introduced, and skipped some steps which revealed a missing case. We repaired both proofs thanks to the formalization.

As a sanity check, we created a sequence of interpretations in `splitting_calculus`, as an illustration of how to use the `AF_calculus_with_XYZ` locales in conjunction with the `extend_OPT_with_XYZ` lemmas. It starts from empty sets of extra rules and adds all the ones presented in this section one after the other. The corresponding code is in the subsection *Combining all simplifications and optional inferences* in the theory *Modular_Splitting_Calculus*.

# 5 Lightweight AVATAR for Ordered Resolution

Results stated in Isabelle locales are only as trustworthy as the locale's assumptions. In-
stantiating a locale ensures these contain no inconsistencies. For this reason, we provide an
instance of the work above. It is a splitting calculus called Lightweight AVATAR, described
in Sec. 7.1 of "Unifying Splitting" and formalized in the theory `Lightweight_Avatar`. It
follows an implementation of splitting present in the Zipperposition theorem prover [21].
In "Unifying Splitting", this model is compared with a closely related splitting calculus by
Riazanov and Voronkov called "Splitting without Backtracking" [14].

## 5.1 Binary Splitting

Lightweight AVATAR operates in first-order logic on formulas in clausal normal form. It
extends the signature $\Sigma$ of the base calculus with a countable set of fresh nullary predicate
symbols $\mathbb{P}$ and adds as a simplification a binary split rule, that differs from the `SPLIT` rule
<figure><img src="image_11.png" /><figcaption>Figure 4 Binary splitting rule.</figcaption></figure>

of Sec. 4.3 in that clauses are always cut in two and the predicates from $\mathbb{P}$ are used in a slightly different way. This binary split rule can be handled exactly as the other optional simplification rules, independently of the first-order base calculus. It is defined in Figure 4. We can reuse the same criterion for splittability as in the SPLIT rule, but its Isabelle/HOL definition `bin_spittable` is different to account for the binary-only splitting and the changes in the conclusions of the rule. In our small resolution-based example, BINSPLIT turns $\{P(x) \lor Q(y, b), \neg P(a), \neg Q(z, z)\}$ into $\{P(x) \leftarrow \{p\}, Q(y, b) \leftarrow \{\neg p\}, \neg P(a), \neg Q(z, z)\}$, after which BASE inferences produce $\perp \leftarrow \{p\}$ and $\perp \leftarrow \{\neg p\}$ that can be used together by UNSAT to conclude the derivation. We create a locale `AF_calculus_with_binsplit`. The soundness and simplification proofs of BINSPLIT are divided between this locale and the locale `splitting_calculus` where the definition of `bin_spittable` can be found.

## 5.2 The Base Calculus

To instantiate the splitting framework with Lightweight AVATAR, we need a base calculus in first-order logic. While our sources of inspiration deal with the superposition calculus [12], we use the (simpler) ordered resolution calculus [1] available in a suitable form in the AFP.<fnref n="5" />

Among the ordered resolution calculi available in the AFP, we pick the one from the theory `FO_Ordered_Resolution_Prover_Revisited` by Blanchette and Tourret [4], itself using the theory `FO_Ordered_Resolution_Prover` by Schlichtkrull et al. [15, 18]. We denote this calculus $O$. Given a signature $\Sigma$ and a set $\mathbf{F}$ of $\Sigma$-clauses where $\perp$ denotes the empty clause, the calculus $O$ is the tuple $(\mathit{FInf}, \mathit{FRed}_I, \mathit{FRed}_F, \models^{\emptyset})$ such that:

- $\mathit{FInf}$ is the set of ordered resolution inferences on the set $\mathbf{F}$ of $\Sigma$-clauses,

- $(\mathit{FRed}_I, \mathit{FRed}_F)$ is the standard redundancy criterion [1, section 4.2.2], and

- $\models^{\emptyset}$ is the usual (conjunctive) Herbrand entailment.<fnref n="6" />

While the set of inferences of this calculus can be used as is, it takes more effort to obtain a redundancy criterion suitable for the splitting framework. Indeed, only *reduced* redundancy criteria, i.e., such that all inferences where a premise is redundant are themselves redundant, fit in the splitting framework. Fortunately, starting from any redundancy criteria, a reduced version can be defined in a systematic way while preserving the soundness and completeness of the calculus [22]. The saturation framework includes the necessary tools for this transformation [19]. Thus this issue is solved by replacing $\mathit{FRed}_I$ with the appropriate notion, which we denote here $\mathit{FRed}_I$.

Moreover, a disjunctive entailment verifying $(D1)-(D5)$ is needed to instantiate the splitting framework. Whereas it is trivial to go from disjunctive to conjunctive entailment, the reverse is more delicate, unlike what is claimed in Ex. 1 of “Unifying Splitting”. We use:

$$ M \models^\cup N \leftrightarrow M \models^\cap \{\perp\} \lor (\exists M' \subseteq M. \text{ finite } M' \land (\exists C \in N. M' \models^\cap \{C\})) $$

<footnote n="5">⁵ Since the completion of this formalization, a version of superposition that can also be used became available in the AFP [5, 6].</footnote>

<footnote n="6">⁶ Not to be mistaken for $\models^\cap$ introduced in Sec. 2.1.</footnote>
The naive definition of $|\models|$ from $|\models|$ is just $M \models^U N \leftrightarrow \exists C \in N. M \models^\neg \{C\}$, but it only
verifies (D2)-(D4). To additionally verify (D1), the disjunct $M \models^\neg \{\perp\}$ is added, and finally
we consider the finite subset $M'$ of $M$ to ensure that (D5) holds. In practice, a prover always
works with a finite set of clauses so $M'$ and $M$ can be the same. To prove that $|\models|$ is a
consequence relation, we use it to instantiate the locale *consequence_relation*.

► **Remark 12.** Our initial intuition to capture (D5) was to rely on the compactness of first-order logic [9]. This would have been possible had we worked with ground clauses (i.e., clauses without variables) since in that setup $|\models^\neg|$ can be related to satisfiability rather straightforwardly ($M \models^\neg \{C\} \leftrightarrow M \cup \{\neg 1 \mid 1 \in C\} \models^\neg \{\perp\}$). However, the connection between $|\models^\neg|$ and satisfiability in full first-order logic is not as straightforward due to the presence of quantifiers and this prevents the use of the compactness of first-order logic to prove that of our consequence relation.

All of this is done in a locale `FO_resolve_prover_disjunctive` that extends the locale `FO_resolve_prover` from the theory `FO_Ordered_Resolution_Prover` mentioned previously. The internals of first-order ordered resolution are not relevant to this paper so we abstract over a lot of technical details. In particular, it should be noted that finding and then building the correct $|\models^\neg|$ among all those offered by `FO_resolve_prover` requires some thought and a good understanding of the saturation framework. Indeed, `FO_resolve_prover` offers many consequence relations, for example at the ground level, lifted at the non-ground level, over an intersection of ground calculi, or over an intersection of all possible lifted calculi (the reduced version of the last one is the one we need).

## 5.3 Lightweight AVATAR

Equipped with a disjunctive entailment and the locale for binary splitting, building a model *LA* of Lightweight AVATAR in the splitting framework is straightforward. We start with a locale *LA_calculus* that extends *FO_resolve_prover_disjunctive*. The extension adds the *asn* and *fm1* functions, needed for the annotation. These functions are kept abstract and the set of annotations too (as the type 'a'). Further refinements of this instance, possibly leading to an executable verified resolution solver with splitting, are left for future work.

*LA_calculus* provides the tuple *O*<sup>U</sup> = (*FInf*, *FRedRed*<sub>*I*</sub>, *FRed*<sub>*F*</sub>, |*F*<sup>U</sup>>). We prove first that (*FInf*, |*F*<sup>U</sup>) is a sound inference system and then that *O*<sup>U</sup> is a calculus by invoking the results from the saturation framework.

interpretation entails_G_disj sound_inf_system: sound_inference_system FInf ⊥ (|=U)

interpretation LA_is_calculus: calculus ⊥ FInf (|=U) FRedRed_I FRed_F

Next we show that $O^U$ is a sound calculus. We use the same relation $|\models$ to build the standard and the sound consequence relations. All proof obligations are trivially discharged using the interpretations above.

interpretation LA_isSound_calculus:

$$
sound\_calculus \perp FInf (|\models) (|\models) FRedRed_I FRed_F
$$

The assumptions of the locale *LA_calculus* and the results above make it possible to
annotate *O*^U and then obtain a splitting calculus without optional rules.

interpretation LA_is_AF_calculus:

$$
annotated\_calculus \perp FInf (|\models) (|\models) FRedRed_I FRed_F \text{ fm1 asn}
$$

interpretation core_LA_calculus:

$$
splitting\_calculus \perp FInf (|\models) (|\models) FRedRed_I FRed_F \text{ fm1 asn}
$$
The locale `core_LA_calculus` above defines the annotated notions $\perp_{LA}$, $LAInf$, $\models_{LA}$, $\models_{sLA}$, $LARed_I$ and $LARed_F$ that are versions of $\perp_{AF}$, $SInf$, $\models_{AF}$, $\models_{sAF}$, $SRed_I$ and $SRed_F$ specified based on $O^\cup$. Then we show that this calculus can be "extended" with empty sets of extra rules so that it can be used for further, more useful, extensions.

interpretation $AF\_calculus\_extended \perp_{LA} LAInf (\models_{LA}) (\models_{sLA}) LARed_I LARed_F \emptyset \emptyset$

We add the binary splitting rule on top of this construction.

interpretation with_BinSplit:

$$AF\_calculus\_with\_binsplit \perp_{LA} LAInf \models_{LA} \models_{sLA} LARed_I LARed_F \emptyset \emptyset \text{ bin\_splittable}$$

It defines the set of simplifications `Simps_with_Bin_Split` that we use to finally obtain the full LA calculus.

sublocale LA:

$$AF\_calculus\_extended \perp_{LA} LAInf \models_{LA} \models_{sLA} LARed_I LARed_F \text{ Simps\_with\_BinSplit} \emptyset$$

Whereas we keep all intermediate locale instances private to the context by using the interpretation command, we expose LA to the outside by declaring it as a sublocale.

To prove that LA is complete, we must first show that $O^\cup$ is statically complete. The proof follows from the static completeness of $O$ and the agreement of $\models^\cap$ and $\models^\cup$ when their right-hand side is a singleton.

interpretation `statically_complete_calculus \perp FInf (\models^\cup) FRed_{R_I} FRed_F`

Then we obtain the strong static and dynamic completeness of LA from the splitting framework.

sublocale `strong_statically_complete_annotated_calculus \perp FInf (\models^\cup) (\models^\cup) FRed_{R_I} FRed_F` fml asn LAInf LARed_I LARed_F

sublocale `strong_dynamically_complete_annotated_calculus \perp FInf (\models^\cup) (\models^\cup) FRed_{R_I} FRed_F` fml asn LAInf LARed_I LARed_F

# 6 Conclusion

We presented an Isabelle/HOL framework for modeling saturation-based calculi augmented with splitting that preserves soundness and completeness. It provides a number of optional inference and simplification rules, in an architecture that facilitates their combination as well as the creation of new optional rules. We applied this framework to model Lightweight AVATAR [21], an existing splitting approach that we instantiated on top of the ordered resolution calculus. The formalization contains ~8500 non-blank lines of Isabelle/HOL code.

There is a clear avenue of future work for this project, as only the first two sections (introduction excluded) of the pen-and-paper framework by Ebner et al. [7] have been covered. There remain three key splitting features, namely model guidance, locking and timestamping before the ultimate goal of modeling a sound and complete AVATAR [20] in Isabelle/HOL is reached. Each of these layers promises its own challenges, but also its own rewards in the form of an increased coverage of existing splitting techniques, including labeled splitting [8] and SMT solving with complete instantiation strategies [13].
References

1 Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors, *Handbook of Automated Reasoning* (in 2 volumes), pages 19–99. Elsevier and MIT Press, 2001. doi:10.1016/b978-044450813-3/50004-7.

2 Clemens Ballarin. Locales: A module system for mathematical theories. *J. Autom. Reason.*, 52(2):123–153, 2014. doi:10.1007/s10817-013-9284-7.

3 Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. A modular splitting framework for saturation theorem proving. *Archive of Formal Proofs*, June 2025. , Formal proof development. URL: https://isa-afp.org/entries/Splitting_Framework.html.

4 Jasmin Christian Blanchette and Sophie Tourret. Extensions to the comprehensive framework for saturation theorem proving. *Archive of Formal Proofs*, August 2020. , Formal proof development. URL: https://isa-afp.org/entries/Saturation_Framework_Extensions.html.

5 Martin Desharnais and Balazs Toth. A modular formalization of superposition. *Archive of Formal Proofs*, October 2024. , Formal proof development. URL: https://isa-afp.org/ entries/Superposition_Calculus.html.

6 Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A modular formalization of superposition in Isabelle/HOL. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, *15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia*, volume 309 of LIPIcs, pages 12:1–12:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.ITP.2024.12.

7 Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. Unifying splitting. *J. Autom. Reason.*, 67(2):16, 2023. doi:10.1007/s10817-023-09660-8.

8 Arnaud Fietzke and Christoph Weidenbach. Labelled splitting. *Ann. Math. Artif. Intell.*, 55(1-2):3–34, 2009. doi:10.1007/s10472-009-9150-9.

9 John Harrison. Formalizing basic first order model theory. In *TPHOLs*, volume 1479 of *Lecture Notes in Computer Science*, pages 153–170. Springer, 1998. doi:10.1007/BFB0055135.

10 Julius Michaelis and Tobias Nipkow. Formalized proof systems for propositional logic. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, *23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary*, volume 104 of LIPIcs, pages 5:1–5:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.TYPES.2017.5.

11 Julius Michaelis and Tobias Nipkow. Propositional proof systems. *Archive of Formal Proofs*, June 2017. , Formal proof development. URL: https://isa-afp.org/entries/ Propositional_Proof_Systems.html.

12 Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In John Alan Robinson and Andrei Voronkov, editors, *Handbook of Automated Reasoning* (in 2 volumes), pages 371–443. Elsevier and MIT Press, 2001. doi:10.1016/b978-044450813-3/50009-6.

13 Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting enumerative instantiation. In Dirk Beyer and Marieke Huisman, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II*, volume 10806 of Lecture Notes in Computer Science, pages 112–131. Springer, 2018. doi:10.1007/978-3-319-89963-3_7.

14 Alexandre Riazanov and Andrei Voronkov. Splitting without backtracking. In Bernhard Nebel, editor, *Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001, Seattle, Washington, USA, August 4-10, 2001*, pages 611–617. Morgan Kaufmann, 2001.

15 Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, and Uwe Waldmann. Formalizing Bachmair and Ganzinger’s ordered resolution prover. *J. Autom. Reason.*, 64(7):1169–1195, 2020. doi:10.1007/s10817-020-09561-0.
16 Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified functional implementation of Bachmair and Ganzinger's ordered resolution prover. *Arch. Formal Proofs*, 2018, 2018. URL: https://www.isa-afp.org/entries/Functional_Ordered_Resolution_Prover.html.

17 Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified prover based on ordered resolution. In Assia Mahboubi and Magnus O. Myreen, editors, *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*, pages 152-165. ACM, 2019. doi:10.1145/3293880.3294100.

18 Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. Formalization of Bachmair and Ganzinger's ordered resolution prover. *Archive of Formal Proofs*, January 2018. , Formal proof development. URL: https://isa-afp.org/entries/Ordered_Resolution_Prover.html.

19 Sophie Tourret and Jasmin Blanchette. A modular Isabelle framework for verifying saturation provers. In Catalin Hritcu and Andrei Popescu, editors, *CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021*, pages 224-237. ACM, 2021. doi:10.1145/3437992.3439912.

20 Andrei Voronkov. AVATAR: the architecture for first-order theorem provers. In Armin Biere and Roderick Bloem, editors, *Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings*, volume 8559 of *Lecture Notes in Computer Science*, pages 696-710. Springer, 2014. doi:10.1007/978-3-319-08867-9_46.

21 Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. *J. Autom. Reason.*, 66(4):541-564, 2022. doi:10.1007/s10817-021-09613-z.

22 Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. A comprehensive framework for saturation theorem proving. *J. Autom. Reason.*, 66(4):499-539, 2022. doi:10.1007/s10817-022-09621-7.

23 Max Zorn. A remark on method in transfinite algebra. *Bulletin of the American Mathematical Society*, 41(10):667-670, 1935.