Formalizing Splitting in Isabelle/HOL

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 sublocales or interpretations [2].

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

Notably our disjunctive notion has a cut property (D4) as well as compactness (D5) but it is not transitive. Intuitively, M $\vDash$ 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 $\vDash$_∩ from $\vDash$ such that M $\vDash$_∩ {C} $⟷$ M $\vDash$ {C} in the following way: M $\vDash$_∩ N $⟷$ $\forall$C$\in$N. M $\vDash$ {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.

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’ $\wedge$ N $\subseteq$ N’ $\wedge$ $\neg$M’ $\vDash$ N’} and the relation zorn_relation = {(C₁,C₂) $\in$ A $\times$ A. C₁$⪯$_sC₂} where (M,N) $⪯$_s (M’,N’) if and only if M $\subseteq$ M’ 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 ${𝐅}_{\sim }=𝐅\cup \{\sim C\mid C\in {𝐅}_{\sim }\}$ where $𝐅$ 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:

The extension of $\vDash$ to $\vDash$_∼ on signed formulas (of type ’f sign set) is defined directly in the locale consequence_relation.

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

• $\mathrm{■}$

  an inference system, i.e., a set of inferences Inf, where an inference $\mathrm{\iota }$ = Infer P C with

  • –

    premises prems_of $\mathrm{\iota }$ = P, a list of formulas, and

  • –

    a conclusion concl_of $\mathrm{\iota }$ = C, a formula;

• $\mathrm{■}$

  a disjunctive consequence relation as described in the previous section;

adding as two arguments a redundancy criterion, i.e., a pair of functions (Red_F,Red_I) where

• $\mathrm{■}$

  Red_F N is the set of redundant formulas with respect to the set of formulas N and

• $\mathrm{■}$

  Red_I 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:

The numbering follows that of “Unifying Splitting”, except for (R0) which is only implicitly present in the definition of Red_I. 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 $\vDash$_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.

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 $⟹$ N $\vDash$ {$\perp$} $⟹$ $\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. typedef ’a infinite_llist = {l :: ’a llist. llength l = $\mathrm{\infty }$} Using sequences, we define derivations, i.e., sequences $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">Ns</em>}={({\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">N</em>}}_i)}_{i\in \mathbb{N}}$ such that ${\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">N</em>}}_i⊳{\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">N</em>}}_{i+1}$ for any $i$, where M $⊳$ N $\equiv$ (M - N $\subseteq$ Red_F N). Note that $⊳$ is left generic, and that in particular any transformation that preserves soundness is allowed, not limited to the inferences of the calculus. $⊳$ 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 ($⊳$) Ns $⟹$ fair Ns $⟹$ llhd Ns $\vDash$ {$\perp$} $⟹$ $\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.

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:

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 $𝒞$ as (F_of $𝒞$) $\leftarrow$ (A_of $𝒞$). For example, the bottom element of A-formulas, denoted $\perp$_AF, is $\perp$ $\leftarrow$ $\mathrm{\varnothing }$. 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 Pos v or Neg v belongs to the interpretation. In Isabelle, we define propositional interpretations as a type ’v 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 fml :: ’v $\Rightarrow$ ’f and asn :: ’f sign $\Rightarrow$ ’v 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 $\vDash$ and $\vDash$_s of a sound calculus leads to several complex proofs. It defines the annotated consequence relations $\vDash$_AF and $\vDash$_sAF. A salient point in this part of the formalization is that we rely on the compactness of propositional logic to prove (D5) for $\vDash$_AF and $\vDash$_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 $𝒥$ is a propositional model of a set of A-formulas $𝒩$, denoted $𝒥$ $\vDash$_p $𝒩$, when ($𝒩$_⊥)_J = $\mathrm{\varnothing }$. It relies on the splitting framework’s projection mechanism, including the enabled projection $𝒩$_J = {F_of $𝒞$ | $𝒞$ $\in$ $𝒩$ $\wedge$ A_of $𝒞$ $\subseteq$ $𝒥$} that filters formulas in a set $𝒩$ depending on whether their annotation agrees with a given propositional interpretation $𝒥$, and the propositional projection $𝒩$_⊥ = {$𝒞$ $\in$ $𝒩$ | F_of $𝒞$ = $\perp$}. The latter only keeps the propositional clauses in $𝒩$. Annotated formulas of the form $\perp$ $\leftarrow$ {a_i}_i∈1..n are called thus because any annotated formula $𝒞$ $\leftarrow$ {a_i}_i∈1..n can be interpreted as $𝒞\vee {\bigvee }_{i=1}^n\neg {\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">a</em>}}_i$ and if $𝒞=\perp$ then the remaining ${\bigvee }_{i=1}^n\neg {\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">a</em>}}_i$ is a clause in propositional logic. A set of propositional clauses $𝒩$_⊥ without a propositional model is propositionally unsatisfiable, which is equivalent to $𝒩$_⊥ $\vDash$_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.

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.

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.

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_extended.

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_extended.

The locale AF_calculus_extended 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 fml 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_extended 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:

where OPT is either infs for optional inferences or simps for simplification rules. In the first case $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">Simps’</em>}=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">Simps</em>}$ and $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">OptInfs’</em>}=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">OptInfs\_with\_XYZ</em>}$ and in the second case $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">Simps’</em>}=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">Simps\_with\_XYZ</em>}$ and $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">OptInfs’</em>}=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">OptInfs</em>}$. 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.

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 $\leftarrow$ A is a tautology for the sound consequence relation. The inference rule Approx approximates an F-formula by one of its associated assertions $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">a</em>}\in$ A. Finally, the rule StrongUnsat is as Unsat but uses $\vDash$_sAF instead of $\vDash$_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_approx locale. It includes abbreviations following the same convention as in annotated_calculus:

We can now declare AF_calculus_extended as a sublocale of AF_calculus_with_approx 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.

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 ($\sim$ 275 lines of Isabelle/HOL).

The simplifications introduced in “Unifying Splitting” are presented in Figure 3. A formula C is splittable into formulas C₁, $\dots$, C_n if there are at least two formulas in the set – otherwise, splitting would serve no purpose – and if C $\vDash$_s {C₁, $\dots$, C_n} and C $\in$ Red_F {C_i} for each i. Thus, the rule Split performs a case analysis on C. The conclusion $\perp$ $\leftarrow$ {$\neg$a₁, $\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)\vee Q(y,b),\neg P(a),\neg Q(z,z)\}$ into $\{P(x)\leftarrow \{p\},Q(y,b)\leftarrow \{q\},\perp \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.⁵⁵5https://matryoshka-project.github.io/#Publications Briefly, the precondition of Collect in “Unifying Splitting” uses $\vDash$_sAF rather than $\vDash$_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:

AF_calculus_with_split defines the abbreviations

• $\mathrm{■}$

  split_pre, abstracted by splittable,

• $\mathrm{■}$

  split_res, including all the formulas in fset $𝒞$s as well as Pair $\perp$ A_∪, and

• $\mathrm{■}$

  split_simp, such that split_simp $𝒞$ $𝒞$s $\equiv$ Simplify {$𝒞$} (split_res $𝒞$ $𝒞$s)

to augment Simps with the Split inferences:

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 $\perp$_AF SInf $\vDash$_AF $\vDash$_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 $\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">C</em>}\ne \perp$ to the splittable predicate, while a_i $\in$ 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.

Lightweight AVATAR operates in first-order logic on formulas in clausal normal form. It extends the signature $\mathrm{\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 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_splittable 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)\vee 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_splittable can be found.

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.⁶⁶6Since the completion of this formalization, a version of superposition that can also be used became available in the AFP [5, 6].

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 $𝖮$. Given a signature $\mathrm{\Sigma }$ and a set F of $\mathrm{\Sigma }$-clauses where $\perp$ denotes the empty clause, the calculus $𝖮$ is the tuple $(\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FInf</em>},\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FRed</em>}\text{<sub class="ltx\_sub"><span class="ltx\_text ltx\_font\_serif">I</span></sub>},\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FRed</em>}\text{<sub class="ltx\_sub"><span class="ltx\_text ltx\_font\_serif">F</span></sub>},\vDash \text{<sup class="ltx\_sup"><span class="ltx\_text ltx\_font\_serif">∩</span></sup>})$ such that:

• $\mathrm{■}$

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

• $\mathrm{■}$

  $(\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FRed</em>}\text{<sub class="ltx\_sub"><span class="ltx\_text ltx\_font\_serif">I</span></sub>},\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FRed</em>}\text{<sub class="ltx\_sub"><span class="ltx\_text ltx\_font\_serif">F</span></sub>})$ is the standard redundancy criterion [1, section 4.2.2], and

• $\mathrm{■}$

  $\vDash$^∩ is the usual (conjunctive) Herbrand entailment.⁷⁷7Not to be mistaken for $\vDash$_∩ introduced in Sec. 2.1.

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 FRed_I with the appropriate notion, which we denote here FRedRed_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:

All of this is done in a locale FO_resolution_prover_disjunctive that extends the locale FO_resolution_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 $\vDash$^∩ among all those offered by FO_resolution_prover requires some thought and a good understanding of the saturation framework. Indeed, FO_resolution_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).

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_resolution_prover_disjunctive. The extension adds the asn and fml 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 ${𝖮}^{\cup }=(\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FInf</em>},\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FRedRed</em>}\text{<sub class="ltx\_sub"><span class="ltx\_text ltx\_font\_serif">I</span></sub>},\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FRed</em>}\text{<sub class="ltx\_sub"><span class="ltx\_text ltx\_font\_serif">F</span></sub>},\vDash \text{<sup class="ltx\_sup"><span class="ltx\_text ltx\_font\_serif">∪</span></sup>})$. We prove first that $(\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">FInf</em>},\vDash \text{<sup class="ltx\_sup"><span class="ltx\_text ltx\_font\_serif">∪</span></sup>})$ is a sound inference system and then that ${𝖮}^{\cup }$ is a calculus by invoking the results from the saturation framework.

Next we show that ${𝖮}^{\cup }$ is a sound calculus. We use the same relation $\vDash$^∪ to build the standard and the sound consequence relations. All proof obligations are trivially discharged using the interpretations above.

The assumptions of the locale LA_calculus and the results above make it possible to annotate ${𝖮}^{\cup }$ and then obtain a splitting calculus without optional rules.

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 ${𝖮}^{\cup }$ is statically complete. The proof follows from the static completeness of $𝖮$ and the agreement of $\vDash$^∩ and $\vDash$^∪ when their right-hand side is a singleton.