# Unifying Splitting

Gabriel Ebner, Jasmin Blanchette, Sophie Tourret

► To cite this version:

Gabriel Ebner, Jasmin Blanchette, Sophie Tourret. Unifying Splitting. Journal of Automated Reasoning, 2023, 67 (2), pp.16. 10.1007/s10817-023-09660-8. hal-04298584

HAL Id: hal-04298584

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

Submitted on 21 Nov 2023

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 CC BY 4.0 - Attribution - International License
# Unifying Splitting

Gabriel Ebner* · Jasmin Blanchette* · Sophie Tourret*

the date of receipt and acceptance should be inserted later

**Abstract** AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and that embeds the result in a prover guided by a SAT solver. The framework also allows us to study *locking*, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.

## 1 Introduction

One of the great strengths of saturation calculi such as resolution [26] and superposition [1] is that they avoid case analyses. Derived clauses hold unconditionally, and the prover can stop as soon as it derives the empty clause, without having to backtrack. The drawback is that these calculi often generate long, unwieldy clauses that slow down the prover. A remedy is to partition the search space by splitting a multiple-literal clause $C_1 \lor \dots \lor C_n$ into subclauses $C_i$ that share no variables. Splitting approaches include splitting with backtracking [31, 32], splitting without backtracking [25], labeled splitting [13], and AVATAR [28].

The AVATAR architecture, which is based on a satisfiability (SAT) solver, is of particular interest because it is so successful. Voronkov reported that an AVATAR-enabled Vampire could solve 421 TPTP problems that had never been solved before by any system [28, Sect. 9], a mind-boggling number. Intuitively, AVATAR works well in combination with the superposition calculus because it combines superposition's strong equality reasoning with the SAT solver's strong clausal reasoning. It is also appealing theoretically, because it gracefully

<footnote>Gabriel Ebner · Jasmin Blanchette
Vrije Universiteit Amsterdam, Amsterdam, the Netherlands
E-mail: gebner@gebner.org, j.c.blanchette@vu.nl</footnote>

<footnote>Jasmin Blanchette · Sophie Tourret
Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
E-mail: {jasmin.blanchette,sophie.tourret} @inria.fr</footnote>

<footnote>Jasmin Blanchette · Sophie Tourret
Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany
E-mail: {jasmin.blanchette,stourret} @mpi-inf.mpg.de</footnote>
generalizes traditional saturation provers and yet degenerates to a SAT solver if the problem is propositional.

To illustrate the approach, we follow the key steps of an AVATAR-enabled resolution prover on the initial clause set containing $\neg p(a), \neg q(z,z)$, and $p(x) \lor q(y,b)$. The disjunction can be split into $p(x) \leftarrow \{[p(x)]\}$ and $q(y,b) \leftarrow \{[q(y,b)]\}$, where $C \leftarrow \{[C]\}$ indicates that the clause C is enabled only in models in which the associated propositional variable $[C]$ is true. A SAT solver is then run to choose a model $\mathcal{J}$ of $[p(x)] \lor [q(y,b)]$. Suppose $\mathcal{J}$ makes $[p(x)]$ true and $[q(y,b)]$ false. Then resolving $p(x) \leftarrow \{[p(x)]\}$ with $\neg p(a)$ produces $\perp \leftarrow \{[p(x)]\}$, meaning that $[p(x)]$ must be false. Next, the SAT solver makes $[p(x)]$ false and $[q(y,b)]$ true. Resolving $q(y,b) \leftarrow \{[q(y,b)]\}$ with $\neg q(z,z)$ yields $\perp \leftarrow \{[q(y,b)]\}$, meaning that $[q(y,b)]$ must be false. Since both disjuncts of $[p(x)] \lor [q(y,b)]$ are false, the SAT solver reports "unsatisfiable," concluding the refutation.

What about refutational completeness? Far from being a purely theoretical concern, establishing completeness—or finding counterexamples—could yield insights into splitting and perhaps lead to an even stronger AVATAR. Before we can answer this open question, we must mathematize splitting. Our starting point is the saturation framework by Waldmann, Tourret, Robillard, and Blanchette [29], based on the work of Bachmair and Ganzinger [2]. It covers a wide array of techniques, but “the main missing piece of the framework is a generic treatment of clause splitting” [29, p. 332]. We provide that missing piece, in the form of a splitting framework, and use it to show the completeness of an AVATAR-like architecture. The framework is currently a pen-and-paper creature; a formalization using Isabelle/HOL [21] is underway.

Our framework has five layers, linked by refinement. The first layer consists of a *base calculus*, such as resolution or superposition. It must be presentable as an inference system and a redundancy criterion, as required by the saturation framework, and it must be refutationally complete.

From a base calculus, our framework can be used to derive the second layer, which we call the *splitting calculus* (Sect. 3). This extends the base calculus with splitting and inherits the base’s completeness. It works on A-clauses or A-formulas of the form $C \leftarrow A$, where C is a base clause or formula and A is a set of propositional literals, called assertions (Sect. 2).

Using the saturation framework, we can prove the dynamic completeness of an abstract prover, formulated as a transition system, that implements the splitting calculus. However, this ignores a major component of AVATAR: the SAT solver. AVATAR considers only inferences involving A-formulas whose assertions are true in the current propositional model. The role of the third layer is to reflect this behavior. A *model-guided prover* operates on states of the form $(\mathcal{J}, \mathcal{N})$, where $\mathcal{J}$ is a propositional model and $\mathcal{N}$ is a set of A-formulas (Sect. 4). This layer is also dynamically complete.

The fourth layer introduces AVATAR’s *locking* mechanism (Sect. 5). With locking, an A-formula $D \leftarrow B$ can be temporarily disabled by another A-formula $C \leftarrow A$ if C subsumes D, even if $A \not\subseteq B$. Here we make a first discovery: AVATAR-style locking compromises completeness and must be curtailed.

Finally, the fifth layer is an *AVATAR-based prover* (Sect. 6). This refines the locking model-guided prover of the fourth layer with the given clause procedure, which saturates an A-formula set by distinguishing between active and passive A-formulas. Here we make another discovery: Selecting A-formulas fairly is not enough to guarantee completeness. We need a stronger criterion.

There are also implications for other architectures. In a hypothetical tête-à-tête with the designers of labeled splitting, they might gently point out that by pioneering the use of a propositional model, including locking, they almost invented AVATAR themselves. Likewise,
developers of satisfiability modulo theories (SMT) solvers might be tempted to claim that Voronkov merely reinvented SMT. To investigate such questions, we apply our framework to splitting without backtracking, labeled splitting, and SMT with quantifiers (Sect. 7). This gives us a solid basis for comparison as well as some new theoretical results.

A shorter version of this article was presented at CADE-28 [11]. This article extends the conference paper with more explanations, examples, counterexamples, and proofs. We strengthened the definition of consequence relation to require compactness, which allowed us to simplify property (D4). The property (D4) from the conference paper is proved as Lemma 5. The definition of strongly finitary was also changed to include a stronger condition on the introduced assertions, which is needed for the proof of Lemma 72.

## 2 Preliminaries

Our framework is parameterized by abstract notions of formulas, consequence relations, inferences, and redundancy. We largely follow the conventions of Waldmann et al. [29]. A-formulas generalize Voronkov's A-clauses [28].

### 2.1 Formulas

A set $\mathbf{F}$ of formulas, ranged over by $C, D \in \mathbf{F}$, is a set that contains a distinguished element $\perp$ denoting falsehood. A consequence relation $\models$ over $\mathbf{F}$ is a relation $\models \subseteq (\mathcal{P}(\mathbf{F}))^2$ with the following properties for all sets $M, M', N, N' \subseteq \mathbf{F}$ and formulas $C, D \in \mathbf{F}$:

(D1) $\{\perp\} \models \emptyset$;

(D2) $\{C\} \models \{C\}$;

(D3) if $M' \subseteq M$ and $N' \subseteq N$, then $M' \models N'$ implies $M \models N$;

(D4) if $M \models N \cup \{C\}$ and $M' \cup \{C\} \models N'$, then $M \cup M' \models N \cup N'$;

(D5) if $M \models N$, then there exist finite sets $M' \subseteq M$ and $N' \subseteq N$ such that $M' \models N'$.

The intended interpretation of $M \models N$ is conjunctive on the left but disjunctive on the right: "$\wedge M \rightarrow \vee N$". The disjunctive interpretation of $N$ will be useful to define splittability abstractly in Sect. 3.1. Property (D4) is called the cut rule, and (D5) is called compactness.

For their saturation framework, Waldmann et al. instead consider a fully conjunctive version of the consequence relation, with different properties. The incompatibility can easily be repaired: Given a consequence relation $\models$, we can obtain a consequence relation $\models'$ in their sense by defining $M \models' N$ if and only if $M \models \{C\}$ for every $C \in N$. The two versions differ only when the right-hand side is not a singleton. The conjunctive version $\models'$ can then be used when interacting with the saturation framework.

The $\models'$ notation can be extended to allow negation on either side. Let $\mathbf{F}_{\sim}$ be defined as $\mathbf{F} \uplus \{\sim C | C \in \mathbf{F}_{\sim}\}$ such that $\sim\sim C = C$. Given $M, N \subseteq \mathbf{F}_{\sim}$, we set $M \models N$ if and only if

$$ \begin{array}{l} \{C \in \mathbf{F} | C \in M\} \cup \{C \in \mathbf{F} | \sim C \in N\} \\ \models \{C \in \mathbf{F} | \sim C \in M\} \cup \{C \in \mathbf{F} | C \in N\} \end{array} $$

We write $M \models N$ for the conjunction of $M \models N$ and $N \models M$.

**Lemma 1** Let $C \in \mathbf{F}_{\sim}$. Then $\{C\} \cup \{\sim C\} \models \{\perp\}$.

*Proof* This holds by (D2) and (D3) due to the definition of $\models$ on $\mathbf{F}_{\sim}$.
Following the saturation framework [29, p. 318], we distinguish between the consequence relation $|=$ used for stating refutational completeness and the consequence relation $|\cong$ used for stating soundness. For example, $|=$ could be entailment for first-order logic with equality, whereas $|\cong$ could also draw on linear arithmetic, or interpret Skolem symbols so as to make skolemization sound. Normally $|\models \subseteq |\cong$, but this is not required.

**Example 1** In clausal first-order logic with equality, as implemented in superposition provers, the formulas in $\mathbf{F}$ consist of clauses over a signature $\Sigma$. Each clause $C$ is a finite multiset of literals $L_1, \dots, L_n$ written $C = L_1 \lor \dots \lor L_n$. The clause's variables are implicitly quantified universally. Each literal $L$ is either an atom or its negation ($\neg$), and each atom is an unoriented equation $s \approx t$. We define the consequence relation $|=$ by letting $M|=$ $N$ if and only if every first-order $\Sigma$-interpretation that satisfies all clauses in $M$ also satisfies at least one clause in $N$.

## 2.2 Calculi and Derivations

A refutational calculus combines a set of inferences, which are a priori mandatory, and a redundancy criterion, which identifies inferences that a posteriori need not be performed as well as formulas that can be deleted.

Let $\mathbf{F}$ be a set of formulas equipped with $\perp$. An $\mathbf{F}$-inference $\iota$ is a tuple $(C_n, \dots, C_1, D) \in \mathbf{F}^{n+1}$. The formulas $C_n, \dots, C_1$ are the premises, and $D$ is the conclusion. Define prems($\iota$) = $\{C_n, \dots, C_1\}$ and concl($\iota$) = $\{D\}$. An inference $\iota$ is sound w.r.t. $|\cong$ if prems($\iota$) $|\cong$ concl($\iota$). An inference system Inf is a set of $\mathbf{F}$-inferences.

Given $N \subseteq \mathbf{F}$, we let $\text{Inf}(N)$ denote the set of all inferences in $\text{Inf}$ whose premises are included in $N$, and $\text{Inf}(N, M) = \text{Inf}(N \cup M) \setminus \text{Inf}(N \setminus M)$ for the set of all inferences in $\text{Inf}$ such that one or more premises are in $M$ and the remaining premises are in $N$.

A redundancy criterion for an inference system $\text{Inf}$ and a consequence relation $|=$ is a pair $\text{Red} = (\text{Red}_1, \text{Red}_F)$, where $\text{Red}_1 : \mathcal{P}(\mathbf{F}) \to \mathcal{P}(\text{Inf})$ and $\text{Red}_F : \mathcal{P}(\mathbf{F}) \to \mathcal{P}(\mathbf{F})$ enjoy the following properties for all sets $M, N \subseteq \mathbf{F}$:

(R1) if $N|\models \{\perp\}$, then $N \setminus \text{Red}_F(N)|\models \{\perp\}$;

(R2) if $M \subseteq N$, then $\text{Red}_F(M) \subseteq \text{Red}_F(N)$ and $\text{Red}_1(M) \subseteq \text{Red}_1(N)$;

(R3) if $M \subseteq \text{Red}_F(N)$, then $\text{Red}_F(N) \subseteq \text{Red}_F(N \setminus M)$ and $\text{Red}_1(N) \subseteq \text{Red}_1(N \setminus M)$;

(R4) if $\iota \in \text{Inf}$ and $\text{concl}(\iota) \in N$, then $\iota \in \text{Red}_1(N)$.

Inferences in $\text{Red}_1(N)$ and formulas in $\text{Red}_F(N)$ are said to be redundant w.r.t. $N$. $\text{Red}_1$ indicates which inferences need not be performed, whereas $\text{Red}_F$ justifies the deletion of formulas deemed useless. The above properties make the passage from static to dynamic completeness possible: (R1) ensures that deleting a redundant formula preserves a set's inconsistency, so as not to lose refutations; (R2) and (R3) ensure that arbitrary formulas can be added and redundant formulas can be deleted by the prover; and (R4) ensures that adding an inference's conclusion to the formula set makes the inference redundant.

A pair $(\text{Inf}, \text{Red})$ forms a calculus. A set $N \subseteq \mathbf{F}$ is saturated w.r.t. $\text{Inf}$ and $\text{Red}_1$ if $\text{Inf}(N) \subseteq \text{Red}_1(N)$. The calculus $(\text{Inf}, \text{Red})$ is statically (refutationally) complete (w.r.t. $|=$) if for every set $N \subseteq \mathbf{F}$ that is saturated w.r.t. $\text{Inf}$ and $\text{Red}_1$ and such that $N|\models \{\perp\}$, we have $\perp \in N$.

**Lemma 2** Assume that the calculus $(\text{Inf}, \text{Red})$ is statically complete. Then $\perp \notin \text{Red}_F(N)$ for every $N \subseteq \mathbf{F}$.
**Proof** By (R2), it suffices to show $⊥ \notin Red_F(\mathbf{F})$. Clearly, by (D2) and (D3), $\mathbf{F} \models \{⊥\}$. Thus, by (R1), $\mathbf{F} \setminus Red_F(\mathbf{F}) \models \{⊥\}$. Moreover, by (R3) and (R4), $\mathbf{F} \setminus Red_F(\mathbf{F})$ is saturated. Hence, since $(Inf, Red)$ is statically complete, $⊥ \in \mathbf{F} \setminus Red_F(\mathbf{F})$. Therefore, $⊥ \notin Red_F(\mathbf{F})$. □

**Remark 3** Given a redundancy criterion $(Red_1, Red_F)$, where $⊥ \notin Red_F(\mathbf{F})$, we can make it stricter as follows. Define $Red'_1$ such that $ι \in Red'_1(N)$ if and only if either $ι \in Red_1(N)$ or $⊥ \in N$. Define $Red'_F$ such that $C \in Red'_F(N)$ if and only if either $C \in Red_F(N)$ or else both $⊥ \in N$ and $C \neq ⊥$. Obviously, $Red' = (Red'_1, Red'_F)$ is a redundancy criterion. Moreover, if $N$ is saturated w.r.t. $Inf$ and $Red_1$, then $N$ is saturated w.r.t. $Inf$ and $Red'_1$, and if the calculus $(Inf, Red)$ is statically complete, then $(Inf, Red')$ is also statically complete. (In the last case, the condition $⊥ \notin Red_F(\mathbf{F})$ holds by Lemma 2.)

A sequence $(x_i)_i$ over a set $X$ is a function from $\mathbb{N}$ to $X$ that maps each $i \in \mathbb{N}$ to $x_i \in X$. Let $(X_i)_i$ be a sequence of sets. Its *limit inferior* is $X_\infty = \lim_{j \to \infty} X_j = \bigcup_i \bigcap_{j \ge i} X_j$, and its *limit superior* is $X^\infty = \limsup_{j \to \infty} X_j = \bigcap_i \bigcup_{j \ge i} X_j$. The elements of $X_\infty$ are called *persistent*. A sequence $(N_i)_i$ of sets of $\mathbf{F}$-formulas is *weakly fair* w.r.t. $Inf$ and $Red_1$ if $Inf(N_\infty) \subseteq \bigcup_i Red_1(N_i)$ and *strongly fair* if $limsup_{i \to \infty} Inf(N_i) \subseteq \bigcup_i Red_1(N_i)$. Weak fairness requires that all inferences possible from some index $i$ and ever after eventually be performed or become redundant for another reason. Strong fairness requires the same from all inferences that are possible infinitely often, even if not continuously so. Both can be used to ensure that some limit is saturated.

Given a relation $▷ \subseteq X^2$ (pronounced “triangle”), a $▷$-derivation is a sequence of $X$ elements such that $x_i▷x_{i+1}$ for every $i$. Finite runs can be extended to derivations by repeating the final state infinitely. We must then ensure that $▷$ supports such stuttering. Abusing language, and departing slightly from the saturation framework, we will say that a derivation $(x_i)_i$ terminates if $x_i = x_{i+1} = \dots$ for some index $i$.

Let $▷_{Red_F} \subseteq (\mathcal{P}(\mathbf{F}))^2$ be the relation such that $M▷_{Red_F} N$ if and only if $M \setminus N \subseteq Red_F(N)$. Note that it is reflexive and hence supports stuttering. The relation is also transitive due to (R3). We could additionally require soundness ($M \approx N$) or at least consistency preservation ($M \not\approx \{⊥\}$ implies $N \not\approx \{⊥\}$), but this is unnecessary for proving completeness.

The calculus $(Inf, Red)$ is *dynamically (refutationally) complete* (w.r.t. $|=$) if for every $▷_{Red_F}$-derivation $(N_i)_i$ that is weakly fair w.r.t. $Inf$ and $Red_1$ and such that $N_0 \models \{⊥\}$, we have $⊥ \in N_i$ for some $i$.

## 2.3 A-Formulas

We fix throughout a countable set $\mathbf{V}$ of propositional variables $v_0, v_1, \dots$. For each $v \in \mathbf{V}$, let $¬v \in \neg \mathbf{V}$ denote its negation, with $¬¬v = v$. We assume that a formula $fml(v) \in \mathbf{F}$ is associated with each propositional variable $v \in \mathbf{V}$. Intuitively, $v$ approximates $fml(v)$ at the propositional level. This definition is extended so that $fml(¬v) = \sim fml(v)$. A propositional literal, or *assertion*, $a \in \mathbf{A} = \mathbf{V} \cup \neg \mathbf{V}$ over $\mathbf{V}$ is either a propositional variable $v$ or its negation $¬v$.

A propositional interpretation $\mathcal{J} \subseteq \mathbf{A}$ is a set of assertions such that for every variable $v \in \mathbf{V}$, exactly one of $v \in \mathcal{J}$ and $¬v \in \mathcal{J}$ holds. We lift $fml$ to sets in an elementwise fashion: $fml(\mathcal{J}) = \{fml(a) \mid a \in \mathcal{J}\}$. In the rest of this article, we will often implicitly lift functions elementwise to sets. The condition on the variables ensures that $\mathcal{J}$ is propositionally consistent. $\mathcal{J}$ might nevertheless be inconsistent for $|=$, which takes into account the semantics of the formulas $fml(v)$ associated with the variables $v$; for example, we might have $\mathcal{J} = \{v_0, v_1\}$, $fml(v_0) = \mathbf{p}(x)$, and $fml(v_1) = \neg \mathbf{p}(a)$, and $\mathcal{J} \models \{⊥\}$.
An A-formula over a set **F** of base formulas and an assertion set **A** is a pair $\mathcal{C} = (C, A) \in \mathbf{AF} = \mathbf{F} \times \mathcal{P}_{\text{fin}}(\mathbf{A})$, written $C \leftarrow A$, where *C* is a formula and *A* is a finite set of assertions $\{a_1, \dots, a_n\}$ understood as an implication $a_1 \wedge \dots \wedge a_n \to C$. We identify $C \leftarrow \emptyset$ with *C* and define the projections $\lfloor C \leftarrow A \rfloor = C$ and $\lfloor (C_n \leftarrow A_n, \dots, C_0 \leftarrow A_0) \rfloor = (C_n, \dots, C_0)$. Moreover, $\mathcal{N} \leftarrow \mathcal{N}$ is the set consisting of all A-formulas of the form $\perp \leftarrow A \in \mathcal{N}$, where $A \in \mathcal{P}_{\text{fin}}(\mathbf{A})$. Since $\perp \leftarrow \{a_1, \dots, a_n\}$ can be read as $\neg a_1 \vee \dots \vee \neg a_n$, we call such A-formulas propositional clauses. (In contrast, we call a variable-free base formula such as $p \vee q$ a ground clause when **F** is first-order logic.) The set $\mathcal{N}_\perp$ represents the clauses considered by the SAT solver in the original AVATAR [28]. Note the use of calligraphic letters (e.g., $\mathcal{C}, \mathcal{N}$) to range over A-formulas and sets of A-formulas.

Model-guided provers only consider A-formulas whose assertions are true in the current interpretation. Thus we say that an A-formula $C \leftarrow A \in \mathbf{AF}$ is enabled in a propositional interpretation $\mathcal{J}$ if $A \subseteq \mathcal{J}$. A set of A-formulas is enabled in $\mathcal{J}$ if all of its members are enabled in $\mathcal{J}$. Given an A-formula set $\mathcal{N} \subseteq \mathbf{AF}$, the enabled projection $\mathcal{N}_\mathcal{J} \subseteq \lfloor \mathcal{N} \rfloor$ consists of the projections $\lfloor \mathcal{C} \rfloor$ of all A-formulas $\mathcal{C}$ enabled in $\mathcal{J}$. Analogously, the enabled projection $\text{Inf}_\mathcal{J} \subseteq \lfloor \text{Inf} \rfloor$ of a set $\text{Inf}$ of $\mathbf{AF}$-inferences consists of the projections $\lfloor \iota \rfloor$ of all inferences $\iota \in \text{Inf}$ whose premises are all enabled in $\mathcal{J}$.

A propositional interpretation $\mathcal{J}$ is a propositional model of $\mathcal{N}_\perp$, written $\mathcal{J} \models \mathcal{N}_\perp$, if $\perp \notin (\mathcal{N}_\perp)_\mathcal{J}$. (i.e., $(\mathcal{N}_\perp)_\mathcal{J} = \emptyset$). Moreover, we write $\mathcal{J} \vDash \mathcal{N}_\perp$ if $\perp \notin (\mathcal{N}_\perp)_\mathcal{J}$ or $\text{fml}(\mathcal{J}) \vDash \{\perp\}$. A set $\mathcal{N}_\perp$ is propositionally satisfiable if there exists an interpretation $\mathcal{J}$ such that $\mathcal{J} \models \mathcal{N}_\perp$. In contrast to consequence relations, propositional modelhood $\models$ interprets the set $\mathcal{N}_\perp$ conjunctively: $\mathcal{J} \models \mathcal{N}_\perp$ is informally understood as $\mathcal{J} \models \bigwedge \mathcal{N}_\perp$.

Given consequence relations $\models$ and $\vDash$, we lift them from $\mathcal{P}(\mathbf{F})$ to $\mathcal{P}(\mathbf{AF})$: $\mathcal{M} \models \mathcal{N}$ if and only if $\mathcal{M}_\mathcal{J} \models \lfloor \mathcal{N} \rfloor$ for every $\mathcal{J}$ in which $\mathcal{N}$ is enabled, and $\mathcal{M} \vDash \mathcal{N}$ if and only if $\text{fml}(\mathcal{J}) \cup \mathcal{M}_\mathcal{J} \vDash \lfloor \mathcal{N} \rfloor$ for every $\mathcal{J}$ in which $\mathcal{N}$ is enabled. The consequence relation $\models$ is used for the completeness of the splitting prover and only captures what inferences such a prover must perform. In contrast, $\vDash$ captures a stronger semantics: For example, thanks to $\text{fml}(\mathcal{J})$ among the premises for $\vDash$, the A-formula $\text{fml}(a) \leftarrow \{a\}$ is always a $\vDash$-tautology. Also note that assuming $\emptyset \not= \emptyset$, then $\models \vDash$ on sets that contain exclusively propositional clauses. When needed, we use $\vDash_\mathbf{F}$ to denote $\vDash$ on $\mathcal{P}(\mathbf{F})$ and analogously for $\vDash_{\mathbf{AF}}$, as well as $\models_\mathbf{F}$ and $\models_{\mathbf{AF}}$.

**Lemma 4** The relations $\models$ and $\vDash$ on $\mathcal{P}(\mathbf{AF})$ are consequence relations.

*Proof* We consider only $\vDash$; the proof for $\models$ is analogous. For (D1), we need to show $\text{fml}(\mathcal{J}) \cup \{\emptyset\} \vDash \emptyset$ for every $\mathcal{J}$ because $\emptyset$ is always enabled. This follows from (D1) and (D3). For (D2), we need to show $\text{fml}(\mathcal{J}) \cup \{C \leftarrow A\}_\mathcal{J} \vDash \lfloor C \leftarrow A \rfloor$, assuming $C \leftarrow A$ is enabled in $\mathcal{J}$. Hence it suffices to show $\text{fml}(\mathcal{J}) \cup \{C\} \vDash \{C\}$, which follows from (D2) and (D3). For (D3), it suffices to show $\text{fml}(\mathcal{J}) \cup \mathcal{M}_\mathcal{J} \vDash \lfloor \mathcal{N} \rfloor$ assuming that $\mathcal{N}$ is enabled in $\mathcal{J}$, and $\text{fml}(\mathcal{J}) \cup \mathcal{M}'_\mathcal{J} \vDash \lfloor \mathcal{N}' \rfloor$ for every $\mathcal{M}' \subseteq \mathcal{M}$ and $\mathcal{N}' \subseteq \mathcal{N}$. This follows from (D3) and monotonicity of $\lfloor \cdot \rfloor$ and $(\cdot)_\mathcal{J}$. For (D4), we need to show $\text{fml}(\mathcal{J}) \cup (\mathcal{M} \cup \mathcal{M}')_\mathcal{J} \vDash \lfloor \mathcal{N} \cup \mathcal{N}' \rfloor$, assuming $\text{fml}(\mathcal{J}) \cup \mathcal{M}_\mathcal{J} \vDash \lfloor \mathcal{N} \rfloor \cup \{C\}$ if $C \leftarrow A$ is enabled in $\mathcal{J}$, $\text{fml}(\mathcal{J}) \cup \mathcal{M}'_\mathcal{J} \cup \{C \leftarrow A\}_\mathcal{J} \vDash \lfloor \mathcal{N}' \rfloor$, and $\mathcal{N} \cup \mathcal{N}'$ is enabled in $\mathcal{J}$. This follows directly from (D4) if $C \leftarrow A$ is enabled in $\mathcal{J}$, and from (D3) if $C \leftarrow A$ is not enabled.

Finally, we show the compactness of $\Vdash_{\mathbf{AF}}$ (D5), using the compactness of propositional logic. First we consider the case where $\mathcal{N}$ is never enabled. Then the set of assertions in $\mathcal{N}$, seen as conjunctions of propositional literals, is unsatisfiable. By compactness, there exists a finite subset of these assertions that is also unsatisfiable, i.e., there is a finite subset $\mathcal{N}'$ of $\mathcal{N}$ that is also never enabled. Thus for any finite subset $\mathcal{M}'$ of $\mathcal{M}$, $\mathcal{M}' \Vdash_{\mathcal{N}'}$ as wanted.
Otherwise, there is at least one $\mathcal{J}$ enabling $\mathcal{N}$. By abuse of notation, we write $\mathcal{N}_A$ even if $A \subseteq \mathbf{A}$ is not an interpretation. For every interpretation $\mathcal{J}$ in which $\mathcal{N}$ is enabled, there exist by compactness of $\Vdash_F$ finite sets $\mathcal{J}' \subseteq \mathcal{J}, \mathcal{M}^\mathcal{J} \subseteq \mathcal{M}$, and $\mathcal{N}^\mathcal{J} \subseteq \mathcal{N}$ such that $\mathrm{fm}\ell(\mathcal{J}') \cup \mathcal{M}^\mathcal{J}_{\mathcal{J}'} \Vdash_{\mathcal{N}^\mathcal{J}} [\mathcal{N}^\mathcal{J}]$. Define $E = \{\perp \leftarrow \{-a\} \mid a \in A \text{ for some } C \leftarrow A \in \mathcal{N}\}$. Note that $\mathcal{J} \models E$ if and only if $\mathcal{N}$ is enabled in $\mathcal{J}$. This observation implies that the sets of propositional clauses $E$ and $\{\perp \leftarrow \mathcal{J}' \mid \mathcal{J} \text{ interpretation where } \mathcal{N} \text{ is enabled}\} \cup E$ are respectively propositionally satisfiable and propositionally unsatisfiable. By compactness, there exists a finite unsatisfiable subset $\{\perp \leftarrow \mathcal{J}'_1, \dots, \perp \leftarrow \mathcal{J}'_n\} \cup E'$ of the latter set.

Let $\mathcal{M}' = \bigcup_i \mathcal{M}^{\mathcal{J}_i}$ and $\mathcal{N}' = \bigcup_i \mathcal{N}^{\mathcal{J}_i} \cup \mathcal{N}''$ where $\mathcal{J}_i$ is any of the interpretations enabling $\mathcal{N}$ that is at the origin of the existence of this $\mathcal{J}'_i$ and $\mathcal{N}''$ is a finite subset of $\mathcal{N}$ such that all assertions in $E'$ also occur negated in $\mathcal{N}''$. Note that both $\mathcal{M}'$ and $\mathcal{N}'$ are finite sets. It now suffices to show $\mathcal{M}' \Vdash_{\mathcal{N}'} \mathcal{N}'$. Thus let $\mathcal{J}$ be an interpretation in which $\mathcal{N}'$ is enabled. Then $\mathcal{J} \models E'$ because all assertions in $E'$ also appear negated in $\mathcal{N}'' \subseteq \mathcal{N}'$. Thus, since $\{\perp \leftarrow \mathcal{J}'_1, \dots, \perp \leftarrow \mathcal{J}'_n\} \cup E'$ is unsatisfiable, there must exist an index $k$ such that $\mathcal{J} \not\models \perp \leftarrow \mathcal{J}'_k$, that is, $\mathcal{J}'_k \subseteq \mathcal{J}$. We have $\mathrm{fm}\ell(\mathcal{J}'_k) \cup \mathcal{M}^{\mathcal{J}_k}_{\mathcal{J}'_k} \Vdash_{\mathcal{N}^{\mathcal{J}_k}} [\mathcal{N}^{\mathcal{J}_k}]$ by construction, and thus $\mathrm{fm}\ell(\mathcal{J}) \cup \bigcup_i \mathcal{M}^{\mathcal{J}_i}_{\mathcal{J}} \Vdash \bigcup_i [\mathcal{N}^{\mathcal{J}_i}] \cup [\mathcal{N}^{''}]$ by (D3). $\square$

Given sets $M, N \subseteq \mathcal{P}(\mathbf{F})$, the expression $M \models N$ can refer to either the base consequence relation on $\mathcal{P}(\mathbf{F})$ or the lifted consequence relation on $\mathcal{P}(\mathbf{AF})$ (since $\mathbf{F} \subseteq \mathbf{AF}$). Fortunately, there is no ambiguity. First, let us show a preparatory lemma:

**Lemma 5** Let $\models$ be a consequence relation on $\mathbf{F}$, and $M, N \subseteq \mathbf{F}$. If $M' \models N'$ for all $M' \supseteq M$ and $N' \supseteq N$ such that $M' \cup N' = \mathbf{F}$, then $M \models N$.

*Proof* By contraposition, we assume that $M \not\models N$, and we need to find $M' \supseteq M$ and $N' \supseteq N$ such that $M' \cup N' = \mathbf{F}$ and $M' \not\models N'$. We apply Zorn's lemma to obtain a maximal element $(M', N')$ of the set $\{(M', N') \mid M \subseteq M', N \subseteq N' \text{ and } M' \not\models N'\}$ with the order $(M_1, N_1) \le (M_2, N_2)$ if and only if $M_1 \subseteq M_2$ and $N_1 \subseteq N_2$. Compactness of $\models$, together with (D3), guarantees that every chain in this set has an upper bound; for nonempty chains, this is the pairwise union of all the elements in the chain. It remains to show that $M' \cup N' = \mathbf{F}$. Assume to the contrary that $C \not\in M' \cup N'$ for some $C$. Due to the maximality of $(M', N')$, we necessarily have $M' \cup \{C\} \models N'$ and $M' \models N' \cup \{C\}$. Applying the cut rule for $\models$, we get $M' \models N'$, a contradiction. $\square$

**Lemma 6** The two versions of $\models$ coincide on $\mathbf{F}$-formulas, and similarly for $\Vdash$.

*Proof* The first property is obvious. For the second property, the argument is as follows. Let $M, N \subseteq \mathbf{F}$. Then we must show that $M \Vdash_F N$ if and only if $M \Vdash_{\mathbf{AF}} N$. First assume that $M \Vdash_F N$. Then clearly $\mathrm{fm}\ell(\mathcal{J}) \cup M \Vdash_F N$ for any $\mathcal{J}$ by (D3) and thus $M \Vdash_{\mathbf{AF}} N$. Assuming $M \Vdash_{\mathbf{AF}} N$, we show $M \Vdash_F N$ using Lemma 5. It thus suffices to show that $M' \Vdash_F N'$ for every $M' \supseteq M$ and $N' \supseteq N$ such that $M' \cup N' = \mathbf{F}$. Set $\mathcal{J} = \{v \mid \mathrm{fm}\ell(v) \in M'\} \cup \{-v \mid \mathrm{fm}\ell(v) \notin M'\}$. Then $\mathrm{fm}\ell(\mathcal{J}) \cup M \cup \sim N \subseteq M' \cup \sim N'$. By the assumption $M \Vdash_{\mathbf{AF}} N$ we have $\mathrm{fm}\ell(\mathcal{J}) \cup M \Vdash_F N$ and thus $M' \Vdash_F N'$ via (D3). $\square$

Aside from resolving ambiguity, Lemma 6 justifies the use of splitting in provers without compromising soundness or completeness: When we prove a completeness theorem that claims that a given prover derives $\perp$ from any initial $\models_{\mathbf{AF}}$-unsatisfiable set $M \subseteq \mathbf{AF}$, Lemma 6 allows us to conclude that it also derives $\perp$ when starting from any initial $\models_F$-unsatisfiable set $M \subseteq \mathbf{F}$.
Given a formula $C \in \mathbf{F}_{\sim}$, let $asn(C)$ denote the set of assertions $a \in \mathbf{A}$ such that $\{fml(a)\} \not\models \{C\}$. Normally, we would make sure that $asn(C)$ is nonempty for every formula $C$. Given $a \in asn(C)$, observe that if $a \in asn(D)$, then $\{C\} \not\models \{D\}$, and if $\neg a \in asn(D)$, then $\{C\} \models \{\sim D\}$.

**Remark 7** Our propositional interpretations are always total. We could also consider partial interpretations—that is, $\mathcal{J} \subseteq \mathbf{A}$ such that at most one of $v \in \mathcal{J}$ and $\neg v \in \mathcal{J}$ holds for every $v \in V$. But this is not necessary, because partial interpretations can be simulated by total ones: For every variable $v$ in the partial interpretation, we can use two variables $v^+$ and $v^-$ in the total interpretation and interpret $v^+$ as true if $v$ is true and $v^-$ as true if $v$ is false. By adding the propositional clause $\perp \leftarrow \{v^-, v^+\}$, every total model of the translated A-formulas corresponds to a partial model of the original A-formulas.

**Example 8** In the original description of AVATAR [28], the connection between first-order clauses and assertions takes the form of a function $[ ] : \mathbf{F} \to \mathbf{A}$. The encoding is such that $[\neg C] = \neg[C]$ for every ground unit clause $C$ and $[C] = [D]$ if and only if $C$ is syntactically equal to $D$ up to variable renaming. This can be supported in our framework by letting $fml(v) = C$ for some $C$ such that $[C] = v$, for every propositional variable $v$.

A different encoding is used to exploit the theories of an SMT solver [4]. With a notion of $\not\models$-entailment that gives a suitable meaning to Skolem symbols, we can go further and have $[\neg C(\mathrm{sk}_{-C(x)})] = \neg[C(x)]$. Even if the superposition prover considers $\mathrm{sk}_{-C(x)}$ an uninterpreted symbol (according to $\models$), the SAT or SMT solver can safely prune the search space by assuming that $C(x)$ and $\neg C(\mathrm{sk}_{-C(x)})$ are exhaustive (according to $\not\models$).

### 3 Splitting Calculi

Let $\mathbf{F}$ be a set of base formulas equipped with $\perp$, $\models$, and $\not\models$. The consequence relation $\not\models$ is assumed to be nontrivial: (D6) $\emptyset \not\models \emptyset$. Let $\mathbf{A}$ be a set of assertions over $\mathbf{V}$, and let $\mathbf{AF}$ be the set of A-formulas over $\mathbf{F}$ and $\mathbf{A}$. Let $(\mathit{FInf}, \mathit{FRed})$ be a base calculus for $\mathbf{F}$-formulas, where $\mathit{FRed}$ is a redundancy criterion that additionally satisfies

$$ (\mathbf{R5}) \quad \mathit{Inf}(\mathbf{F}, \mathit{Red}_{\mathbf{F}}(N)) \subseteq \mathit{Red}_{\mathbf{I}}(N) \text{ for every } N \subseteq \mathbf{F}; $$

$$ (\mathbf{R6}) \quad \perp \notin \mathit{FRed}_{\mathbf{F}}(N) \text{ for every } N \subseteq \mathbf{F}; $$

$$ (\mathbf{R7}) \quad C \in \mathit{FRed}_{\mathbf{F}}(\{\perp\}) \text{ for every } C \neq \perp. $$

These requirements can easily be met by a well-designed redundancy criterion. Requirement (R5) is called reducedness by Waldmann et al. [30, Sect. 2.3]. Requirement (R6) must hold of any complete calculus (Lemma 2), and (R7) can be made without loss of generality (Remark 3). Bachmair and Ganzinger's redundancy criterion for superposition [1, Sect. 4.3] meets (R1)–(R7).

From a base calculus, we will define an induced splitting calculus $(\mathit{SInf}, \mathit{SRed})$. We will show that the splitting calculus is sound w.r.t. $\not\models$ and that it is statically and dynamically complete w.r.t. $\models$. Furthermore, we will show two stronger results that take into account the switching of propositional models that characterizes most splitting architectures: strong static completeness and strong dynamic completeness.

#### 3.1 The Inference Rules

We start with the mandatory inference rules.
**Definition 9** The splitting inference system SInf consists of all instances of the following two rules:

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

$$ \frac{(\perp \leftarrow A_i)^n_{i=1}}{\perp} \text{UNSAT} $$

For BASE, the side condition is $(C_n, \dots, C_1, D) \in FInf$. For UNSAT, the side condition is that $\{\perp \leftarrow A_1, \dots, \perp \leftarrow A_n\}$ is propositionally unsatisfiable.

In addition, the following optional inference rules can be used if desired; the completeness proof does not depend on their application. Rules identified by double bars, such as SPLIT, are simplifications; they replace their premises with their conclusions in the current A-formula set. The premises' removal is justified by SRed<sub>F</sub>, defined in Sect. 3.2.

$$ \frac{C \leftarrow A}{\perp \leftarrow \{\neg a_1, \dots, \neg a_n\} \cup A \quad (C_i \leftarrow \{a_i\})^n_{i=1}} \text{SPLIT} $$

In the SPLIT rule, we require that $C \neq \perp$ is splittable into $C_1, \dots, C_n$ and that $a_i \in asn(C_i)$ for each $i$. A formula $C$ is splittable into formulas $C_1, \dots, C_n$ if $n \ge 2$, $\{C\} \models \{C_1, \dots, C_n\}$ and $C \in FRed_F(\{C_i\})$ for each $i$.

SPLIT performs an n-way case analysis on $C$. Each case $C_i$ is approximated by an assertion $a_i$. The first conclusion expresses that the cases are exhaustive. The n other conclusions assume $C_i$ if its approximation $a_i$ is true.

In a clausal prover, typically $C = C_1 \lor \dots \lor C_n$, where the subclauses $C_i$ have mutually disjoint sets of variables and form a maximal split. For example, the clause $p(x) \lor q(x)$ is not splittable because of the shared variable $x$, whereas $p(x) \lor q(y)$ can be split into $\{p(x), q(y)\}$.

$$ \frac{(\perp \leftarrow A_i)^n_{i=1}}{(\perp \leftarrow A_i)^n_{i=1}} \text{COLLECT} $$

$$ \frac{(\perp \leftarrow A_i)^n_{i=1}}{(\perp \leftarrow A_i)^n_{i=1}} \frac{C \leftarrow A \cup B}{C \leftarrow B} \text{TRIM} $$

For COLLECT, we require $C \neq \perp$ and $\{\perp \leftarrow A_i\}^n_{i=1} \models \{\perp \leftarrow A\}$. For TRIM, we require $C \neq \perp$ and $\{\perp \leftarrow A_i\}^n_{i=1} \cup \{\perp \leftarrow A\} \models \{\perp \leftarrow B\}$.

COLLECT removes A-formulas whose assertions cannot be satisfied by any model of the propositional clauses—a form of garbage collection. Similarly, TRIM removes assertions that are entailed by existing propositional clauses.

$$ \frac{(\perp \leftarrow A_i)^n_{i=1}}{\perp} \text{STRONGUNSAT} $$

$$ \frac{C \leftarrow A}{\perp \leftarrow \{\neg a\} \cup A} \text{APPROX} $$

$$ \frac{\text{TAUTO}}{C \leftarrow A} $$

For STRONGUNSAT, we require $\{\perp \leftarrow A_i\}^n_{i=1} \models \{\perp\}$. For APPROX, we require $a \in asn(C)$. For TAUTO, we require $\models \{C \leftarrow A\}$.

STRONGUNSAT is a variant of UNSAT that uses $\models$ instead of $|=$. A splitting prover may choose to apply STRONGUNSAT if desired, but only UNSAT is necessary for completeness. In practice, $|=$-entailment can be much more expensive to decide, or even be undecidable. A splitting prover could invoke an SMT solver [4] ($|=$) with a time limit, falling back on a SAT solver ($|=$) if necessary.

APPROX can be used to make any derived A-formula visible to $|=$. It is similar to a one-way split. TAUTO, which asserts a $|=$-tautology, allows communication in the other direction, from the SMT or SAT solver to the calculus.
**Example 10** Suppose the base calculus is first-order resolution [2] and the initial clauses are $\neg p(a), \neg q(z,z)$, and $p(x) \lor q(y,b)$, as in Sect. 1. SPLIT replaces the last clause by $\bot \leftarrow \{\neg v_0, \neg v_1\}$, $p(x) \leftarrow \{v_0\}$, and $q(y,b) \leftarrow \{v_1\}$. Two BASE inferences then generate $\bot \leftarrow \{v_0\}$ and $\bot \leftarrow \{v_1\}$. Finally, UNSAT generates $\bot$.

**Example 11** Consider a splitting calculus obeying the AVATAR conventions of Example 8. When splitting on $C(x) \vee D(y)$, after closing the $C(x)$ case, we can assume that $C(x)$ does not hold when considering the $D(y)$ case. This can be achieved by adding the A-clause $\neg C(\text{sk}_{C(x)}) \leftarrow \{\neg[C(x)]\}$ using TAUTO. If we use an SMT solver that is strong enough to determine that $\neg C(\text{sk}_{C(x)})$ and $D(y)$ are inconsistent, we can then apply STRONGUNSAT immediately, skipping the $D(y)$ branch altogether. This would be the case if we took $C(x) := f(x)>0$ and $D(y) := f(y)>3$ with a solver that supports linear arithmetic and quantifiers. We are not aware of any prover that implements this idea, although a similar idea is described for ground $C(x)$ in the context of labeled splitting [13, Sect. 2].

**Example 12** Consider a splitting calculus whose propositional solver is an SMT solver supporting linear arithmetic. Suppose that we are given the inconsistent clause set $\{c > 0, c < 0\}$. Two applications of APPROX make these clauses visible to the SMT solver, as the propositional clause set $\{\bot \leftarrow \neg(c > 0), \bot \leftarrow \neg(c < 0)\}$. Then the SMT solver, modeled by STRONGUNSAT, detects the unsatisfiability.

The splitting inference system commutes nicely with the enabled projection:

**Lemma 13** ($\mathbf{SInf}(\mathcal{N})_\mathcal{J} = \mathbf{FInf}(\mathcal{N}_\mathcal{J})$) if $\bot \notin \mathcal{N}_\mathcal{J}$.

*Proof* The condition $\bot \notin \mathcal{N}_\mathcal{J}$ rules out the UNSAT inferences. It remains to show that the enabled projection of a BASE inference is an $\mathbf{FInf}$-inference from enabled premises, and vice versa. $\square$

**Theorem 14 (Soundness)** The rules UNSAT, SPLIT, COLLECT, TRIM, STRONGUNSAT, APPROX, and TAUTO are sound w.r.t. $\models$. Moreover, if every rule in $\mathbf{FInf}$ is sound w.r.t. $\models$ (on $\mathcal{P}(\mathbf{F})$), then the rule BASE is sound w.r.t. $\models$ (on $\mathcal{P}(\mathbf{AF})$).

*Proof* CASES UNSAT, STRONGUNSAT, TAUTO: Trivial.

**CASE SPLIT:** For the left conclusion, by definition of $\models$, it suffices to show $\mathbf{fml}(\mathcal{J}) \cup \{C\} \models \{\bot\}$ for every $\mathcal{J} \supseteq A \cup \{-a_1, \dots, \neg a_n\}$. By the side condition $\{C\} \models \{C_1, \dots, C_n\}$, it suffices in turn to show $\mathbf{fml}(\mathcal{J}) \cup \{C_i\} \models \{\bot\}$ for every $i$. Notice that $\sim C_i \in \mathbf{fml}(\mathcal{J})$. The entailment amounts to $(\mathbf{fml}(\mathcal{J}) \setminus \{\sim C_i\}) \cup \{C_i\} \models \{C_i\}$, which follows from (D2) and (D3).

For the right conclusions, we must show $\mathbf{fml}(\mathcal{J}) \cup \{C \leftarrow A\}_\mathcal{J} \models \{C_i\}$ for every $\mathcal{J} \supseteq \{a_i\}$. Notice that $C_i \in \mathbf{fml}(\mathcal{J})$. The desired result follows from (D2) and (D3).

**CASE COLLECT:** We must show $\{\bot \leftarrow A_i\}_{i=1}^n \models \{C \leftarrow A\}$. This follows from the stronger side condition $\{\bot \leftarrow A_i\}_{i=1}^n \models \{\bot \leftarrow A\}$.

**CASE TRIM:** Only the right conclusion is nontrivial. Let $\mathcal{N} = \{\bot \leftarrow A_i\}_{i=1}^n$. It suffices to show $\mathcal{N}_\mathcal{J} \cup \{C \leftarrow A\}_\mathcal{J} \models \{C\}$ for every $\mathcal{J} \supseteq B$. Assume $\mathcal{J} \models \mathcal{N}_\mathcal{J} \cup \{C \leftarrow A\}_\mathcal{J}$. By the side condition $\mathcal{N} \cup \{\bot \leftarrow A\} \models \{\bot \leftarrow B\}$, we get $\mathcal{N}_\mathcal{J} \cup \{\bot \leftarrow A\}_\mathcal{J} \models \{\bot\}$, meaning that either $\mathcal{N}_\mathcal{J} \models \{\bot\}$ or $\mathcal{J} \supseteq A$. The first case is trivial. In the other case, $\mathcal{J} \models \mathcal{N}_\mathcal{J} \cup \{C\}$ and thus $\mathcal{J} \models \{C\}$, as required.

**CASE APPROX:** The proof is as for the left conclusion of SPLIT.

**CASE BASE:** To show $\{C_i \leftarrow A_i\}_{i=1}^n \models \{D \leftarrow A_1 \cup \dots \cup A_n\}$, by the definition of $\models$ on $\mathcal{P}(\mathbf{AF})$, it suffices to show $\{C_1, \dots, C_n\} \models \{D\}$. This follows from the soundness of the inferences in $\mathbf{FInf}$. $\square$
## 3.2 The Redundancy Criterion

Next, we lift the base redundancy criterion.

**Definition 15** The splitting redundancy criterion $SRed = (SRed_1, SRed_F)$ is specified as follows. An A-formula $C \leftarrow A \in AF$ is redundant w.r.t. $\mathcal{N}$, written $C \leftarrow A \in SRed_F(\mathcal{N})$, if either of these conditions is met:

(1) $C \in FRed_F(\mathcal{N}_\mathcal{J})$ for every propositional interpretation $\mathcal{J} \supseteq A$; or

(2) there exists an A-formula $C \leftarrow B \in \mathcal{N}$ such that $B \subset A$.

An inference $\iota \in SInf$ is redundant w.r.t. $\mathcal{N}$, written $\iota \in SRed_1(\mathcal{N})$, if either of these conditions is met:

(3) $\iota$ is a BASE inference and $\{\iota\}_\mathcal{J} \subseteq FRed_1(\mathcal{N}_\mathcal{J})$ for every $\mathcal{J}$; or

(4) $\iota$ is an UNSAT inference and $\perp \in \mathcal{N}$.

Condition (1) lifts $FRed_F$ to A-formulas. It is used both as such and to justify the SPLIT and COLLECT rules, as we will see below. Condition (2) is used to justify TRIM. We will use $SRed_F$ to justify global A-formula deletion, but also $FRed_F$ for local A-formula deletion in the locking prover. Note that $SRed$ is not reduced. Inference redundancy partly commutes with the enabled projection:

**Lemma 16** $(SRed_1(\mathcal{N}))_\mathcal{J} \subseteq FRed_1(\mathcal{N}_\mathcal{J})$ if $\perp \notin \mathcal{N}$.

*Proof* Since $\perp \notin \mathcal{N}$, condition (4) of the definition of $SRed_1$ cannot apply. The inclusion then follows directly from condition (3) applied to the interpretation $\mathcal{J}$. $\square$

**Lemma 17** $\perp \notin SRed_F(\mathcal{N})$ for every $\mathcal{N} \subseteq AF$.

*Proof* By Lemma 2, condition (1) of the definition of $SRed_F$ cannot apply. Nor can condition (2). $\square$

**Lemma 18** $SRed$ is a redundancy criterion.

*Proof* We will first show that the restriction $ARed$ of $SRed$ to BASE inferences is a redundancy criterion. Then we will consider UNSAT inferences.

We start by showing that $ARed$ is a special case of the redundancy criterion $FRed^{(\mathcal{G}, \sqsupset)}$ of Waldmann et al. [29, Sect. 3]—the intersection of lifted redundancy criteria with tiebreaker orders. Then we can simply invoke Theorem 37 and Lemma 19 from their technical report [30].

To strengthen the redundancy criterion, we define a tiebreaker order $\sqsupset$ such that $C \leftarrow A \sqsupset D \leftarrow B$ if and only if $C = D$ and $A \subset B$. In this way, $C \leftarrow B$ is redundant w.r.t. $C \leftarrow A$ if $A \subset B$, even though the base clause is the same. The only requirement on $\sqsupset$ is that it must be well founded, which is the case since the assertion sets of A-formulas are finite. We also define a family of grounding functions $\mathcal{G}_\mathcal{J}$ indexed by a propositional model $\mathcal{J}$. Here, “grounding” will mean enabled projection. For A-formulas $\mathcal{C}$, we set $\mathcal{G}_\mathcal{J}(\mathcal{C}) = \{\mathcal{C}\}_\mathcal{J}$. For inferences $\iota$, we set $\mathcal{G}_\mathcal{J}(\iota) = \{\iota\}_\mathcal{J}$.

We must show that $\mathcal{G}_\mathcal{J}$ satisfies the following characteristic properties of grounding function: (G1) $\mathcal{G}_\mathcal{J}(\perp) = \{\perp\}$; (G2) for every $\mathcal{C} \in AF$, if $\perp \in \mathcal{G}_\mathcal{J}(\mathcal{C})$, then $\mathcal{C} = \perp$; and (G3) for every $\iota \in SInf$, $\mathcal{G}_\mathcal{J}(\iota) \subseteq FRed_1(\mathcal{G}_\mathcal{J}(concl(\iota)))$.

Condition (G1) obviously holds, and (G3) holds by property (R4) of $FRed$. However, (G2) does not hold, a counterexample being $\perp \leftarrow \{a\}$. On closer inspection, Waldmann
et al. use (G2) only to prove static completeness (Theorems 27 and 45 in their technical report) but not to establish that $FRed^{\sqcap, \sqsuperscript{\mathcal{G}}}$ is a redundancy criterion, so we can proceed. It is a routine exercise to check that ARed coincides with $FRed^{\sqcap, \sqsuperscript{\mathcal{G}}}(FRed_{\mathcal{F}}^{\sqcap, \sqsuperscript{\mathcal{G}}})$, which is defined as follows:

1. $\iota \in FRed_{\mathcal{I}}^{\sqcap}(\mathcal{N})$ if and only if for every propositional interpretation $\mathcal{J}$, we have $\mathcal{G}_{\mathcal{J}}(\iota) \subseteq FRed_{\mathcal{I}}(\mathcal{G}_{\mathcal{J}}(\mathcal{N}))$;

2. $\mathcal{C} \in FRed_{\mathcal{F}}^{\sqcap, \sqsuperscript{\mathcal{G}}}(\mathcal{N})$ if and only if for every propositional interpretation $\mathcal{J}$ and every $\mathcal{D} \in \mathcal{G}_{\mathcal{J}}(\mathcal{C})$, either $\mathcal{D} \in FRed_{\mathcal{F}}(\mathcal{G}_{\mathcal{J}}(\mathcal{N}))$ or there exists $\mathcal{C}' \in \mathcal{N}$ such that $\mathcal{C}' \sqsubseteq \mathcal{C}$ and $\mathcal{D} \in \mathcal{G}_{\mathcal{J}}(\mathcal{C}')$.

We also need to check that the consequence relation $\models$ used in SRed coincides with the consequence relation $\models_{\sqcap}$, which is defined as $\mathcal{M} \models_{\sqcap} \{\mathcal{C}\}$ if and only if for every $\mathcal{J}$ and $\mathcal{D} \in \mathcal{G}_{\mathcal{J}}(\{\mathcal{C}\})$, we have $\mathcal{G}_{\mathcal{J}}(\mathcal{M}) \models \{\mathcal{D}\}$. After expanding $\mathcal{G}_{\mathcal{J}}$, this is exactly the definition we used for lifting $\models$ to AF.

To extend the above result to SRed, we must show the second half of conditions (R2) and (R3) as well as (R4) for UNSAT inferences.

(R2) Given an UNSAT inference $\iota$, we must show that if $\mathcal{M} \subseteq \mathcal{N}$ and $\iota \in SRed_{\mathcal{I}}(\mathcal{M})$, then $\iota \in SRed_{\mathcal{I}}(\mathcal{N})$. This holds because if $\perp \in \mathcal{M}$, then $\perp \in \mathcal{N}$.

(R3) Given an UNSAT inference $\iota$, we must show that if $\mathcal{M} \subseteq SRed_{\mathcal{F}}(\mathcal{N})$ and $\iota \in SRed_{\mathcal{I}}(\mathcal{N})$, then $\iota \in SRed_{\mathcal{I}}(\mathcal{N} \setminus \mathcal{M})$. This amounts to proving that if $\perp \in \mathcal{N}$, then $\perp \in \mathcal{N} \setminus \mathcal{M}$, which follows from Lemma 17.

(R4) Given an UNSAT inference $\iota$, we must show that if $\perp \in \mathcal{N}$, then $\iota \in SRed_{\mathcal{I}}(\mathcal{N})$. This follows from the definition of $SRed_{\mathcal{I}}$. $\square$

SRed is highly versatile. It can justify the deletion of A-formulas that are propositionally tautological, such as $C \leftarrow \{v, \neg v\}$. It lifts the base redundancy criterion gracefully: If $D \in FRed_{\mathcal{F}}(\{C_i\}_{i=1}^n)$, then $D \leftarrow A_1 \cup \dots \cup A_n \in SRed_{\mathcal{F}}(\{C_i \leftarrow A_i\}_{i=1}^n)$. It also allows other simplifications, as long as the assertions on A-formulas used to simplify a given $C \leftarrow A$ are contained in A. If the base criterion $FRed_{\mathcal{F}}$ supports subsumption (e.g., following the lines of Waldmann et al. [29]), this also extends to A-formulas: $D \leftarrow B \in SRed_{\mathcal{F}}(\{C \leftarrow A\})$ if $D$ is strictly subsumed by C and $B \supseteq A$, or if $C = D$ and $B \supset A$. Finally, it is strong enough to justify case splits and the other simplification rules presented in Sect. 3.1.

**Theorem 19 (Simplification)** For every SPLIT, COLLECT, or TRIM inference, the conclusions collectively make the premises redundant according to $SRed_{\mathcal{F}}$.

*Proof CASE SPLIT:* We must show $C \leftarrow A \in SRed_{\mathcal{F}}(\{\perp \leftarrow \neg a_1, \dots, \neg a_n\} \cup A) \cup \{C_i \leftarrow \{a_i\}_{i=1}^n\}$. By condition (1) of the definition of $SRed_{\mathcal{F}}$, it suffices to show $C \in FRed_{\mathcal{F}}(\{\perp \leftarrow \neg a_1, \dots, \neg a_n\} \cup (\{C_i \leftarrow \{a_i\}_{i=1}^n\}) \cup \{\mathcal{J} \supseteq A\})$ for every $\mathcal{J} \supseteq A$. If $a_i \in \mathcal{J}$ for some $i$, this follows from SPLIT's side condition $C \in FRed_{\mathcal{F}}(\{C_i\})$. Otherwise, this follows from (R7), the requirement that $C \in FRed_{\mathcal{F}}(\{\perp\})$, since $C \neq \perp$.

**CASE COLLECT:** We must show $C \leftarrow A \in SRed_{\mathcal{F}}(\{\perp \leftarrow A_i\}_{i=1}^n)$. By condition (1) of the definition of $SRed_{\mathcal{F}}$, it suffices to show $C \in FRed_{\mathcal{F}}((\{\perp \leftarrow A_i\}_{i=1}^n) \cup \{\mathcal{J} \supseteq A\})$ for every $\mathcal{J} \supseteq A$. If $A_i \subseteq \mathcal{J}$ for some $i$, this follows from COLLECT's side condition that $C \neq \perp$ and (R7). Otherwise, from the side condition $\{\perp \leftarrow A_i\}_{i=1}^n \models \{\perp \leftarrow A\}$, we obtain $\emptyset \models \{\perp\}$, which contradicts (D6).

**CASE TRIM:** We must show $C \leftarrow A \cup B \in SRed_{\mathcal{F}}(\{\perp \leftarrow A_i\}_{i=1}^n \cup \{C \leftarrow B\})$. This follows directly from condition (2) of the definition of $SRed_{\mathcal{F}}$. $\square$
Annoyingly, the redundancy criterion SRed does not mesh well with $\alpha$-equivalence. We would expect the A-formula $p(x) \leftarrow \{a\}$ to be subsumed by $p(y) \leftarrow \emptyset$, where x, y are variables, but this is not covered by condition (2) of SRed$_F$ because $p(x) \neq p(y)$. The simplest solution is to take F to be the quotient of some set of raw formulas by $\alpha$-equivalence. An alternative is to generalize the theory so that the projection operator $\mathcal{G}_{\emptyset}$ generates entire $\alpha$-equivalence classes (e.g., $\mathcal{G}_{\emptyset}(\{p(x)\}) = \{p(x), p(y), p(z), \dots\}$) or groundings (e.g., $\mathcal{G}_{\emptyset}(\{p(x)\}) = \{p(a), p(f(a)), \dots\}$). Waldmann et al. describe the second approach [29, Sect. 4].

### 3.3 Standard Saturation

We will now prove that the splitting calculus is statically complete and therefore dynamically complete. Unfortunately, derivations produced by most practical splitting architectures violate the fairness condition associated with dynamic completeness. Nevertheless, the standard completeness notions are useful stepping stones, so we start with them.

**Lemma 20** Let $\mathcal{N} \subseteq \mathbf{AF}$ be an A-formula set, and let $\mathcal{J}$ be a propositional interpretation. If $\mathcal{N}$ is saturated w.r.t. $\mathbf{SInf}$ and $\mathbf{SRed}_1$, then $\mathcal{N}_{\mathcal{J}}$ is saturated w.r.t. $\mathbf{FInf}$ and $\mathbf{FRed}_1$.

*Proof* Assuming $\iota \in \mathbf{FInf}(\mathcal{N}_{\mathcal{J}})$, we must show $\iota \in \mathbf{FRed}_1(\mathcal{N}_{\mathcal{J}})$. The argument follows that of the “folklore” Lemma 26 in the technical report of Waldmann et al. [30]. First note that any inference in $\mathbf{FInf}$ is lifted, via BASE, in $\mathbf{SInf}$, so that we have $\iota \in (\mathbf{SInf}(\mathcal{N}))_{\mathcal{J}}$. This means that there exists a BASE inference $\iota_0 \in \mathbf{SInf}(\mathcal{N})$. By saturation of $\mathcal{N}$, we have $\iota_0 \in \mathbf{SRed}_1(\mathcal{N})$. By definition of $\mathbf{SRed}_1$, $\{\iota_0\}_{\mathcal{J}} = \{\iota\} \subseteq \mathbf{FRed}_1(\mathcal{N}_{\mathcal{J}})$, as required. $\square$

**Theorem 21** (Static completeness) Assume $(\mathbf{FInf}, \mathbf{FRed})$ is statically complete. Then $(\mathbf{SInf}, \mathbf{SRed})$ is statically complete.

*Proof* Suppose $\mathcal{N} \subseteq \mathbf{AF}$, $\mathcal{N} \models \{\perp\}$, and $\mathcal{N}$ is saturated w.r.t. $\mathbf{SInf}$ and $\mathbf{SRed}_1$. We will show $\perp \in \mathcal{N}$.

First, we show $\perp \in \mathcal{N}_{\mathcal{J}}$ for every $\mathcal{J}$. From $\mathcal{N} \models \{\perp\}$, by the definition of $\models$ on A-formulas, it follows that $\mathcal{N}_{\mathcal{J}} \models \{\perp\}$. Moreover, by Lemma 20, $\mathcal{N}_{\mathcal{J}}$ is saturated w.r.t. $\mathbf{FInf}$ and $\mathbf{FRed}_1$. By static completeness of $(\mathbf{FInf}, \mathbf{FRed})$, we get $\perp \in \mathcal{N}_{\mathcal{J}}$.

Hence $\mathcal{N}_{\perp}$ is propositionally unsatisfiable. By compactness of propositional logic, there exists a finite subset $\mathcal{M} \subseteq \mathcal{N}_{\perp}$ such that $\mathcal{M} \models \{\perp\}$. By saturation w.r.t. UNSAT, we obtain $\perp \in \mathcal{N}$, as required. $\square$

Thanks to the requirements on the redundancy criterion, we obtain dynamic completeness as a corollary:

**Corollary 22** (Dynamic completeness) Assume $(\mathbf{FInf}, \mathbf{FRed})$ is statically complete. Then $(\mathbf{SInf}, \mathbf{SRed})$ is dynamically complete.

*Proof* This immediately follows from Theorem 21 by Lemma 6 in the technical report of Waldmann et al. [30]. $\square$
### 3.4 Local Saturation

The above completeness result, about ▷<sub>SRed<sub>F</sub></sub>-derivations, can be extended to prover designs based on the given clause procedure, such as the Otter, DISCOUNT, and Zipperposition loops, as explained by Waldmann et al. [29, Sect. 4]. But it fails to capture a crucial aspect of most splitting architectures. Since ▷<sub>SRed<sub>F</sub></sub>-derivations have no notion of current split branch or propositional model, they place no restrictions on which inferences may be performed when.

To fully capture splitting, we need to start with a weaker notion of saturation. If an A-formula set is consistent, it should suffice to saturate w.r.t. a single propositional model. In other words, if no A-formula ⊥ ← A such that A ⊆ J is derivable for some model J ⊨ N<sub>⊥</sub>, the prover will never be able to apply the UNSAT rule to derive ⊥. It should then be allowed to deliver a verdict of “consistent.” We will call such model-specific saturations local and standard saturations global.

**Definition 23** A set N ⊆ AF is locally saturated w.r.t. SInf and SRed<sub>1</sub> if either ⊥ ∈ N or there exists a propositional model J ⊨ N<sub>⊥</sub> such that N<sub>J</sub> is saturated w.r.t. FInf and FRed<sub>1</sub>.

Local saturation works in tandem with strong static completeness:

**Theorem 24 (Strong static completeness)** Assume (FInf, FRed) is statically complete. Given a set N ⊆ AF that is locally saturated w.r.t. SInf and SRed<sub>1</sub> and such that N ⊨ {⊥}, we have ⊥ ∈ N.

*Proof* We show ⊥ ∈ N by case analysis on the condition by which N is locally saturated. The first case is vacuous. Otherwise, let J ⊨ N<sub>⊥</sub>. Since N ⊨ {⊥}, we have N<sub>J</sub> ⊨ {⊥}. By the definition of local saturation and static completeness of (FInf, FRed), we get ⊥ ∈ N<sub>J</sub>, contradicting J ⊨ N<sub>⊥</sub>. □

**Example 25** Consider the following A-clause set expressed using AVATAR conventions:

$$ \{\bot \leftarrow \neg[p(x)], \neg[q(y)]\}, \quad p(x) \leftarrow \{[p(x)]\}, \quad q(y) \leftarrow \{[q(y)]\}, \quad \neg q(a) \} $$

It is not globally saturated for resolution, because the conclusion ⊥ ← {[q(y)]} of resolving the last two A-clauses is missing, but it is locally saturated with J ⊇ {[p(x)], [q(y)]} as the witness in Definition 23.

We also need a notion of local fairness that works in tandem with local saturation.

**Definition 26** A sequence (N<sub>i</sub>)<sub>i</sub> of sets of A-formulas is locally fair w.r.t. SInf and SRed<sub>1</sub> if either ⊥ ∈ N<sub>i</sub> for some i or there exists a propositional model J ⊨ (N<sub>∞</sub>)⊥ such that FInf((N<sub>∞</sub>)<sub>J</sub>) ⊆ ⋃<sub>i</sub> FRed<sub>1</sub>((N<sub>i</sub>)<sub>J</sub>).

**Lemma 27** Let (N<sub>i</sub>)<sub>i</sub> be a ▷<sub>SRed<sub>F</sub></sub>-derivation that is locally fair w.r.t. SInf and SRed<sub>1</sub>. Then the limit inferior N<sub>∞</sub> is locally saturated w.r.t. SInf and SRed<sub>1</sub>.

*Proof* The proof is by case analysis on the condition by which (N<sub>i</sub>)<sub>i</sub> is locally fair. If ⊥ ∈ N<sub>i</sub>, then ⊥ ∈ N<sub>∞</sub> by Lemma 17, and N<sub>∞</sub> is therefore locally saturated. In the remaining case, we have N<sub>i</sub> ⊆ N<sub>∞</sub> ∪ SRed<sub>F</sub>(N<sub>∞</sub>) by Lemma 4 in the technical report of Waldmann et al. [30], and therefore ⋃<sub>i</sub> FRed<sub>1</sub>((N<sub>i</sub>)<sub>J</sub>) ⊆ ⋃<sub>i</sub> FRed<sub>1</sub>((N<sub>∞</sub>)<sub>J</sub> ∪ FRed<sub>F</sub>((N<sub>∞</sub>)<sub>J</sub>)) = ⋃<sub>i</sub> FRed<sub>1</sub>((N<sub>∞</sub>)<sub>J</sub>) because we clearly have (SRed<sub>F</sub>(N<sub>∞</sub>))<sub>J</sub> ⊆ FRed<sub>F</sub>((N<sub>∞</sub>)<sub>J</sub>) ∪ (N<sub>∞</sub>)<sub>J</sub>. □
the soundness of the individual inferences. Similarly, $\mathcal{M}$ and $\mathcal{M}'$ will usually be enabled in $\mathcal{J}$, but we do not require this.

The interpretation $\mathcal{J}$ should be a model of $\mathcal{N}_\perp$ most of the time; when it is not, SWITCH can be used to switch interpretation or STRONG UNSAT to finish the refutation. Although the condition $\mathcal{J}_i \models (\mathcal{N}_i)_\perp$ might be violated for some $i$, to make progress we must periodically check it and apply SWITCH as needed. Much of the work that is performed while the condition is violated will likely be wasted. To avoid this waste, Vampire invokes the SAT solver whenever it selects a clause as part of the given clause procedure.

Transitions can be combined to form $\Rightarrow_{MG}$-derivations (pronounced “arrow-MG-derivations”).

**Lemma 29** If $(\mathcal{J}, \mathcal{N}) \Rightarrow_{MG} (\mathcal{J}', \mathcal{N}')$, then $\mathcal{N} \succcurlyeq_{SRed_F} \mathcal{N}'$.

*Proof* The only rule that deletes A-formulas, DERIVE, exclusively takes out A-formulas that are redundant w.r.t. the next state, as mandated by $\succcurlyeq_{SRed_F}$. $\square$

To develop our intuitions, we will study several examples of $\Rightarrow_{MG}$-derivations. In all the examples in this section, the base calculus is first-order resolution, and $\models$ is entailment for first-order logic with equality.

**Example 30** Let us revisit Example 10. Initially, the propositional interpretation is $\mathcal{J}_0 = \{\neg v_0, \neg v_1\}$. After the split, we have the A-clauses $\neg p(a), \neg q(z, z), p(x) \leftarrow \{v_0\}, q(y, b) \leftarrow \{v_1\}$, and $\perp \leftarrow \{\neg v_0, \neg v_1\}$. The natural option is to switch interpretation. We take $\mathcal{J}_1 = \{v_0, \neg v_1\}$. We then derive $\perp \leftarrow \{v_0\}$. Since $\mathcal{J}_1 \not\models \perp \leftarrow \{v_0\}$, we switch to $\mathcal{J}_2 = \{\neg v_0, v_1\}$, where we derive $\perp \leftarrow \{v_1\}$. Finally, we detect that the propositional clauses are unsatisfiable and generate $\perp$. This corresponds to the transitions below, where arrows are annotated by transition names and light gray boxes identify enabled A-clauses:

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

## 4.2 Fairness

We need a fairness criterion for MG that implies local fairness of the underlying $\succcurlyeq_{SRed_F}$-derivation. The latter requires a witness $\mathcal{J}$ but gives us no hint as to where to look for one. This is where basic topology comes into play.

**Definition 31** A propositional interpretation $\mathcal{J}$ is a *limit point* in a sequence $(\mathcal{J}_i)_i$ if there exists a subsequence $(\mathcal{J}'_i)_i$ of $(\mathcal{J}_i)_i$ such that $\mathcal{J} = \mathcal{J}'_\infty = \mathcal{J}^\infty$.
<figure><img src="image_3.png" /><figcaption>**Fig. 1:** A split tree with a single infinite branch</figcaption></figure>

<caption>**Fig. 2:** A split tree with two infinite branches</caption>

Intuitively, a limit point is a propositional interpretation that is the limit of a family of interpretations that we revisit infinitely often. We will see that there always exists a limit point. To achieve fairness, we will focus on saturating a limit point.

**Example 32** Let $(\mathcal{J}_i)_i$ be the sequence such that $\mathcal{J}_{2i} \cap \mathbf{V} = \{v_1, v_3, \dots, v_{2i-1}\}$ (i.e., $v_1, v_3, \dots, v_{2i-1}$ are true and the other variables are false) and $\mathcal{J}_{2i+1} = (\mathcal{J}_{2i} \setminus \{\neg v_{2i}\}) \cup \{v_{2i}\}$. Although it is not in the sequence, the interpretation $\mathcal{J} \cap \mathbf{V} = \{v_1, v_3, \dots\}$ is a limit point. The split tree of $(\mathcal{J}_i)_i$ is depicted in Fig. 1. The direct path from the root to a node labeled $\mathcal{J}_i$ specifies the assertions that are true in $\mathcal{J}_i$. The limit point $\mathcal{J}$ corresponds to the only infinite branch of the tree.

The above example hints at why the proof of MG's dynamic completeness is nontrivial: Some derivations might involve infinitely many split branches, making it difficult for the prover to focus on any single one and saturate it.

**Example 33** A sequence may have multiple limit points. Let $(\mathcal{J}_i)_i$ be the sequence such that $\mathcal{J}_0 \cap \mathbf{V} = \emptyset$, $\mathcal{J}_{4i+1} \cap \mathbf{V} = \{v_0\} \cup \{v_{4j+3} \mid j < i\}$, $\mathcal{J}_{4i+2} \cap \mathbf{V} = \{v_0, v_{4i+2}\} \cup \{v_{4j+3} \mid j < i\}$, $\mathcal{J}_{4i+3} \cap \mathbf{V} = \{v_{4j+1} \mid j \le i\}$, and $\mathcal{J}_{4i+4} \cap \mathbf{V} = \{v_{4j+1} \mid j \le i\} \cup \{v_{4i+4}\}$. This sequence has two limit points: $\mathcal{J}' = \liminf_{i \to \infty} \mathcal{J}_{4i+1}$ and $\mathcal{J}'' = \liminf_{i \to \infty} \mathcal{J}_{4i+3}$. The split tree is depicted in Fig. 2.

**Lemma 34** Let $(\mathcal{J}_i)_i$ be a sequence of propositional interpretations. Then $\mathcal{J}_\infty \subseteq \mathcal{J} \subseteq \mathcal{J}^\infty$ for all of its limit points $\mathcal{J}$.

*Proof* By definition of limit point, there must exist a subsequence $(\mathcal{J}_i')_i$ of $(\mathcal{J}_i)_i$ such that $\mathcal{J}^\prime_\infty = \mathcal{J}^\prime_\infty = \mathcal{J}$. It is obvious by definition that the limit inferior of a subsequence must be a superset of the limit inferior of the original sequence, and analogously that the limit superior of a subsequence must be a subset of the limit superior of the original sequence. $\square$

**Lemma 35** Every sequence $(\mathcal{J}_i)_i$ of propositional interpretations has at least one limit point.

*Proof* The set of propositional interpretations is homeomorphic to the set of functions $\mathbf{V} \to \{0, 1\}$ equipped with the product topology. Since $\mathbf{V}$ is countable, this set of functions is a compact metric space—namely, the Cantor space. In a compact metric space, every sequence has a convergent subsequence, and thus a limit point in our notation. $\square$

We can nearly as easily supply an elementary proof:
**Proof** We construct a subsequence $(J'_j)_j$ converging to a limit point $J$ in such a way that $J'_j$ gets the first $j$ variables right—i.e., such that $J'_j \models v_k$ if and only if $J \models v_k$ for every $k \le j$. Moreover, we maintain the invariant that there are infinitely many elements in the sequence $(J_i)_i$ that agree with this finite prefix. Assume that we have already defined $J'_0, \dots, J'_j$. Among the infinitely many elements $J_i$ that agree with $J'_0, \dots, J'_j$ on $v_1, \dots, v_j$, there must be infinitely many with $J_i \models v_{j+1}$ or infinitely many with $J_i \models \neg v_{j+1}$. In the first case, set $J'_{j+1} = J_i$ for one such index $i$, and analogously in the second case. $\square$

Lemma 35 tells us that every sequence has a limit point. No matter how erratically the prover switches branches, it will systematically explore at least one branch in a limit point. It then suffices to perform the base *Finf*-inferences fairly in that branch:

**Definition 36** An $\Rightarrow_{MG}$-derivation $(\mathcal{J}_i, \mathcal{N}_i)_i$ is fair if either (1) $\perp \in \mathcal{N}_i$ for some $i$ or (2) $\mathcal{J}_i \models (\mathcal{N}_i)_{\perp}$ for infinitely many indices $i$ and there exists a limit point $\mathcal{J}$ of $(\mathcal{J}_i)_i$ such that $\text{Finf}((\mathcal{N}_{\infty})_{\mathcal{J}}) \subseteq \bigcup_i \text{FRed}_1((\mathcal{N}_i)_{\mathcal{J}})$.

Until $\perp$ is derived, it is impossible in a fair $\Rightarrow_{MG}$-derivation to delay SWITCH forever (by the first half of (2)) or to starve off DERIVE by performing only SWITCH transitions (by the second half of (2)). Also note that we make no assumptions about the order in which propositional models are enumerated; the propositional solver is given carte blanche.

We might at first expect that a realistic prover would ensure the inclusion $\text{Finf}((\mathcal{N}_{\infty})_{\mathcal{J}}) \subseteq \bigcup_i \text{FRed}_1((\mathcal{N}_i)_{\mathcal{J}})$ for all limit points $\mathcal{J}$. However, a prover like Vampire, based on the given-clause procedure with an age-based heuristic, might saturate only one of the limit points, as we will see in Sect. 6.2.

Fairness of $\Rightarrow_{MG}$-derivations is deliberately defined in terms of $\text{FRed}_1$ instead of $\text{SRed}_1$. This results in a more suitable notion of fairness, since it allows the prover to ignore formulas and inferences that are locally redundant at the limit point but not redundant w.r.t. $(\text{SInf}, \text{SRed})$. For example, the inference $(t \approx s, p(t), p(s))$ is locally redundant in $\mathcal{J} \supseteq \{v_0\}$ if the A-clause $p(s) \leftarrow \{v_0\}$ has already been derived, but it is not redundant w.r.t. $(\text{SInf}, \text{SRed})$.

**Lemma 37** Let $(\mathcal{J}_i, \mathcal{N}_i)_i$ be an $\Rightarrow_{MG}$-derivation such that $\mathcal{J}_i \models (\mathcal{N}_i)_{\perp}$ for infinitely many indices $i$. Then for every $\mathcal{D} \in (\mathcal{N}_{\infty})_{\perp}$, there exists an index $i$ such that $\mathcal{J}_j \models \{\mathcal{D}\}$ for every $j \ge i$.

**Proof** Let $\mathcal{D} = \perp \leftarrow A \in (\mathcal{N}_{\infty})_{\perp}$. Then $\perp \leftarrow A \in \mathcal{N}_k$ for some $k$. For every $j \ge k$, we then have $\perp \leftarrow B \in \mathcal{N}_j$ for some $B \subseteq A$, since every $\Rightarrow_{MG}$-derivation is a $\Delta_{SRed_F}$-derivation and $\perp \leftarrow A$ can only become redundant due to such a $\perp \leftarrow B$. Since $\{\perp \leftarrow B\} \models \{\perp \leftarrow A\}$, we get $(\mathcal{N}_j)_{\perp} \models \{\perp \leftarrow A\}$ for every $j \ge k$. By the assumption, there exists an index $i \ge k$ such that $\mathcal{J}_i \models \{\perp \leftarrow A\}$. For $j \ge i$, the interpretation changes only in the SWITCH transition, which has $\mathcal{J}_j \models (\mathcal{N}_j)_{\perp}$ as a side condition. Since $(\mathcal{N}_j)_{\perp} \models \{\perp \leftarrow A\}$, we have $\mathcal{J}_j \models \{\perp \leftarrow A\}$ for every $j \ge i$. $\square$

**Lemma 38** Let $(\mathcal{J}_i, \mathcal{N}_i)_i$ be an $\Rightarrow_{MG}$-derivation such that $\mathcal{J}_i \models (\mathcal{N}_i)_{\perp}$ for infinitely many indices $i$, and let $\mathcal{J}$ be a limit point of $(\mathcal{J}_i)_i$. Then $\mathcal{J} \models (\mathcal{N}_{\infty})_{\perp}$.

**Proof** Let $\mathcal{C} \in (\mathcal{N}_{\infty})_{\perp}$. By Lemma 37, there exists an index $i$ such that $\mathcal{J}_j \models \{\mathcal{C}\}$ for every $j \ge i$. Let $(\mathcal{J}'_i)_i$ be the subsequence associated with the limit point $\mathcal{J}$. Then there also exists an index $i'$ such that $\mathcal{J}'_j \models \{\mathcal{C}\}$ for every $j \ge i'$ and hence $\mathcal{J} \models \{\mathcal{C}\}$. $\square$

In the spirit of refinement, we have that fairness of an $\Rightarrow_{MG}$-derivation implies local fairness of the underlying $\Delta_{SRed_F}$-derivation:
**Theorem 39 (Fairness)** Let $(\mathcal{J}_i, \mathcal{N}_i)_i$ be a fair $\implies_{\text{MG}}$-derivation. Then $(\mathcal{N}_i)_i$ is a $\triangleright_{\text{SRed}_F}$-derivation that is locally fair w.r.t. $\text{SInf}$ and $\text{SRed}_1$.

*Proof* The case where $\perp \in \mathcal{N}_i$ for some $i$ is trivial. Otherwise, we have that $\mathcal{J}_i \models (\mathcal{N}_i)_\perp$ for infinitely many $i$ and there is a limit point $\mathcal{J}$ such that $\text{Finf}((\mathcal{N}_\infty)_\mathcal{J}) \subseteq \bigcup_i \text{FRed}_1((\mathcal{N}_i)_\mathcal{J})$. We take this limit point as the witness for $\mathcal{J}$ in Definition 26. It remains to show that $\mathcal{J} \models (\mathcal{N}_\infty)_\perp$. This follows from Lemma 38. □

**Corollary 40 (Dynamic completeness)** Assume $(\text{Finf}, \text{FRed})$ is statically complete. Given a fair $\implies_{\text{MG}}$-derivation $(\mathcal{J}_i, \mathcal{N}_i)_i$ such that $\mathcal{N}_0 \models \{\perp\}$, we have $\perp \in \mathcal{N}_i$ for some $i$.

*Proof* By Theorem 28. □

A well-behaved propositional solver, as in labeled splitting, enumerates potential models in a systematic way and always gives rise to a single limit point $\mathcal{J}_\infty$, which can be taken for $\mathcal{J}$ in the definition of fairness (Definition 36). To achieve this kind of fairness, a splitting prover would perform all inferences from persistently enabled A-formulas—that is, A-formulas that eventually become enabled and remain enabled forever. In a prover based on the given clause procedure, this can be implemented in the standard way, using an age-based selection heuristic [27, Sect. 4]. However, such a strategy is not sufficient if the prover exploits local redundancy, as we will see in Sects. 5 and 7.2, even if the propositional solver is well behaved.

By contrast, an unconstrained solver, as supported by AVATAR, can produce multiple limit points; in particular, the restart feature of SAT solvers [20] could produce this kind of behavior. Then it is more challenging to ensure fairness, as we will see in Sect. 6.

**Example 41** Suppose that we leave out $\neg q(z, z)$ from the initial clause set of Example 10. Then we can still derive $\perp \leftarrow \{v_0\}$, as in Example 30, but not $\perp \leftarrow \{v_1\}$. By static completeness of the splitting calculus, we conclude that the A-clause set is consistent.

**Example 42** Consider the initial clause set consisting of $p(x) \lor q(a)$ and $\neg q(y) \lor q(f(y))$. Without splitting, and without selection [2, Sect. 3], a resolution prover would diverge attempting to generate infinitely many clauses of the form $p(x) \lor q(f^i(a))$.

By contrast, in a splitting prover, we might split the first clause, yielding the A-clauses $p(x) \leftarrow \{v_0\}$, $q(a) \leftarrow \{v_1\}$, and $\perp \leftarrow \{\neg v_0, \neg v_1\}$. If we then choose the model $\{v_1\}$ and commit to it, we will also diverge, although somewhat faster since we do not need to carry around the literal $p(x)$. On the other hand, if we at any point switch to $\{v_0\}$, we notice that $\{p(x)\}$ is saturated and terminate. This illustrates the benefits of employing an unconstrained SAT solver.

**Example 43** It is crucial to invoke the SAT solver often enough—in other words, to take `SWITCH` and `STRONGUNSAT` transitions periodically. Suppose that the inconsistent initial clause set of Example 10 is supplemented by the prolific but unhelpful clauses $r(a)$ and $\neg r(x) \lor r(f(x))$. We can perform the same split as before, but if we ignore the fairness condition that $\mathcal{J}_i \models (\mathcal{N}_i)_\perp$ must hold infinitely often, we can stick to the interpretation $\{\neg v_1, \neg v_2\}$ and derive useless consequences of the form $r(f^i(a))$ forever, thereby failing to generate $\perp$. Similarly, the SAT solver must be invoked eventually after deriving a propositional clause $\perp \leftarrow A$ that conflicts with the current interpretation.

**Example 44** Consider the consistent set consisting of $\neg p(x)$, $p(a) \lor q(a)$, and $\neg q(y) \lor p(f(y)) \lor q(f(y))$. Splitting the second clause into $p(a)$ and $q(a)$ and resolving $q(a)$ with the third clause yields $p(f(a)) \lor q(f(a))$. This process can be iterated to yield arbitrarily many
applications of f. Now suppose that $v_{2i}$ and $v_{2i+1}$ are associated with $p(f^i(a))$ and $q(f^i(a))$, respectively. If we split every emerging clause $p(f^i(a)) \lor q(f^i(a))$ and the SAT solver always makes $v_{2i}$ true before $v_{2i+1}$, we end up with the situation of Example 32 and Fig. 1. For the limit point $\mathcal{J}$, all *Finf*-inferences are performed. Thus, the derivation is fair.

**Example 45** We build a clause set from two copies of Example 44, where each clause C from each copy $i \in \{1,2\}$ is extended to $\neg r_i \lor C$. We add the clause $r_1 \lor r_2$ and split it as our first move. From there, each branch imitates Example 44. A SAT solver might jump back and forth between them, as in Example 33 and Fig. 2. Even if the A-clauses get disabled and re-enabled infinitely often, we must select them eventually and perform all nonredundant inferences in at least one of the two limit points ($\mathcal{J}'$ or $\mathcal{J}''$).

# 5 Locking Provers

With both AVATAR and labeled splitting, an enabled A-clause can be redundant locally, w.r.t. the current interpretation, and yet nonredundant globally. Both architectures provide mechanisms to temporarily lock away such A-clauses and unlock them when coming back to an interpretation where they are no longer locally redundant. In AVATAR, conditionally deleted A-clauses are stored in the locked set; in labeled splitting, they are stored in the split stack. We will refine the model-guided prover into a locking prover that captures these mechanisms.

## 5.1 The Transition Rules

The states of a locking derivation are triples $(\mathcal{J}, \mathcal{N}, \mathcal{L})$, where $\mathcal{J}$ is a propositional interpretation, $\mathcal{N} \subseteq \mathbf{AF}$ is a set of A-formulas, and $\mathcal{L} \subseteq \mathcal{P}_{\text{fin}}(\mathbf{A}) \times \mathbf{AF}$ is a set of pairs of finite assertion sets and A-formulas. Intuitively, $(B, C \leftarrow A) \in \mathcal{L}$ means that $C \leftarrow A$ is “locally redundant” in all interpretations $\mathcal{J} \supseteq B$. The function $\llbracket \rrbracket$ erases the locks: $\llbracket \mathcal{L} \rrbracket = \{\mathcal{C} \mid (B, \mathcal{C}) \in \mathcal{L} \text{ for some } B\}$. Initial states have the form $(\mathcal{J}, N, \emptyset)$, where $N \subseteq \mathbf{F}$. The *locking prover* is defined by two transition rules:

**LIFT** $(\mathcal{J}, \mathcal{N}, \mathcal{L}) \Rightarrow_L (\mathcal{J}', \mathcal{N}' \cup \llbracket \mathcal{U} \rrbracket, \mathcal{L} \setminus \mathcal{U})$ if $(\mathcal{J}, \mathcal{N}) \Rightarrow_{\text{MG}} (\mathcal{J}', \mathcal{N}')$ and $\mathcal{U} = \{(B, C \leftarrow A) \in \mathcal{L} \mid B \not\subseteq \mathcal{J}' \text{ and } A \subseteq \mathcal{J}'\}$

**LOCK** $(\mathcal{J}, \mathcal{N} \uplus \{C \leftarrow A\}, \mathcal{L}) \Rightarrow_L (\mathcal{J}, \mathcal{N}, \mathcal{L} \cup \{(B, C \leftarrow A)\})$ if $B \subseteq \mathcal{J}$ and $C \in \text{FRed}_F(\mathcal{N}_{\mathcal{J}'})$ for every $\mathcal{J}' \supseteq A \cup B$

The LIFT rule performs an $\Rightarrow_{\text{MG}}$-transition and unlocks any A-formulas that are no longer locally redundant. The LOCK rule can be used to lock A-formulas that are locally redundant.

**Lemma 46** Let $(\mathcal{J}_i, \mathcal{N}_i, \mathcal{L}_i)_i$ be an $\Rightarrow_L$-derivation. Then $(\mathcal{J}_i, \mathcal{N}_i \cup \llbracket \mathcal{L}_i \rrbracket)_i$ is an $\Rightarrow_{\text{MG}}$-derivation.

*Proof* Every LIFT transition clearly corresponds to an MG transition. Every LOCK transition corresponds to a DERIVE transition with $\mathcal{M} = \mathcal{M}' = \emptyset$. $\square$
**Example 47** Let $\mathcal{J}_0 = \{\neg v_0\}$ and $\mathcal{J}_1 = \{v_0\}$. The following derivation based on first-order resolution illustrates the locking and unlocking of an A-clause:

$$
\begin{align*}
& (\mathcal{J}_0, \{\neg \mathbf{p}(a), \mathbf{p}(x) \leftarrow \{\neg v_0\}, \mathbf{p}(a)\}, \emptyset) \\
\Rightarrow &_{\text{LOCK}} (\mathcal{J}_0, \{\neg \mathbf{p}(a), \mathbf{p}(x) \leftarrow \{\neg v_0\}\}, \{((\neg v_0), \mathbf{p}(a))\}) \\
\Rightarrow &_{\text{LIFT}} (\mathcal{J}_0, \{\neg \mathbf{p}(a), \mathbf{p}(x) \leftarrow \{\neg v_0\}, \perp \leftarrow \{\neg v_0\}\}, \{((\neg v_0), \mathbf{p}(a))\}) \\
\Rightarrow &_{\text{LIFT}} (\mathcal{J}_1, \{\neg \mathbf{p}(a), \mathbf{p}(x) \leftarrow \{\neg v_0\}, \perp \leftarrow \{\neg v_0\}, \mathbf{p}(a)\}, \emptyset) \\
\Rightarrow &_{\text{LIFT}} (\mathcal{J}_1, \{\neg \mathbf{p}(a), \mathbf{p}(x) \leftarrow \{\neg v_0\}, \perp \leftarrow \{\neg v_0\}, \mathbf{p}(a), \perp\}, \emptyset)
\end{align*}
$$

Gray boxes indicate enabled unlocked clauses. We first put a lock on $p(a)$, because it is “locally subsumed” by $p(x) \leftarrow \{\neg v_0\}$ in $\mathcal{J}_0$. Once we switch to $\mathcal{J}_1$, the lock is released, and we can use $p(a)$ to conclude the refutation.

There are three things to note. First, if we had simply thrown away the clause $p(a)$ instead of locking it, we would have lost refutability. Second, it would have been advantageous not to lock $p(a)$ at all and to use it immediately to derive $\perp$; however, it is not difficult to come up with examples where locking actually helps, which is why AVATAR includes this mechanism. Third, although the derivation shows only “local subsumption,” it could easily be changed to perform “local simplification”—e.g., demodulation from an equation $s \approx t \leftarrow A$.

## 5.2 Counterexamples

Locking can cause incompleteness, because an A-formula can be locally redundant at every point in the derivation and yet not be so at any limit point, thereby breaking local saturation. For example, if we have derived $p(x) \leftarrow \{\neg v_k\}$ for every $k$, then $p(c)$ is locally redundant in any interpretation $\mathcal{J}$ that contains $\neg v_k$. If the sequence of interpretations is given by $\mathcal{J}_i = \{v_0, \dots, v_{i-1}, \neg v_i, \neg v_{i+1}, \dots\}$, the clause $p(c)$ would always be locally redundant and never be considered for inferences. Yet $p(c)$ might not be locally redundant at the unique limit point $\mathcal{J} = \mathbf{V}$.

**Example 48** Consider the inconsistent initial clause set

$$
\{ \begin{array}{l} \mathbf{t}(a), \quad \neg \mathbf{t}(x) \lor \mathbf{t}(\mathbf{f}(x)), \quad \neg \mathbf{t}(x) \lor \neg \mathbf{s}(x) \lor \neg \mathbf{r}(x, y) \lor \mathbf{q}(y), \\ \neg \mathbf{p}(c), \quad \neg \mathbf{q}(c), \quad \mathbf{r}(x, y), \quad \neg \mathbf{r}(x, y) \lor \neg \mathbf{r}(x, z) \lor \mathbf{q}(x) \lor \mathbf{p}(x) \end{array} \}
$$

and ordered resolution with selection as the calculus. Assume that the selection function always chooses the maximal negative literals w.r.t. the precedence $p \prec q \prec r \prec s \prec t$. Let $fml(v_i) = \neg \mathbf{r}(\mathbf{f}^i(a), x) \lor \mathbf{q}(x)$ and $fml(w_i) = \neg \mathbf{s}(\mathbf{f}^i(a))$, and let $v_i$ and $w_i$ be false in the initial model for all $i$. Following an age-based selection heuristic and maximal splitting, the second clause the prover derives is $\neg \mathbf{s}(a) \lor \neg \mathbf{r}(a, y) \lor \mathbf{q}(y)$, which it splits into $\neg \mathbf{s}(a) \leftarrow \{w_0\}$ and $\neg \mathbf{r}(a, y) \lor \mathbf{q}(y) \leftarrow \{v_0\}$. The s predicate's role is purely to ensure that this clause is split and that the assertion $v_0$ is introduced. The prover later also derives $\mathbf{q}(x) \lor \mathbf{p}(x)$ and $\mathbf{q}(y) \leftarrow \{v_0\}$ and switches to a model in which $v_i$ is true if and only if $i = 0$. The first of the two clauses is clearly locally redundant, so LOCK applies, and $((\{v_0\}, \mathbf{q}(x) \lor \mathbf{p}(x))$ is added to $\mathcal{L}$.

Next, $\mathbf{q}(y) \leftarrow \{v_1\}$ is derived, before $\mathbf{q}(y) \leftarrow \{v_0\}$ is selected for inferences. Eventually, that latter clause can be used together with $\neg \mathbf{q}(c)$ to derive $\perp \leftarrow \{v_0\}$. The prover then switches to a new model in which $v_i$ is true if and only if $i = 1$. The clause $\mathbf{q}(x) \lor \mathbf{p}(x)$ can immediately be relocked. This process can be repeated indefinitely. The clause $\mathbf{q}(x) \lor \mathbf{p}(x)$, which is necessary for a refutation (together with $\neg \mathbf{p}(c)$ and $\neg \mathbf{q}(c)$), is ignored because it is always locally redundant. It is locked each time the prover selects an A-clause for inferences, due to a different A-clause. But it is not locally redundant at the limit point $\mathcal{J} = \neg \mathbf{V}$.
In the derivation in Example 48, locking is not applied exhaustively: The A-clause $\neg r(f^i(a), y) \lor q(y) \leftarrow \{v_j\}$ is not locked, even though $q(y) \leftarrow \{v_j\}$ has already been derived. This situation is unrealistic and would not happen in Vampire. We could hope that is enough for completeness to forbid such anomalous scenarios. However, this is not the case, as we can see from a more complicated example:

**Example 49** The calculus is ordered resolution with selection using the precedence $p \prec q_1 \prec q_2 \prec r_1 \prec r_2 \prec s \prec t_1 \prec t_2 \prec u$, selecting nothing if the clause is of the form $\neg u(\dots) \lor u(\dots)$ and otherwise selecting the maximal negative literals.

The initial clauses are as follows. First, we have a splittable clause $q_1(x) \lor q_2(y)$. Then we have clauses $u(a, y)$ and $\neg u(x, y) \lor u(f(x), y)$. We will use the predicate symbol $u$ to delay the selection of a clause in an age-based selection heuristic, by adding a literal $\neg u(f^j(x), y)$ to the clause. Moreover, we have the clause $s(x, y)$. We can prevent splitting by adding the literal $\neg s(x, y)$ to a clause. Finally, we add the following clauses:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \neg u(f(y), x) \lor r_1(x) \lor \neg q_1(x) & \neg u(f(y), x) \lor \neg r_1(x) & \neg t_1(x) \lor \neg s(x, y) \lor \neg p(x) \lor r_1(y) \\ \neg u(f(y), x) \lor r_2(x) \lor \neg q_2(x) & \neg u(f(y), x) \lor \neg r_2(x) & \neg t_2(x) \lor \neg s(x, y) \lor \neg p(x) \lor r_2(y) \\ t_1(a) & t_2(f(a)) & \neg t_1(x) \lor t_1(f(f(x))) \\ & & \neg t_2(x) \lor t_2(f(f(x))) \end{array} $$

The initial clause set is clearly inconsistent. Yet we will sketch an infinite derivation that corresponds to an age-based selection heuristic and that does not derive $\perp$. First, we split $q_1(x) \lor q_2(y)$ into $q_1(x) \leftarrow \{x_1\}$ and $q_2(x) \leftarrow \{x_2\}$, where the assertion denotations are as follows:

$$ \begin{array}{l@{\qquad}l} fml(w_{2i}) = \neg s(f^{2i}(a), x) \lor r_1(x) & fml(v_i) = \neg p(f^i(a)) \\ fml(w_{2i+1}) = \neg s(f^{2i+1}(a), x) \lor r_2(x) & fml(x_i) = q_i(x) \end{array} $$

The derivation uses the following sequence of interpretations $\mathcal{J}_i$:

- $\mathcal{J}_i \models v_j$ if and only if $j < i$;

- $\mathcal{J}_i \models w_j$ if and only if $j \in \{i, i+1\}$;

- $\mathcal{J}_i \models x_1$ if and only if $i$ is even;

- $\mathcal{J}_i \models x_2$ if and only if $i$ is odd.

The derivation thus alternates between two families of interpretations, with even and odd indices, giving rise to two limit points.

After the clause $q_1(x) \lor q_2(y)$ is split, the prover is in the model $\mathcal{J}_0$ and derives the clauses $\neg u(y, x) \lor r_1(x) \lor \neg q_1(x)$, $\neg u(y, x) \lor r_2(x) \lor \neg q_2(x)$, $\neg s(a, y) \lor r_1(y) \lor \neg p(a)$. The last clause is split into $\neg s(a, y) \lor r_1(y) \leftarrow \{w_0\}$, $\neg p(a) \leftarrow \{v_0\}$, and $\perp \leftarrow \{\neg v_0, \neg w_0\}$. Then an analogous split happens with $r_2$ instead of $r_1$. After a few more inferences, we derive $r_1(x) \lor \neg q_1(x)$ and then $r_1(y) \leftarrow \{w_0\}$, which makes $r_1(x) \lor \neg q_1(x)$ locally redundant (and analogously for $r_2$ in place of $r_1$). Once $r_1(y) \leftarrow \{w_0\}$ is picked as the given clause, the prover derives $\perp \leftarrow \{w_0\}$ and switches to the next model $\mathcal{J}_1$.

In the first family, $\mathcal{J}_{2i}$, the clause $\neg q_1(x) \lor r_1(x)$ is always locally redundant due to $r_1(x) \leftarrow \{w_{2i}\}$, and is locked with the assertion $w_{2i}$. Similarly, $\neg q_2(x) \lor r_2(x)$ is locally redundant in the second family, $\mathcal{J}_{2i+1}$, with the assertion $w_{2i+1}$. In both cases we can already lock each of the clauses while the prover is still in the previous model ($\mathcal{J}_{2i-1}$ and $\mathcal{J}_{2i}$, respectively).

The clause $\neg q_2(x) \lor r_2(x)$ is thus only ever unlocked in interpretations $\mathcal{J}_{2i}$. In those interpretations, $q_2(x) \leftarrow \{x_2\}$ is disabled and hence no inferences can be performed with $\neg q_2(x) \lor r_2(x)$. The same holds mutatis mutandis for $\neg q_1(x) \lor r_1(x)$, which is unlocked only
when no inferences can be performed with it. As a result, the derivation never performs inferences with $q_1(x) \leftarrow \{x_1\}$ or $q_2(x) \leftarrow \{x_2\}$. Removing these A-clauses makes the set satisfiable; thus, by soundness, the derivation cannot contain $\perp$.

Given the right sequence of propositional interpretations returned by the SAT solver, the derivation in Example 49 could potentially happen in a prover such as Vampire. It is difficult to exclude that the SAT solver used by Vampire could produce this sequence, or generally to characterize the sequence of models produced by SAT solvers in such a concrete way. This derivation is also strongly fair—every inference that is possible infinitely often, perhaps intermittently, is eventually made redundant. Thus strong fairness is not a sufficient criterion for completeness either.

## 5.3 Fairness

Our solution to the issues encountered above is as follows. Let $(\mathcal{J}_i, \mathcal{N}_i, \mathcal{L}_i)_i$ be an $\implies_L$-derivation. Given a subsequence $(\mathcal{J}'_j)_j$ of $(\mathcal{J}_i)_i$, let $(\mathcal{N}'_j)_j$ be the corresponding subsequence of $(\mathcal{N}_i)_i$. To achieve fairness, we now consider $\mathcal{N}'_\infty$, the A-formulas persistent in the subsequence $(\mathcal{N}'_j)_j$. By contrast, with no A-formulas locked away, fairness of $\implies_{\text{MG}}$-derivations could use $\mathcal{N}'_\infty$.

**Definition 50** An $\implies_L$-derivation $(\mathcal{J}_i, \mathcal{N}_i, \mathcal{L}_i)_i$ is fair if (A) $\mathcal{L}_0 = \emptyset$ and (B) either (1) $\perp \in \bigcup_i \mathcal{N}_i$ or (2) $\mathcal{J}_i \models (\mathcal{N}_i)_\perp$ for infinitely many indices $i$ and there exists a subsequence $(\mathcal{J}'_j)_j$ converging to a limit point $\mathcal{J}$ such that $\text{Finf}((\mathcal{N}'_\infty)_\mathcal{J} \cup (\limsup_{j \to \infty} \|\mathcal{L}'_j\|)_\mathcal{J} \setminus \|\mathcal{L}^{\text{f}\infty}\|)_\mathcal{J}) \subseteq \bigcup_i \text{FRed}_1((\mathcal{N}_i \cup \|\mathcal{L}_i\|)_\mathcal{J})$, where $(\mathcal{N}'_j)_j$ and $(\mathcal{L}'_j)_j$ correspond to $(\mathcal{J}'_j)_j$.

Fairness of an $\implies_L$-derivation implies fairness of the corresponding $\implies_{\text{MG}}$-derivation. The condition on the sets $\mathcal{L}'_j$ ensures that inferences from A-formulas that are locked infinitely often, but not infinitely often with the same lock, are redundant at the limit point. In particular, if we know that each A-formula is locked at most finitely often, then $\limsup_{j \to \infty} \|\mathcal{L}'_j\| = \|\mathcal{L}^{\text{f}\infty}\|$ and the inclusion in the definition above simplifies to $\text{Finf}((\mathcal{N}'_\infty)_\mathcal{J}) \subseteq \bigcup_i \text{FRed}_1((\mathcal{N}_i \cup \|\mathcal{L}_i\|)_\mathcal{J})$.

**Theorem 51 (Fairness)** Let $(\mathcal{J}_i, \mathcal{N}_i, \mathcal{L}_i)_i$ be a fair $\implies_L$-derivation. Then $(\mathcal{J}_i, \mathcal{N}_i \cup \|\mathcal{L}_i\|)_i$ is a fair $\implies_{\text{MG}}$-derivation.

*Proof* We already showed that $(\mathcal{J}_i, \mathcal{N}_i, \mathcal{L}_i)_i$ is an $\implies_{\text{MG}}$-derivation in Lemma 46. It remains to show fairness. If the $\implies_L$-derivation is fair by case (1) of Definition 50, we apply case (1) of Definition 36 to show that the $\implies_{\text{MG}}$-derivation is fair. Otherwise, from case (2) of Definition 50, we retrieve a limit point $\mathcal{J}$. We will show, for that limit point, case (2) of Definition 36:

$$ \text{Finf}((\liminf_{i \to \infty} \mathcal{N}_i \cup \|\mathcal{L}_i\|)_\mathcal{J}) \subseteq \bigcup_i \text{FRed}_1((\mathcal{N}_i \cup \|\mathcal{L}_i\|)_\mathcal{J}) $$

Assume (a) $i \in \text{Finf}((\liminf_{j \to \infty} \mathcal{N}_j \cup \|\mathcal{L}_j\|)_\mathcal{J})$. By the definition of fairness of $\implies_L$-derivations, if all of $i$'s premises belong to $(\mathcal{N}'_\infty)_\mathcal{J} \cup ((\limsup_{j \to \infty} \|\mathcal{L}'_j\|)_\mathcal{J} \setminus (\|\mathcal{L}^{\text{f}\infty}\|)_\mathcal{J})$, then $i$ is redundant. Otherwise, we have that (b) one of $i$'s premises, $C$, is not in that set; that is, $C \notin (\mathcal{N}'_\infty)_\mathcal{J}$ and either $C \notin (\limsup_{j \to \infty} \|\mathcal{L}'_j\|)_\mathcal{J}$ or $C \in (\|\mathcal{L}^{\text{f}\infty}\|)_\mathcal{J}$.

By (a) we have that $C \leftarrow A \in \liminf_{j \to \infty} \mathcal{N}_j \cup \|\mathcal{L}_j\| \subseteq \liminf_{j \to \infty} \mathcal{N}'_j \cup \|\mathcal{L}'_j\|$ for some $A \subseteq \mathcal{J}$. Since $C \notin (\mathcal{N}'_\infty)_\mathcal{J}$ by (b), $C \leftarrow A$ cannot be persistent in $(\mathcal{N}'_j)_j$ and hence must
occur infinitely often in the sequence ($\|\mathcal{L}'_j\|$)$_j$. Thus $C \in (\limsup_{j \to \infty} \|\mathcal{L}'_j\|)\mathcal{J}$ and therefore
$C \in (\|\mathcal{L}^{\text{f}\infty}\|)\mathcal{J}$ by (b).

Hence $(B, C \leftarrow A') \in \mathcal{L}'^{\text{f}\infty}$ for some $A' \subseteq \mathcal{J}$ and B. If $(B, C \leftarrow A') \in \mathcal{L}'_j$ for some $j$, then necessarily $B \subseteq \mathcal{J}'_j$ due to the side conditions of the $\Rightarrow_L$-transitions. Since this is true for infinitely many indices $j$, we also have $B \subseteq \mathcal{J}^{\text{f}\infty} = \mathcal{J}$, and thus $C \in \mathcal{F}Red((\mathcal{N}_i)\mathcal{J})$ for some $i$ by the side condition of the LOCK transition. Therefore, by reducedness of $\mathcal{F}Red$, the inference $t$ is redundant. $\square$

**Corollary 52 (Dynamic completeness)** Assume $(\mathcal{F}Inf, \mathcal{F}Red)$ is statically complete. Given a fair $\Rightarrow_L$-derivation $(\mathcal{J}_i, \mathcal{N}_i, \mathcal{L}_i)_i$ such that $\mathcal{N}_0 \models \{\perp\}$, we have $\perp \in \mathcal{N}_i$ for some $i$.

*Proof* By Theorems 28 and 39. $\square$

# 6 AVATAR-Based Provers

AVATAR was unveiled in 2014 by Voronkov [28], although it was reportedly present in
Vampire already in 2012. Since then, he and his colleagues studied many options and
extensions [4,22]. At least two reimplementations exist, in Ebner's *super* tactic for Lean [12]
and in the Drodi prover by Oscar Contreras. Here we attempt to capture AVATAR's essence.

We will define an abstract AVATAR-based prover that extends the locking prover L with
a given clause procedure [17, Sect. 2.3]. A-formulas are moved in turn from the passive to
the active set, where inferences are performed. The heuristic for choosing the next given
A-formula to move is guided by timestamps indicating when the A-formulas were derived, to
ensure fairness.

## 6.1 The Transition Rules

Let **TAF** = **AF** × N be the set of timestamped A-formulas. (We will often omit the adjective “timestamped.”) Given a subset **N** ⊆ **TAF**, we define ⌈**N**⌈ = {C | (C, t) ∈ **N** for some t} and overload existing notations to erase timestamps as necessary. Accordingly, ⌈**N**⌈ = ⌈**N**⌈⌈, **N**⊥ = ⌈**N**⌈⊥, and **N**<sub>θ</sub> = ⌈**N**⌈<sub>θ</sub>. Note that we use a new set of calligraphic letters (e.g., C, **N**) to range over timestamped A-formulas and timestamped A-formula sets. We say that **N** is enabled in θ if and only if ⌈**N**⌈ is enabled in θ. We also define ⌈(*C*<sub>1</sub>,..., *C*<sub>n</sub>, *D*)⌈ = ( ⌈*C*<sub>1</sub>⌈,..., ⌈*C*<sub>n</sub>⌈, ⌈*D*⌈) for **TAF**-inferences *t*.

Using the saturation framework [29, Sect. 3], we lift a calculus (*SInf*, *SRed*) on **AF** to a
calculus (*TSInf*, *TSRed*) on **TAF** with the tiebreaker order < on timestamps. The tiebreaker is
used to strengthen redundancy, so that if the same A-formula appears but with two different
timestamps, the more recent version is considered redundant. In other words, if an A-formula
appears with two timestamps, the later version is redundant. Note that *TSRed* is in general
not reduced. Traditionally, provers use the active or passive status as tiebreaker: An active
clause may subsume a passive copy of itself, but not the other way around. Timestamps are
more fine-grained.

**Lemma 53** Let $\mathcal{N} \subseteq \mathbf{AF}$, $\mathcal{C} \in \mathbf{AF}$, and $t, k \in \mathbb{N}$. Then:

1. $\mathcal{L}\mathcal{T}\mathcal{S}\mathit{Inf}(\mathcal{N})\mathcal{I} = \mathcal{S}\mathit{Inf}(\mathcal{L}(\mathcal{N})\mathcal{I})$;

2. $\mathcal{L}\mathcal{T}\mathcal{S}\mathit{Red}_1(\mathcal{N})\mathcal{I} = \mathcal{S}\mathit{Red}_1(\mathcal{L}(\mathcal{N})\mathcal{I})$;

3. $\mathcal{L}\mathcal{T}\mathcal{S}\mathit{Red}_F(\mathcal{N})\mathcal{I} \supseteq \mathcal{S}\mathit{Red}_F(\mathcal{L}(\mathcal{N})\mathcal{I})$; and
4. $(\mathscr{C}, t+k) \in \text{TSRed}_F(\{(\mathscr{C}, t)\}) \text{ if } k > 0.$

*Proof* This follows directly from the definition in Waldmann et al. [29]. □

A state is a tuple $(\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q}, \mathcal{L})$ consisting of a propositional interpretation $\mathcal{J}$, a set of enabled nonpropositional active A-formulas $\mathcal{A} \subseteq \mathbf{TAF}$, a set of enabled nonpropositional passive A-formulas $\mathcal{P} \subseteq \mathbf{TAF}$, a set of A-formulas $\mathcal{Q} \subseteq \mathbf{TAF}$ that are either disabled in $\mathcal{J}$ or propositional clauses, and a set of locked A-formulas $\mathcal{L} \subseteq \mathcal{P}_{\text{fin}}(\mathbf{A}) \times \mathbf{TAF}$ such that

$$ (1) \quad \mathcal{A}_{\perp} = \mathcal{P}_{\perp} = \emptyset; $$

$$ (2) \quad \mathcal{A} \cup \mathcal{P} \text{ is enabled in } \mathcal{J}; $$

$$ (3) \quad \mathcal{Q}_{\mathcal{J}} \subseteq \{\perp\}. $$

Whenever we write a tuple $(\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q}, \mathcal{L})$, we assume that it satisfies all these invariants. For every $\mathcal{L} \subseteq \mathbf{A} \times \mathbf{TAF}$, we define $\mathcal{L}\mathcal{J} = \{(B, \mathcal{C}\mathcal{J}) \mid (B, \mathcal{C}) \in \mathcal{L}\} \subseteq \mathbf{A} \times \mathbf{AF}$.

The input formulas are first put in the passive set $\mathcal{P}$. Once an A-formula is selected for inferences and all inferences with it and the active A-formulas have been made redundant, it is moved to the active set $\mathcal{A}$. Inferences such as SPLIT produce disabled and propositional clauses, which are put into $\mathcal{Q}$. When switching to a new model, the prover moves the newly enabled A-formulas from $\mathcal{Q}$ to $\mathcal{P}$ and the newly disabled A-formulas from $\mathcal{A}$ and $\mathcal{P}$ to $\mathcal{Q}$ to preserve the state invariant.

The division of nonactive A-formulas into the sets $\mathcal{P}$ and $\mathcal{Q}$ is done for notational convenience; for example, $\mathcal{P}$ is a separate set because fairness will be stated in terms of $\mathcal{A}$ and $\mathcal{P}$. In a practical implementation, this division would likely be different. The set $\mathcal{Q}$ would typically be distributed over two data structures: The propositional clauses in $\mathcal{Q}_{\perp}$ are directly passed to the SAT solver and need not be stored by the prover itself. The remaining A-formulas $\mathcal{Q} \setminus \mathcal{Q}_{\perp}$ are those that need to be moved back into $\mathcal{P}$ when the prover switches to an interpretation that enables them. These might be stored in the same data structure as the set of locked A-formulas $\mathcal{L}$, which also need to be reactivated depending on the interpretation. This is what Vampire does. Alternatively, they could be stored in the same data structure as $\mathcal{P}$, with the prover checking on every access whether an A-formula is enabled in the current interpretation.

The AVATAR-based prover $\mathcal{AV}$ is defined as the following transitions:

**INFER**
$$ (\mathcal{J}, \mathcal{A}, \mathcal{P} \uplus \{\mathcal{C}\}, \mathcal{Q}, \mathcal{L}) \implies_{\mathcal{AV}} (\mathcal{J}, \mathcal{A} \cup \{\mathcal{C}\}, \mathcal{P}', \mathcal{Q}', \mathcal{L}) $$
if $\text{TSInf}(\mathcal{A}, \{\mathcal{C}\}) \subseteq \text{TSRed}_1(\mathcal{A} \cup \{\mathcal{C}\} \cup \mathcal{P}' \cup \mathcal{Q}'),$
$\mathcal{P} \subseteq \mathcal{P}',$ and $\mathcal{Q} \subseteq \mathcal{Q}'$

**PROCESS**
$$ (\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q}, \mathcal{L}) \implies_{\mathcal{AV}} (\mathcal{J}, \mathcal{A}', \mathcal{P}', \mathcal{Q}', \mathcal{L}) $$
if $\mathcal{A} \supseteq \mathcal{A}'$ and
$$ (\mathcal{A} \setminus \mathcal{A}') \cup (\mathcal{P} \setminus \mathcal{P}') \cup (\mathcal{Q} \setminus \mathcal{Q}') \subseteq \text{TSRed}_F(\mathcal{A}' \cup \mathcal{P}' \cup \mathcal{Q}') $$

**SWITCH**
$$ (\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q}, \mathcal{L}) \implies_{\mathcal{AV}} (\mathcal{J}', \mathcal{A}', \mathcal{P}' \cup \llbracket \mathcal{U} \rrbracket, \mathcal{Q}', \mathcal{L} \setminus \mathcal{U}) $$
if $\mathcal{J} \nvdash \mathcal{Q}_{\perp}, \mathcal{J}' \nvdash \mathcal{Q}_{\perp}, \mathcal{A}' = \{\mathcal{C} \in \mathcal{A} \mid \mathcal{C} \text{ is enabled in } \mathcal{J}'\},$
$\mathcal{U} = \{(B, (C \leftarrow A, t)) \in \mathcal{L} \mid B \not\subseteq \mathcal{J}' \text{ and } A \subseteq \mathcal{J}'\},$ and
$\mathcal{A} \cup \mathcal{P} \cup \mathcal{Q} = \mathcal{A}' \cup \mathcal{P}' \cup \mathcal{Q}'$

**STRONGUNSAT**
$$ (\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q}, \mathcal{L}) \implies_{\mathcal{AV}} (\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q} \cup \{(\perp, t)\}, \mathcal{L}) $$
if $\mathcal{Q}_{\perp} \models \{\perp\}$

**LOCKA**
$$ (\mathcal{J}, \mathcal{A} \uplus \{(C \leftarrow A, t)\}, \mathcal{P}, \mathcal{Q}, \mathcal{L}) \implies_{\mathcal{AV}} (\mathcal{J}, \mathcal{A}, \mathcal{P}, \mathcal{Q}, \mathcal{L} \cup \{(B, (C \leftarrow A, t))\}) $$
if $B \subseteq \mathcal{J}$ and $C \in \text{FRed}_F((\mathcal{A} \cup \mathcal{P})_{\mathcal{J}'})$ for every $\mathcal{J}' \supseteq \mathcal{A} \cup \mathcal{B}$

There is also a LOCKP rule that is identical to LOCKA except that it starts in the state $(\mathcal{J}, \mathcal{A}, \mathcal{P} \uplus \{(C \leftarrow A, t)\}, \mathcal{Q}, \mathcal{L})$. An AV-derivation is *well timestamped* if every A-formula
introduced by a rule is assigned a unique timestamp. In practice, a prover would ensure well-timestampedness by assigning timestamps monotonically, but this is not necessary for the fairness and completeness proofs.

**Lemma 54** Let $(\mathcal{J}_i, A_i, \mathcal{P}_i, \Omega_i, \mathcal{L}_i)_i$ be an $\Rightarrow_{AV}$-derivation. Then $(\mathcal{J}_i, \{A_i \cup \mathcal{P}_i \cup \Omega_i\}, \{\mathcal{L}_i\})_i$ is an $\Rightarrow_L$-derivation.

*Proof* The transitions map directly to the corresponding transitions in $\Rightarrow_L$; both INFER and PROCESS map to a LIFT of DERIVE. $\square$

**Lemma 55** Let $(\mathcal{J}_i, A_i, \mathcal{P}_i, \Omega_i, \mathcal{L}_i)_i$ be an $\Rightarrow_{AV}$-derivation such that $A_0 = \emptyset$. Then $\text{TSInf}(A_i) \subseteq \text{TSRed}_1(A_i \cup \mathcal{P}_i \cup \Omega_i \cup \llcorner \mathcal{L}_i \rrcorner)$ for every $i$.

*Proof* The invariant is preserved by each transition. $\square$

**Example 56** Let us redo the $\Rightarrow_{MG}$-derivation of Example 30 using $\Rightarrow_{AV}$. For readability, we emphasize in gray the A-clauses that appear or move between state components and omit all timestamps. One possible derivation is

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

**Example 57** Let us redo the $\Rightarrow_L$-derivation of Example 47 using $\Rightarrow_{AV}$, following the same conventions as in the previous example. One possible derivation is

<figure><img src="image_5.png" /></figure>
## 6.2 Counterexamples

In contrast with nonsplitting provers, for AV, fairness w.r.t. formulas does not imply fairness w.r.t. inferences. To ensure fairness in a nonsplitting prover, it suffices to select the oldest formula for inferences infinitely often; for example, provers can alternate between choosing the oldest and choosing the heuristically best formula. In splitting provers, such a strategy is incomplete, and we need an even stronger fairness criterion.

A problematic scenario involves two premises C, D of a binary inference t and four transitions repeated forever, with other steps interleaved: INFER makes C active; SWITCH disables it; INFER makes D active; SWITCH disables it. Even though C and D are selected in a strongly fair fashion, t is never performed.

**Example 58** More concretely, make two copies of the clause set

$$ \{\neg p(x) \lor p(f(x)) \lor q(x), \quad p(a), \quad \neg q(x), \quad \neg p(x) \lor q(f(x))\} $$

one with the assertion {$x_1$}, the other with {$x_2$}, in addition to the propositional clause $\perp \leftarrow \neg x_1, \neg x_2$. Suppose the prover starts with the model {$x_1$} and processes the clauses in the order given above. It first chooses the A-clause $\neg p(x) \lor p(f(x)) \lor q(x) \leftarrow \{x_1\}$ for inferences, followed by $p(a) \leftarrow \{x_1\}$. Let $fml(v_i) = p(f^i(a))$ and $fml(w_i) = q(f^i(a))$. By resolution and splitting, it derives $p(f(a)) \leftarrow \{v_1\}$, $q(a) \leftarrow \{w_0\}$, and $\perp \leftarrow \{x_1, \neg v_1, \neg w_0\}$. It then switches to a model in which $x_2$ is true. There it selects $\neg p(x) \lor p(f(x)) \lor q(x) \leftarrow \{x_2\}$ and $p(a) \leftarrow \{x_2\}$ for inferences, deriving analogous A-clauses as in the $x_1$ branch.

Let the models alternate between the $x_1$ and $x_2$ branches, making as few variables true as possible. Because the models alternate between the two branches, $\neg p(x) \lor p(f(x)) \lor q(x) \leftarrow \{x_i\}$ will always be the oldest passive A-clause after switching to a new model. Assume that the prover chooses this clause for inferences based on age. If we are allowed to interleave age-based selection with heuristic selection, we can cause the prover to switch model after selecting at most two additional A-clauses for inferences: If an A-clause $q(f^j(a)) \leftarrow \{w_j\}$ is enabled, we heuristically select both that A-clause and $\neg q(x) \leftarrow \{x_i\}$. Otherwise, an A-clause of the form $p(f^j(a)) \leftarrow \{v_j\}$ is enabled. Assume that $j$ is maximal among such clauses, and that thus $v_{j+1}$ is false in the model. We heuristically select that clause for inferences, deriving $\perp \leftarrow \neg v_{j+1}, \neg w_j, v_j, x_i$ by splitting $p(f^{j+1}(a)) \lor q(f^j(a)) \leftarrow \{v_j, x_i\}$.

With this strategy, the prover will never select $\neg p(x) \lor q(f(x)) \leftarrow \{x_i\}$ for inferences, since there is always an older clause to choose first. Consequently, it will never derive $\perp$.

In Example 58, the prover did not derive $\perp$ because it never performed an inference between $p(a) \leftarrow \{x_1\}$ and $\neg p(x) \lor q(f(x)) \leftarrow \{x_1\}$ (and analogously for $x_2$), even though both A-clauses are enabled infinitely often. Forbidding this situation does not guarantee completeness either. As Example 49 showed, there exist strongly fair derivations that do not derive $\perp$ from an inconsistent initial set.

We believe that this counterexample cannot arise with Vampire, because Vampire alternates between age-based and weight-based selection using a fixed ratio (the “age–weight ratio” or “pick–given ratio”). In contrast, our example requires a highly unrestricted heuristic selection, where we choose young, large A-clauses such as $p(f^n(a)) \leftarrow \{v_n\}$ even though smaller, older ones are enabled.

Unrelated to completeness, we might expect that under a reasonable strategy an $\implies_{AV}$-derivation saturates every limit point. This is, however, not the case either, even with strict age-based selection:
**Example 59** Take the following consistent A-clause set:

$$ \begin{array}{l} \{\neg q(x) \leftarrow \{x\}, \quad p(a) \leftarrow \{x\}, \quad \neg p(x) \vee p(f(x)) \vee q(f(x)) \leftarrow \{x\}, \\ \neg q(x) \leftarrow \neg x, \quad p(a) \leftarrow \neg x, \quad \neg p(x) \leftarrow \neg x \} \end{array} $$

Assume ordered resolution as the base calculus with the precedence $q \prec p$. Thus the prover will not resolve $\neg q(x) \leftarrow \{x\}$ with $\neg p(x) \vee p(f(x)) \vee q(f(x)) \leftarrow \{x\}$. We will sketch a derivation with two limit points, $\mathcal{J} \models x$ and $\mathcal{J}' \not\models x$, where $\mathcal{J}'$ will not be locally saturated. Let $fml(v_i) = p(f^i(a))$ and $fml(w_i) = q(f^i(a))$. We define the sequence of models $(\mathcal{J}_i)_i$ such that:

$$ \begin{array}{lclcl} \mathcal{J}_{2i} \models x & \quad & \mathcal{J}_{2i} \models v_j \text{ iff } j \le i & \quad & \mathcal{J}_{2i} \not\models w_j \\ \mathcal{J}_{2i+1} \not\models x & \quad & \mathcal{J}_{2i+1} \models v_j & \quad & \mathcal{J}_{2i+1} \models w_j \text{ iff } j > i \end{array} $$

The prover now starts in the model $\mathcal{J}_0$, and processes the formulas in the order we listed them at the beginning of the example. The first new formula it derives is $p(f(a)) \vee q(f(a)) \leftarrow \{x\}$, which it splits into $p(f(a)) \leftarrow \{v_1\}$, $q(f(a)) \leftarrow \{w_1\}$, and $\perp \leftarrow \{x, \neg v_1, \neg w_1\}$. The last propositional clause is not satisfied in $\mathcal{J}_0$, so the prover switches to a new interpretation.

After switching to the next model $\mathcal{J}_1 = \mathcal{J}_{2 \cdot 0+1}$, the two formulas $p(f(a)) \leftarrow \{v_1\}$ and $q(f(a)) \leftarrow \{w_1\}$ remain in the active set. The prover then chooses the oldest enabled passive formula, $\neg q(x) \leftarrow \neg x$, for inferences. Thus deriving the propositional clause $\perp \leftarrow \{\neg x, w_1\}$, which is not satisfied in $\mathcal{J}_1$.

This process is then repeated infinitely often. In the model $\mathcal{J}_{2i}$, the prover derives the three new formulas $p(f^{i+1}(a)) \leftarrow \{v_{i+1}\}$, $q(f^{i+1}(a)) \leftarrow \{w_{i+1}\}$, and $\perp \leftarrow \{x, \neg v_{i+1}, \neg w_{i+1}\}$. The last propositional clause causes a switch to the next model $\mathcal{J}_{2i+1}$, where $\perp \leftarrow \{\neg x, w_{i+1}\}$ is derived.

The subsequence $(\mathcal{J}_{2i+1})_i$ converges a limit point, call it $\mathcal{J}'$. The formulas enabled at $\mathcal{J}'$ are not saturated: $p(a)$ and $\neg p(x)$ are enabled, but $\perp$ is not.

## 6.3 Fairness

**Definition 60** An $\Rightarrow \mathcal{A}\mathcal{V}$-derivation $(\mathcal{J}_i, A_i, \mathcal{P}_i, \mathcal{Q}_i, \mathcal{L}_i)_i$ is fair if (A) $\mathcal{L}_0 = \emptyset$, (B) $A_0 = \emptyset$, and (C) either (1) $\perp \in \mathcal{L}_i \mathcal{Q}_i \frown$ or (2) $\mathcal{J}_i \models (\mathcal{Q}_i)_{\perp}$ for infinitely many indices $i$ and there exists a subsequence $(\mathcal{J}'_j)$ converging to a limit point $\mathcal{J}$ such that (3) $\liminf_{j \to \infty} \text{TSInf}(A'_j, \mathcal{P}'_j) = \emptyset$ and (4) $(\limsup_{j \to \infty} \mathcal{L}'_j \mathcal{J})_{\mathcal{J}} \setminus \mathcal{L}^{\infty} \mathcal{J} \subseteq \bigcup_i \text{FRed}_F((A_i \cup \mathcal{P}_i \cup \mathcal{Q}_i \cup \mathcal{L}_i \mathcal{J})_{\mathcal{J}})$.

Condition (3) ensures that all inferences involving passive A-formulas are redundant at the limit point. It would not suffice to simply require $\mathcal{P}'_\infty = \emptyset$ because A-formulas can move back and forth between the sets $A$, $\mathcal{P}$, and $\mathcal{Q}$, as we saw in Example 58. Condition (4) is similar to the condition on locks in Definition 50.

**Theorem 61 (Fairness) Let $(\mathcal{J}_i, A_i, \mathcal{P}_i, \mathcal{Q}_i, \mathcal{L}_i)_i$ be a fair $\Rightarrow \mathcal{A}\mathcal{V}$-derivation. Then the $\Rightarrow \mathcal{L}$-derivation $(\mathcal{J}_i, \mathcal{L}_i A_i \cup \mathcal{P}_i \cup \mathcal{Q}_i \frown, \mathcal{L}_i \mathcal{J})_i$ is fair.**

*Proof* We trivially have $\mathcal{L}_0 \frown = \emptyset$. Furthermore, if $\perp \in \mathcal{L}_i \mathcal{Q}_i$, we clearly have $\Rightarrow \mathcal{L}$-fairness. It remains to show subcase (B)(2) of Definition 50, using the corresponding subsequence as used for $\Rightarrow \mathcal{A}\mathcal{V}$-fairness. So let $\diamond_L = (\limsup_{j \to \infty} \mathcal{L}'_j \mathcal{J})_{\mathcal{J}} \setminus \mathcal{L}^{\infty} \mathcal{J} \subseteq \bigcup_j \text{FRed}_F((A_j \cup \mathcal{P}_j \cup \mathcal{Q}_j \cup \mathcal{L}_j \mathcal{J})_{\mathcal{J}})$ and $\diamond_{\mathcal{A}\mathcal{V}} = (\limsup_{j \to \infty} \mathcal{L}'_j \mathcal{J})_{\mathcal{J}} \setminus \mathcal{L}^{\infty} \mathcal{J} \subseteq \bigcup_j \text{FRed}_F((A_j \cup \mathcal{P}_j \cup \mathcal{Q}_j \cup \mathcal{L}_j \mathcal{J})_{\mathcal{J}})$, that is, every enabled formula in the subsequence is either persistent or redundant

First we show $(\bigcup_j A'_j \cup \mathcal{P}'_j \cup \mathcal{L}'_j \mathcal{J})_{\mathcal{J}} \subseteq (\liminf_{j \to \infty} A'_j \cup \mathcal{P}'_j)_{\mathcal{J}} \cup \bigcup_i \text{FRed}_F((A_i \cup \mathcal{P}_i \cup \mathcal{Q}_i \cup \mathcal{L}_i \mathcal{J})_{\mathcal{J}})$, that is, every enabled formula in the subsequence is either persistent or redundant
on the base level. So let $(C \leftarrow A, t) \in P'_j$. We prove the statement by induction on $(A, t)$ w.r.t. the lexicographic order. If $C \in \text{\textcolor{blue}{\textcircled{A}}}_\text{AV}$ or $C \in \llbracket \limsup_{j \to \infty} \textcolor{blue}{\mathcal{L}'_j \rfloor} \rfloor_\mathcal{G}$, we are done. Otherwise $C \notin \llbracket \mathcal{L}^{\to}_\infty \rfloor_\mathcal{G}$ (because $\llbracket \mathcal{L}^{\to}_\infty \rfloor_\mathcal{G} \subseteq \llbracket \limsup_{j \to \infty} \textcolor{blue}{\mathcal{L}'_j \rfloor} \rfloor_\mathcal{G}$) and hence $C \notin (\limsup_{j \to \infty} \llbracket \mathcal{L}'_j \rfloor \rfloor_\mathcal{G})_\mathcal{G}$ (because $C \notin \text{\textcolor{blue}{\textcircled{A}}}_\text{AV}$). So since $(C \leftarrow A, t)$ is not locked infinitely often, there exists an index after which it is never locked again, which means that it is either persistent in $(A'_j \cup P'_j)_j$ (and we are done) or deleted in PROCESS and thus $(C \leftarrow A, t) \in \bigcup_i \text{TSRed}_F(A_i \cup P_i \cup Q_i)_\mathcal{G}$. By definition of $\text{TSRed}_F$, either (a) $C \in \bigcup_i \text{FRed}_F((A_i \cup P_i \cup Q_i)_\mathcal{G})$, (b) $C \leftarrow B \in \bigcup_i \textcolor{blue}{A_i \cup P_i \cup \mathcal{S}}$ for some $B \subset A$, or (c) $(C \leftarrow A, s) \in \bigcup_i \textcolor{blue}{A_i \cup P_i}$ for some $s < t$. In case (a), we are done. In cases (b) and (c), we apply the induction hypothesis.

Now let $R = \bigcup_i \text{FRed}_1((A_i \cup P_i \cup Q_i \cup \llbracket \mathcal{L}_i \rfloor)_\mathcal{G})$ and compute

$$
\begin{align*}
& FInf((\liminf_{j \to \infty} \textcolor{blue}{\mathcal{A}'_j \cup P'_j \cup Q'_j})_\mathcal{G} \cup \text{\textcolor{blue}{\textcircled{L}}}_\text{L}) \\
&= FInf((\liminf_{j \to \infty} \textcolor{blue}{\mathcal{A}'_j \cup P'_j})_\mathcal{G} \cup \text{\textcolor{blue}{\textcircled{L}}}_\text{L}) \quad \begin{array}{l} \text{(since by fairness } \perp \notin (Q'_j)_\mathcal{G} \text{ and} \\ \text{hence } Q'_j \text{ is disabled at } \liminf) \end{array} \\
&\subseteq FInf((\liminf_{j \to \infty} \textcolor{blue}{\mathcal{A}'_j \cup P'_j})_\mathcal{G} \cup \bigcup_i \text{FRed}_F((A_i \cup P_i)_\mathcal{G})) \quad \begin{array}{l} \text{(as shown above)} \end{array} \\
&\subseteq FInf((\liminf_{j \to \infty} \textcolor{blue}{\mathcal{A}'_j \cup P'_j})_\mathcal{G}) \cup R \quad \begin{array}{l} \text{(by reducedness of } \text{FRed}) \end{array} \\
&= (\text{TSInf}(\liminf_{j \to \infty} \textcolor{blue}{\mathcal{A}'_j \cup P'_j}))_\mathcal{G} \cup R \quad \begin{array}{l} \text{(by Lemmas 13 and 53)} \end{array} \\
&= (\liminf_{j \to \infty} \text{TSInf}(\textcolor{blue}{\mathcal{A}'_j \cup P'_j}))_\mathcal{G} \cup R \quad \begin{array}{l} \text{(by property of } \liminf) \end{array} \\
&= (\liminf_{j \to \infty} \text{TSInf}(\textcolor{blue}{\mathcal{A}'_j \cup P'_j})_\mathcal{G}) \cup R \quad \begin{array}{l} \text{(by definition of } \text{TSInf}(, \,)) \end{array} \\
&\subseteq (\bigcup_i \text{TSRed}_1(\textcolor{blue}{\mathcal{A}'_i \cup P'_i \cup Q'_i \cup \llbracket \mathcal{L}'_i \rfloor})_\mathcal{G}) \cup \liminf_{j \to \infty} \text{TSInf}(\textcolor{blue}{\mathcal{A}'_j, P'_j})_\mathcal{G}) \cup R \quad \begin{array}{l} \text{(by Lemma 55)} \end{array} \\
&\subseteq (\bigcup_i \text{TSRed}_1(A_i \cup P_i \cup Q_i \cup \llbracket \mathcal{L}_i \rfloor))_\mathcal{G} \cup R \quad \begin{array}{l} \text{(by } \implies \text{\textcolor{blue}{\textcircled{A}}}_\text{AV}-\text{fairness}) \end{array} \\
&= \bigcup_i \text{FRed}_1((A_i \cup P_i \cup Q_i \cup \llbracket \mathcal{L}_i \rfloor)_\mathcal{G}) \quad \begin{array}{l} \text{(by Lemmas 16 and 53)} \end{array} \quad \square
\end{align*}
$$

**Corollary 62 (Dynamic completeness)** Assume $(\text{Fin}, \text{FRed})$ is statically complete. Given a fair $\implies \text{\textcolor{blue}{\textcircled{A}}}$-derivation $(\mathcal{J}_i, A_i, P_i, Q_i, \mathcal{L}_i)_i$ such that $P_0 \cup Q_0 \models \{\perp\}$, we have $\perp \in Q_i$ for some $i$.

*Proof* By Theorems 28, 39, and 51. $\square$

Assuming the restriction on locking we already required for $\implies_L$-derivations, the $\implies_{\text{AV}}$ relation is concrete enough to allow us to show that typical clause selection strategies are fair and avoid the counterexamples from Sects. 5.2 and 6.2. Many selection strategies are combinations of basic strategies, such as choosing the smallest formula by weight or the oldest by age. We capture such strategies using selection orders $\prec$. Intuitively, $\mathcal{C} \prec \mathcal{D}$ if the prover will select $\mathcal{C}$ before $\mathcal{D}$ whenever both are present. That is, the prover always chooses one of the $\prec$-minimal A-formulas. We use two selection orders: $\prec_{\text{TAF}}$, on timestamped A-formulas, must be followed infinitely often; $\prec_F$, on base formulas, must be followed otherwise.

**Definition 63** Let $X$ be a set. A selection order $\prec$ on $X$ is an irreflexive and transitive relation such that $\{y \mid y \not\prec x\}$ is finite for every $x \in X$.

**Example 64** Let $X \subseteq \text{TAF}$ be such that $X$ only contains finitely many A-formulas with the same timestamp. Define $\prec_{\text{age}}$ on $X$ so that $(\mathcal{C}, t) \prec_{\text{age}} (\mathcal{C}', t')$ if and only if $t < t'$. Then $\prec_{\text{age}}$ is a selection order corresponding to age-based selection.
**Remark 65** Every selection order is a well-founded relation, but not every well-founded relation is a selection order. A well-order is a selection order if and only if its order type is less than $\omega+1$. The ordinal $\omega+1 = \{0 < 1 < 2 < \cdots < \omega\}$ is not a selection order since $\{y \mid y \not\prec \omega\}$ is infinite. Even well-founded relations of low rank need not be selection orders: The empty relation $\emptyset \subseteq \mathbb{N} \times \mathbb{N}$ is irreflexive, transitive, and well-founded (with rank zero) but not a selection order.

Selection orders on **TAF** also generalize the mechanism, outlined by Bachmair and Ganzinger in a footnote [2, Sect. 4.3] and elaborated by Schlichtkrull et al. [27, Sect. 4], of using an $\mathbb{N}$-valued weight function that is strictly monotone in the timestamp.

**Example 66** Let $\mathbf{F}$ be the set of first-order clauses in a fixed signature. Define the selection order $\prec_{\mathbf{F}}$ on $\mathbf{F}$ by $C' \prec_{\mathbf{F}} C$ if and only if $|C'| \le |C|$, where $|C|$ denotes the sum of the number of nonvariable positions in $C$. Then $\prec_{\mathbf{F}}$ is a selection order because there exists at most a finite number of first-order clauses with at most $n$ nonvariable positions for any $n$. This selection order corresponds to a simple weight-based selection scheme.

The intersection of two orders $\prec_1$ and $\prec_2$ corresponds to the nondeterministic alternation between them. The prover may choose either a $\prec_1$-minimal or a $\prec_2$-minimal A-formula, at its discretion.

**Lemma 67** Let $\prec_1$ and $\prec_2$ be selection orders on $X$. Then $\prec_1 \cap \prec_2$ is a selection order as well.

*Proof* Irreflexivity and transitivity are preserved by intersections, and note that $\{y \mid \text{not } (x \prec_1 y \text{ and } x \prec_2 y)\} = \{y \mid x \not\prec_1 y\} \cup \{y \mid x \not\prec_2 y\}$ is finite as a union of two finite sets. $\square$

**Lemma 68** Let $\prec$ be a selection order on an infinite set $X$. Then for all elements $x$ and $y$, there exists an element $z$ such that $x \prec z$ and $y \prec z$.

*Proof* The set $X \setminus \{z \mid x \prec z \text{ and } y \prec z\} = \{z \mid x \not\prec z\} \cup \{z \mid y \not\prec z\}$ is finite, and therefore $\{z \mid x \prec z \text{ and } y \prec z\}$ is infinite and in particular nonempty. $\square$

To ensure completeness of the given clause procedure, we must restrict the inferences that the prover may perform; otherwise, it could derive infinitely many A-formulas with different assertions, causing it to switch between two branches of the split tree without making progress as in Example 58. Given $\mathcal{N} \subseteq \mathbf{AF}$, let $\lceil \mathcal{N} \rceil = \bigcup \{A \mid C \leftarrow A \in \mathcal{N} \text{ for some } C\}$.

**Definition 69** A function $F : \mathcal{P}(\mathbf{AF}) \to \mathcal{P}(\mathbf{AF})$ is called *strongly finitary* if (1) $|F(\mathcal{N})|$ is finite for every $\mathcal{N} \subseteq \mathbf{AF}$ such that $|\mathcal{N}|$ is finite, and (2) there exists a function $B : \mathbf{F} \to \mathcal{P}_{\text{fin}}(\mathbf{A})$ such that $\lceil F(\mathcal{N}) \rceil \subseteq \lceil \mathcal{N} \rceil \cup B(\lceil \mathcal{N} \rceil)$ for every $\mathcal{N} \subseteq \mathbf{AF}$.

A set of **AF**-inferences *Inf* is *strongly finitary* if the function $\mathcal{N} \mapsto \text{concl}(\text{Inf}(\mathcal{N}))$ is strongly finitary. An inference rule is *strongly finitary* if the set of inferences it defines is strongly finitary. We can extend a strongly finitary function *F* to sets of base formulas by taking $F_{\mathbf{F}}(\mathcal{N}) = |F(N \times \mathcal{P}_{\text{fin}}(\mathbf{A}))|$ for every $\mathcal{N} \subseteq \mathbf{F}$ and to sets of timestamped A-formulas by taking $F_{\mathbf{TAF}}(\mathcal{N}) = F(\lceil \mathcal{N} \rceil) \times \mathbb{N}$ for every $\mathcal{N} \subseteq \mathbf{TAF}$. The functions *F* and *F*<sub>**F**</sub> are finitary, mapping finite sets to finite sets. Moreover, if *F* and *G* are strongly finitary, then so is $\mathcal{N} \mapsto F(\mathcal{N}) \cup G(\mathcal{N})$.

The function *B* in Definition 69 gives a bound on the new assertions. For the inference rules *BASE*, *UNSAT*, *COLLECT*, *TRIM*, and *STRONG*-*UNSAT*, we can set $B(\mathcal{N}) = \emptyset$ since the conclusions do not contain assertions which were not already in the premises. So if
$Inf(N)$ is finite for every finite $N \subseteq \mathbf{F}$, then $Inf$ is strongly finitary. The inference rules $SPLIT$ and $APPROX$ require a nonempty $B(N)$, containing the assertions chosen for the split A-formulas. Deterministic splitting rules (where the chosen assertions are fully determined by the base formula), such as AVATAR's, are thus also strongly finitary because then $B(N)$ is finite. The optional inference rule $TAUTO$ is not strongly finitary.

For the completeness of the given clause procedure, Lemma 77, we will fix a strongly finitary function $I$ restricting the inferences: The prover may perform an inference only if its conclusion is in $I(\mathcal{A}_i)$, where $\mathcal{A}_i$ is the active clause set after the $INFER$ transition. This restriction will allow us to rule out the case where $[\cup_i \mathcal{A}_i]$ is finite and the prover switches models without making progress. Condition (1) in Definition 69 then says that the prover only infers finitely many $\mathbf{F}$-formulas—this will in turn ensure that splitting creates only finitely many new assertions. Condition (2) says that the inferred A-formulas contain only finitely many new assertions. Taken together, only finitely many assertions are added in the case where $[\cup_i \mathcal{A}_i]$ is finite, which means that the prover can only switch models finitely often, a contradiction.

Simplification rules used by the prover must be restricted even more to ensure completeness, because they can lead to new splits and assertions, and hence switching to new models. For example, simplifying $p(x*0) \lor p(x)$ to $p(0) \lor p(x)$ transforms a nonsplittable clause into a splittable one. Even for the standard orders on first-order clauses, there can be infinitely many clauses that are smaller than a given clause. For example, with the lexicographic path order, the set $\{u' | u' \prec u\}$ is typically infinite for a term $u$. If simplifications were to produce infinitely many new splittable clauses, the prover might split clauses and switch propositional interpretations forever without making progress.

**Example 70** Even if $\prec$ is a well-founded order on $\mathbf{F}$, and $I$ is a set of binary inferences such that $C_2 \prec C_1$ and $D \prec C_1$ for every inference $(C_2, C_1, D) \in I$, simplification with $I$ can still produce infinitely many base formulas. This is because in an AV prover, the same base formula may be rederived infinitely often (for example due to switching between two families of interpretations).

As a slightly abstract example, consider $\mathbf{F} = \mathbb{N} \cup \{\infty\}$ with $0 \prec 1 \prec 2 \prec \dots \prec \infty$, and let $I = \{(n, \infty, n+1) \mid n \in \mathbb{N}\}$. If the prover then rederives $\infty$ infinitely often, it might simplify $\infty$ using $I$ in a different way each time, the first time to 1, then to 2, and so on. We hence need to ensure that, in the entire derivation, each formula is simplified in at most a finite number of ways.

**Definition 71** Let $\prec$ be a transitive well-founded relation on $\mathbf{F}$, and let $\preceq$ be its reflexive closure. A function $S : \mathbf{AF} \to \mathcal{P}(\mathbf{AF})$ is a strongly finitary simplification bound for $\prec$ if $\mathcal{N} \mapsto \bigcup_{\mathcal{C} \in \mathcal{N}} S(\mathcal{C})$ is strongly finitary and $[\mathcal{C}'] \preceq [\mathcal{C}]$ for every $\mathcal{C}' \in S(\mathcal{C})$.

The prover may simplify an A-formula $\mathcal{C}$ to $\mathcal{C}'$ only if $\mathcal{C}' \in S(\mathcal{C})$. It may also delete $\mathcal{C}$. Strongly finitary simplification bounds are closed under unions, allowing the combination of simplification techniques based on $\prec$. For superposition, a natural choice for $\prec$ is the clause order. Analogously to strongly finitary functions, we define the extension of strongly finitary simplification bounds to sets of formulas as $S_{\mathbf{F}}(N) = [S(N \times \mathcal{P}_{\text{fin}}(\mathbf{A}))]$. The key property of strongly finitary simplification bounds is that if we saturate a finite set of A-formulas w.r.t. simplifications, the saturation is also finite. This is crucial to bound the number of A-formulas derived by the prover and thus the number of possible model switches: If the prover only selects a finite set of A-formulas for inferences, then simplification will only derive finitely many A-formulas as well, no matter how often an A-formula is derived again:
**Lemma 72** Let $S$ be a strongly finitary simplification bound. For every $\mathcal{C} \in \mathbf{AF}$, let $S^*(\mathcal{C}) = \bigcup_{i=0}^{\infty} S^i(\mathcal{C})$, where $S^i$ denotes the $i$th iterate of $S$. Then $S^*$ is also a strongly finitary simplification bound.

*Proof.* Clearly, $\lfloor \mathcal{C}' \rfloor \preceq \lfloor \mathcal{C} \rfloor$ for every $\mathcal{C}' \in S^*(\mathcal{C})$. Let $N \subseteq \mathbf{F}$ be finite. Next we show that $S^*_{\mathbf{F}}(N)$ is finite as well. Define a sequence of finite sets $M_i \subseteq \mathbf{F}$ by $M_0 = N$ and $M_{i+1} = M_i \cup S_{\mathbf{F}}(M_i)$. Clearly, $S_{\mathbf{F}}(M_\infty) \cup N \subseteq M_\infty = S_{\mathbf{F}}^*(N) \supseteq S^*_{\mathbf{F}}(N)$.

To show that $M_\infty$ is finite, consider the sequence $M_{i+1} \setminus M_i$. By construction $S_{\mathbf{F}}(M_i) \setminus M_i \subseteq (S_{\mathbf{F}}(M_i \setminus M_{i-1}) \cup S_{\mathbf{F}}(M_{i-1})) \setminus M_i \subseteq (S_{\mathbf{F}}(M_i \setminus M_{i-1}) \cup M_i) \setminus M_i = S_{\mathbf{F}}(M_i \setminus M_{i-1}) \setminus M_i$, and thus $M_{i+1} \setminus M_i = S_{\mathbf{F}}(M_i \setminus M_{i-1}) \setminus M_i$. Because $S$ is a strongly finitary simplification bound, $M_{i+1} \setminus M_i$ is always finite, and decreasing in the multiset extension of $\prec$. It is even strictly decreasing as long as $M_{i+1} \setminus M_i \neq \emptyset$ because $M_{i+1} \setminus M_i \cap M_{i-1} = \emptyset$ and therefore $M_{i+1} \setminus M_i \neq M_i \setminus M_{i+1}$. From the well-foundedness of $\prec$, it follows that $M_{i+1} \setminus M_i = \emptyset$ for large enough $i$ and that $S_{\mathbf{F}}^*(N) = M_\infty = \bigcup_i M_i = M_0 \cup \bigcup_i (M_{i+1} \setminus M_i)$ is finite.

Thus $\lfloor S^*(\mathcal{N}) \rfloor$ is finite whenever $\lfloor \mathcal{N} \rfloor$ is finite. It remains to exhibit a function $B' : \mathbf{F} \to \mathcal{P}_{\text{fin}}(\mathbf{A})$ such that $\lfloor S^*(\mathcal{N}) \rfloor \subseteq B'(\lfloor \mathcal{N} \rfloor) \cup \lfloor \mathcal{N} \rfloor$. By assumption, we have such a function $B$ for $S$. Then set $B'(C) = B(S^*_{\mathbf{F}}(C))$ (which is finite for all $C$), and we have $\lfloor S^{i+1}(\mathcal{N}) \rfloor = \lfloor S(S^i(\mathcal{N})) \rfloor \subseteq B(\lfloor S^i(\mathcal{N}) \rfloor) \cup \lfloor S^i(\mathcal{N}) \rfloor \subseteq B'(\lfloor \mathcal{N} \rfloor) \cup \lfloor S^i(\mathcal{N}) \rfloor$ and therefore $\lfloor S^i(\mathcal{N}) \rfloor \subseteq \lfloor \mathcal{N} \rfloor \cup B'(\lfloor \mathcal{N} \rfloor)$ by induction and hence $\lfloor S^*(\mathcal{N}) \rfloor \subseteq \lfloor \mathcal{N} \rfloor \cup B'(\lfloor \mathcal{N} \rfloor)$. $\square$

**Example 73** Let $\mathbf{F}$ be the set of first-order clauses and $S(C \leftarrow A) = \{C' \leftarrow A' \mid C'$ is a subclause of $C$ and $A' \subseteq A\}$. Then $S$ is a strongly finitary simplification bound, because (1) $C' \preceq C$ if $C'$ is a subclause of $C$ and (2) each clause has only finitely many subclauses. This $S$ covers many simplification techniques, including elimination of duplicate literals (simplifying $C \lor L \lor L$ to $C \lor L$), deletion of resolved literals (simplifying $C \lor u \not\approx u$ to $C$), and subsumption resolution (simplifying $C\sigma \lor D\sigma \lor L\sigma$ to $C\sigma \lor D\sigma$ given the side premise $C \lor \neg L$). Removing redundant clauses is possible with every $S$.

**Example 74** If the Knuth–Bendix order [16] is used as the term order and all weights are positive, then $S(C \leftarrow A) = \{C' \leftarrow A' \mid C' \prec C$ and $A' \subseteq A\}$ is a strongly finitary simplification bound. This can be used to cover demodulation.

**Example 75** The simplification rules COLLECT, TRIM, and STRONGUNSAT from Sect. 3.1 are all strongly finitary simplification bounds. In a practical implementation, SPLIT will deterministically split $C \in \mathbf{F}$ into $C_1, \dots, C_n$ and use the same assertions $a_i \in \text{asn}(C_i)$ every time. Under these conditions, SPLIT is also a strongly finitary simplification bound.

For other term orders, the $S$ in Example 74 is not strongly finitary, and proving that demodulation is a strongly finitary simplification bound is much more involved. In this case, the necessary strongly finitary simplification bound even depends on the derivation.

**Example 76** If unit equations are only removed by demodulation, reflexivity deletion, or subsumption, the one-step demodulations possible at any point in the derivation are a strongly finitary simplification bound. By Lemma 72, this implies that many-step demodulation is also a strongly finitary simplification bound.

Assume that demodulation is performed in a postorder traversal (i.e., subterms first), always rewriting using the oldest available equation. Also assume that if $l \approx r$ is an existing (ordered) equation and the prover derives $l \approx r'$, that $l \approx r'$ is not used for demodulation (but for example instead simplified to $r \approx r'$).

We will show that for every term $t$, there exist only finitely many terms $t'$ that are simplified from $t$ in one step. The term $t'$ will typically be different over the course of the derivation.
However, we can assign a decreasing well-founded measure to the rewrite step, ensuring finiteness. Consider a demodulation step transforming $C[\lceil\sigma\rceil]$ to $C[r\sigma]$ using an equation $l \approx r$, with $r\sigma \prec l\sigma$. Let $i$ be the index of $l\sigma$ in $C[\lceil\sigma\rceil]$ in a postorder traversal, let $|l|$ be the number of nonvariable positions in $l$, and let $u = 1$ if the equation is unorientable ($l \not\asymp r$) and $u = 0$ otherwise. Then the tuple $(i, |l|, u, r\sigma)$ decreases or stays the same in the left-to-right lexicographic order as we move along the derivation.

If the prover derives a new ordered equation $l' \approx r'$, it is possible that it applies at an earlier position in $C$, thus decreasing the $i$. Otherwise, it applies at the same position as $l \approx r$ previously, and the prover rewrites using the older $l \approx r$ first, keeping the tuple unchanged. If the equation $l \approx r$ is subsumed by $l' \approx r'$ and deleted, then $|l'| < |l|$. (Note that if $l \approx r$ is subsumed by $l \approx r'$, then $r$ and $r'$ are identical because all variables that occur in $r, r'$ also occur in $l$..) If $l \approx r$ is simplified to $t \approx r$ by $l' \approx r'$ and $l \not\asymp l'$, then $|l'| < |l|$. If $l \approx r$ is simplified to $t \approx r$ by $l \approx r'$ and $l \approx r$ is unorientable, then $|l'| = |l|$ and $u$ decreases. If $l \approx r$ is simplified to $l \approx t$ by $l' \approx r'$, then $|l|$ stays the same, $u$ might decrease, and $r\sigma \succ t\sigma$.

Based on the above definitions, we introduce a fairness criterion that is more concrete and easier to apply than the definition of fairness of $\implies_{AV}$-derivations.

**Lemma 77** Let $I$ be a strongly finitary function, and let $S$ be a strongly finitary simplification bound. Then a well-timestamped $\implies_{AV}$-derivation $(\mathcal{J}_i, A_i, \mathcal{P}_i, \mathcal{Q}_i, \mathcal{L}_i)_i$ is fair if all of the following conditions hold:

1. $\ll_{TAF}$ is a selection order on $\cup_i \mathcal{P}_i$, and $\ll_F$ is a selection order on $F$;

2. $A_0 = \emptyset, \mathcal{L}_0 = \emptyset$, and $\mathcal{P}_0 \cup \mathcal{Q}_0$ is finite;

3. for every INFER transition, either $C$ is $\ll_{TAF}$-minimal in $\mathcal{P}$ or $\lfloor C \rfloor$ is $\ll_F$-minimal in $\lfloor \mathcal{P} \rfloor$;

4. for every INFER transition, $\mathcal{P}' \cup \mathcal{Q}' \subseteq I_{TAF}(A \cup \{C\})$;

5. for every PROCESS transition, $\mathcal{P}' \cup \mathcal{Q}' \subseteq S^*_{TAF}(A \cup \mathcal{P} \cup \mathcal{Q} \cup \lfloor \mathcal{L} \rfloor)$;

6. if $\mathcal{J}_i \not\models (\mathcal{Q}_i)_{\perp}$, then eventually SWITCH or STRONGUNSAT occurs;

7. if $\mathcal{P}_i \neq \emptyset$, then eventually INFER, SWITCH, or STRONGUNSAT occurs;

8. there are infinitely many indices $i$ such that either $\mathcal{P}_i = \emptyset$ or INFER chooses a $\ll_{TAF}$-minimal $C$ at $i$;

9. $(\limsup_{j \to \infty} \lfloor \mathcal{L}'_j \rfloor)_{\emptyset} \setminus \lfloor \mathcal{L}^{\infty} \rfloor_{\emptyset} \subseteq \cup_j FRed_F((A_i \cup \mathcal{P}_i \cup \mathcal{Q}_i \cup \lfloor \mathcal{L}_i \rfloor)_{\emptyset})$ for every subsequence $(\mathcal{J}'_j)_j$ of $(\mathcal{J}_j)_i$ converging to a limit point $\mathcal{J}$.

*Proof* If $\perp \in \cup_i \mathcal{Q}_i$, the derivation is trivially fair. Otherwise, the STRONGUNSAT transition never occurs, and therefore SWITCH is eventually applied if the propositional clauses are not satisfied by the interpretation. Hence $\mathcal{J}_i \models \mathcal{Q}_i$ for infinitely many $i$, thus satisfying condition (C)(2) of Definition 36. Conditions (A) and (B) are satisfied due to condition (2) of this lemma, and (C)(4) due to (9). It remains to construct a subsequence $(\mathcal{J}'_j, A'_j, \mathcal{P}'_j, \mathcal{Q}'_j, \mathcal{L}'_j)_j$ such that $(\mathcal{J}'_j)_j$ converges to a limit point and $\liminf_{j \to \infty} TSInf(A'_j, \mathcal{P}'_j) = \emptyset$, as required for (C)(3).

**CASE 1:** The set of $\ll_F$-minimal A-formulas selected in an INFER transition for some state $j$ is unbounded in $\ll_F$. That is, for every $C \in F$, there is an INFER transition from state $j$ such that the selected A-formula $S_j$ is $\ll_F$-minimal in $\mathcal{P}_j$, and $C \ll_F \lfloor S \rfloor$. These INFER transitions clearly form an infinite subsequence. By Lemma 35, we can further refine it into a subsequence $(\mathcal{J}'_j, A'_j, \mathcal{P}'_j, \mathcal{Q}'_j, \mathcal{L}'_j)_j$ where $(\mathcal{J}'_j)_j$ converges to a limit point. Assume towards a contradiction that $\iota \in \liminf_{j \to \infty} TSInf(A'_j, \mathcal{P}'_j)$. By Lemma 68, for every $C \in \text{prems}(\iota)$ there exists an index $j$ such that $\lfloor C \rfloor \ll_F \lfloor S'_j \rfloor$. Therefore $\text{prems}(\iota) \subseteq A'_j$ by the $\ll_F$-minimality requirement on the INFER transition, a contradiction.
CASE 2: The set of $\ll_{\mathbf{TAF}}$-minimal A-formulas selected in an INFER transition for some state $j$ is unbounded in $\ll_{\mathbf{TAF}}$. This case is analogous to case 1.

CASE 3: Neither case 1 nor case 2 apply. Then the set of $\ll_{\mathbf{F}}$-minimal formulas selected in an INFER transitions is bounded and hence finite since $\ll_{\mathbf{F}}$ is a selection order. Similarly, the set of $\ll_{\mathbf{TAF}}$-minimal TAF-formulas selected in an INFER transitions is finite as well. Let $\mathcal{T}$ be the set of A-formulas selected in an INFER transition. So $|\mathcal{T}|$ and therefore $|\bigcup_i A_i|$ are both finite. The set $S_{\mathbf{F}}^*(I_{\mathbf{F}}(\bigcup_i A_i)) \cup [\mathcal{P}_0] \cup [\mathcal{Q}_0])$ is then finite, and therefore $|\bigcup_i (A_i \cup \mathcal{P}_i \cup \mathcal{Q}_i) \cup \ll_i \rfloor|$ is finite as well. Since both $S_{\mathbf{F}}^*$ and $I$ are strongly finitary, only a finite number of new assertions are introduced, and $|\bigcup_i (A_i \cup \mathcal{P}_i \cup \mathcal{Q}_i) \cup \ll_i \rfloor|$ is also finite. Thus $(\bigcup_i \mathcal{Q}_i)_{\perp}$ is also finite, and only a finite number of SWITCH transitions can occur. Thus there exists an index $N$ such that no SWITCH transitions occur at states $i > N$.

Now take the whole derivation as subsequence. We have $\mathcal{P}_{\infty} = \emptyset$ because there are infinitely many states $j$ with an INFER transition such that a $\ll_{\mathbf{TAF}}$-minimal A-formula $S_j$ is selected. After the initial $N$ steps, every A-formula is selected only once (that is, $S_i \neq S_j$ if $i \neq j$), because once it has been selected, it can only be removed from the active set if it becomes redundant or locked. (There are no SWITCH transitions.) In either case, the A-formula is removed from the passive set for the rest of the derivation. Newly derived A-formulas have a different timestamp due to the well-timestampedness requirement. Therefore, once an A-formula is in the active set, it will not come back into the passive set, and we have $\liminf_{i \to \infty} \text{TSInf}(A_i, \mathcal{P}_i) = \emptyset$. $\square$

Recall the abstract counterexample from Sect. 6.2 in which the A-formulas $\mathcal{C}$ and $\mathcal{D}$ were selected and disabled in turn. Intuitively, selection orders, together with the restrictions on the inferences, ensure that the prover will follow roughly the same steps whenever it is in a model that enables $\mathcal{C}$ and $\mathcal{D}$. Since there are only finitely many formulas that it can select for inferences before $\mathcal{C}$ or $\mathcal{D}$, the prover will eventually repeat itself and thus make progress.

We could refine AV further and use Lemma 77 to show the completeness of an imperative procedure such as Voronkov's extended Otter loop [28, Fig. 3], thus showing that AVATAR as implemented in Vampire is complete if locking is sufficiently restricted. A slight complication is that in Vampire's AVATAR, A-clauses $C \leftarrow \{[C]\}$ are generated on a per-need basis when switching model. This is not a serious issue because we can imagine that the A-clauses were there all along in the $\mathcal{Q}$ set.

Even the concrete criterion offered by Lemma 77 refers, in its condition 9, to limit superiors and limit points. Some architectures will satisfy it by their very design. For AVATAR, an easy way to meet the condition is to bound the number of times each A-formula can be locked. Once that number has been reached, the A-formula can no longer be locked. An alternative, suggested by a reviewer, is to disable all splitting after the prover has run for a specified time.

## 7 Application to Other Architectures

AVATAR may be the most natural application of our framework, but it is not the only one. We will complete the picture below by studying splitting without backtracking, labeled splitting, and SMT with quantifiers.
## 7.1 Splitting without Backtracking

Before the invention of AVATAR, Riazanov and Voronkov [25] had already experimented with splitting in Vampire in a lighter variant without backtracking. They based their work on ordered resolution O with selection [2], but the same ideas work with superposition. Weidenbach [31, end of Sect. 4.5] independently outlined the same technique at about the same time.

The basic idea of splitting without backtracking is to extend the signature Σ with a countable set P of nullary predicate symbols disjoint from Σ and to augment the base calculus with a binary splitting rule that replaces a clause C ∨ D with C ∨ p and D ∨ ¬p, where C and D share no variables and p ∈ P. Riazanov and Voronkov require that the precedence ≺ makes all P-literals smaller than the Σ-literals. Binary splitting then qualifies as a simplification rule. They show that their rule and a few variants are consistency-preserving. They do not show refutational completeness, but this is obvious since the rule is a simplification.

Riazanov and Voronkov also extend the selection function of the base calculus to support P-literals. They present two such extensions: The blocking function allows for the selection of P-literals in clauses that contain Σ-literals, whereas the parallel function selects only maximal P-literals in pure P-clauses and otherwise imitates the original selection function. Parallel selection cleanly separates the P- and the Σ-literals. Bachmair and Ganzinger proved O statically complete, and this also obviously extends to ordered resolution with this extension, which we denote by O<sub>P</sub>, since it is an instance of the same calculus.

The calculus O<sub>P</sub> is closely related to an instance of our framework. Let F be the set of Σ-clauses, with the empty clause as ⊥. Let O = (F<sub>Inf</sub>, F<sub>Red</sub>), where F<sub>Inf</sub> is the set of ordered resolution inferences on F with some selection function and F<sub>Red</sub> is the standard redundancy criterion [2, Sect. 4.2.2], and similarly O<sub>P</sub> = (F<sub>PInf</sub>, F<sub>PRed</sub>). We use the notion of entailment from Example 1 for the base relations ⊨ and ≑ for both calculi. We take V = P for defining AF. The properties (D1)–(D6) and (R1)–(R7) are verified for ⊨ and F<sub>Red</sub>, respectively. This gives us a splitting calculus LA = (S<sub>Inf</sub>, S<sub>Red</sub>), whose name stands for lightweight AVATAR. Lightweight AVATAR amounts to the splitting architecture Cruanes implemented in Zipperposition and confusingly called “AVATAR” [9, Sect. 2.5]. Binary splitting can be realized in LA as the following simplification rule:

$$ \frac{C \lor D \leftarrow A}{C \leftarrow A \cup \{a\} \quad D \leftarrow A \cup \{\neg a\}} \quad \text{BINSPLIT} $$

with the side conditions that $a \in asn(C)$ and $C \lor D$ is splittable into C, D. By Theorem 21, LA is complete.

Like splitting without backtracking but unlike the real AVATAR, Cruanes's architecture is not guided by a propositional model. It is essentially an instance of LA, except that it is based on superposition instead of ordered resolution. It performs branch-specific simplifications (a special case of subsumption demodulation [15]), which is supported by our locking mechanism. A SAT solver is used to detect propositional unsatisfiability (correponding to our UNSAT rule) and to eliminate assertions that are implied at the SAT solver's top level (corresponding to our TRIM rule).

The calculi O<sub>P</sub> and LA are very similar but not identical. O<sub>P</sub> has a slightly stronger notion of inference redundancy, because its order ≺ can access not only the Σ-literals but also the P-literals, whereas with LA the P-literals are invisible to the base calculus. To see this, consider the set consisting of the Σ<sub>P</sub>-clauses

q

b ∨ p ∨ ¬q

¬a ∨ p ∨ ¬q

a ∨ p ∨ ¬q
where $\mathbb{P} = \{a, b\}$. Given the precedence $a \prec b \prec p \prec q$, an ordered resolution inference is
possible between the first two clauses, with $b \lor p$ as its conclusion. This inference is redundant
according to $FPRed_1$, because the conclusion is entailed by the first, third, and fourth clauses
taken together, all of which are $\prec$-smaller than the main premise $b \lor p \lor \neg q$. However, the
corresponding AF-inference is not redundant according to $SRed_1$, because the assertions are
simply truncated by the projection operator $(\cdot)_\mathcal{G}$ and not compared. Without the assertions,
the third and fourth clauses are equal to, but not smaller than, the main premise, and the
inference is not redundant. Note that the set is not saturated: Inferences are possible to derive
$\neg a \lor p$ and $a \lor p$, which make $b \lor p$ redundant.

Another dissimilarity is that LA can detect unsatisfiability immediately using a SAT
solver, whereas splitting without backtracking generally needs many propositional resolution
steps to achieve the same. Correspondingly, on satisfiable problems, LA allows smaller
saturated sets. For example, while the A-clause set $\{\perp \leftarrow \{a, \neg b\}, \perp \leftarrow \{b\}\}$ is saturated, its
$O_{\mathbb{P}}$ counterpart is subject to an inference between $\neg a \lor b$ and $\neg b$.

As positive results, we will show that $O_{\mathbb{P}}$ and LA share the same notion of entailment
and $O_{\mathbb{P}}$'s redundancy criterion is stronger than LA's, yet saturation w.r.t. LA guarantees
saturation w.r.t. $O_{\mathbb{P}}$, up to the natural correspondence between A-clauses and $\Sigma_{\mathbb{P}}$-clauses.
More precisely, a $\Sigma_{\mathbb{P}}$-clause can be written as $C \lor L_1 \lor \cdots \lor L_n$, where $C$ is a $\Sigma$-clause
and the $L_i$'s are $\mathbb{P}$-literals. Let $\alpha$ be a bijective mapping such that $\alpha(C \lor L_1 \lor \cdots \lor L_n) =
C \leftarrow \{\neg L_1, \dots, \neg L_n\}$ is the corresponding A-clause. We overload the operator $\lfloor \rfloor$ to erase
the $\mathbb{P}$-literals: $\lfloor C \lor L_1 \lor \cdots \lor L_n \rfloor = \lfloor C \leftarrow \{\neg L_1, \dots, \neg L_n \} \rfloor = C$. Moreover, let $\mathcal{G}$ denote the
function that returns all ground instances of a clause, clause set, or inference according to $\Sigma$,
which is assumed to contain at least one constant.

**Lemma 78** *Given the $\Sigma_{\mathbb{P}}$-clause sets $M, N$, we have $M \models N$ if and only if $\alpha(M) \models \alpha(N)$.*

*Proof* Since both entailments are defined via grounding, it suffices to consider the case where $M$ and $N$ are ground.

For the forward direction, we must show that $(\alpha(M))_\mathcal{G} \models \lfloor N \rfloor$ for some $\mathcal{J}$ in which $\alpha(N)$ is enabled. Let $\mathcal{K}$ be a $\Sigma$-model of $\{\alpha(M)\}_\mathcal{G}$. We will show that at least one clause in $\lfloor N \rfloor$ is true in $\mathcal{K}$. We start by showing that $\mathcal{K} \cup \mathcal{J}$ is a $\Sigma_{\mathbb{P}}$-model of $M$. Let $C \in M$. If $\alpha(C)$ is enabled in $\mathcal{J}$, then $\lfloor C \rfloor \in (\alpha(M))_\mathcal{J}$. Thus $\mathcal{K} \models \lfloor C \rfloor$ and finally $\mathcal{K} \cup \mathcal{J} \models \{C\}$. Otherwise, $\alpha(C)$ contains an assertion that is false in $\mathcal{J}$, which means that $C$ contains the complementary $\mathbb{P}$-literal, which is true in $\mathcal{J}$, and we have $\mathcal{K} \cup \mathcal{J} \models \{C\}$. Either way, $\mathcal{K} \cup \mathcal{J} \models M$ and hence, since $M \models N$, one of the clauses in $N$ is true in $\mathcal{K} \cup \mathcal{J}$. Since $\alpha(N)$ is enabled in $\mathcal{J}$, all $\mathbb{P}$-literals occurring in $N$ are false in $\mathcal{K} \cup \mathcal{J}$. Therefore, each clause in $N$ must contain a true $\Sigma$-literal in $\mathcal{K}$, which means that the corresponding clause in $\lfloor N \rfloor$ must also be true in $\mathcal{K}$.

For the backward direction, we must show that $M \models N$. Let $\mathcal{K} \cup \mathcal{J}$ be a $\Sigma_{\mathbb{P}}$-model of $M$, where $\mathcal{K}$ is a $\Sigma$-interpretation and $\mathcal{J}$ is a $\mathbb{P}$-interpretation. We will show that a clause in $N$ is true in $\mathcal{K} \cup \mathcal{J}$. If $\alpha(N)$ is disabled in $\mathcal{J}$, there exists a $\mathbb{P}$-literal in some clause from $N$ that is true in $\mathcal{K} \cup \mathcal{J}$, which suffices to make the entire clause true. Otherwise, $N$ is enabled in $\mathcal{J}$ and then $(\alpha(M))_\mathcal{G} \models \lfloor N \rfloor$. Since $\mathcal{K} \cup \mathcal{J} \models M$, we have $\mathcal{K} \models (\alpha(M))_\mathcal{G}$. Hence, one of the clauses in $\lfloor N \rfloor$ is true in $\mathcal{K}$, and its counterpart in $N$ is also true in $\mathcal{K} \cup \mathcal{J}$. $\square$

**Lemma 79** *Given an inference $\iota$ over $\Sigma_{\mathbb{P}}$-clauses, if $\alpha(\iota)$ is a BASE inference, then $\iota \in FPInf$.*

*Proof* Let $\iota = (C_n, \dots, C_1, C_0)$ and assume $\alpha(\iota)$ is a BASE inference. By the definition of ordered resolution, none of the $\Sigma$-clauses $\lfloor C_i \rfloor$, for $i \in \{1, \dots, n\}$, can be $\perp$. Thus, the selected literals in the premises coincide with those chosen by the parallel selection function on the $\Sigma_{\mathbb{P}}$-clauses $C_i$ and so $\iota \in FPInf$. $\square$
**Lemma 80** (1) Given a $\Sigma_P$-clause C, if $\alpha(C) \in SRed_F(\alpha(N))$, then $C \in FPRed_F(N)$. (2) Given an inference $\iota$ over $\Sigma_P$-clauses, if $\alpha(\iota) \in SRed_I(\alpha(N))$, then $\iota \in FPRed_I(N)$.

*Proof* For (2), let $\iota' \in \mathcal{G}(\iota)$ and let $C_n, \dots, C_1$ be $\iota$'s premises and $C_0$ be its conclusion. Let $\mathcal{E} = \{C \leftarrow A \in \alpha(\mathcal{G}(N)) \mid C \prec [C_1]\}$ and $\mathcal{F} = \{C \in N \mid \mathcal{G}(C) \prec C_1\}$. By the definition of standard redundancy, assuming that $\{\alpha(C_n), \dots, \alpha(C_2)\} \cup \mathcal{E} \models \{\alpha(C_0)\}$ we need to show that $\{C_n, \dots, C_2\} \cup \mathcal{F} \models \{C_0\}$. By Lemma 78, this amounts to showing that $\{\alpha(C_n), \dots, \alpha(C_2)\} \cup \alpha(\mathcal{F}) \models \{\alpha(C_0)\}$. By (D3), this follows from our assumption if $\mathcal{E} \subseteq \alpha(\mathcal{F})$. This subset inclusion holds because if $C \prec [C_1]$, then we have $C \vee D \prec C_1$ for every $P$-clause $D$, since $P$-literals are smaller than $\Sigma$-literals.

For (1), essentially the same line of argumentation applies, with $n = 1$ and $C_1 = C_0 = C$. $\square$

**Lemma 81** (Saturation) Let $N$ be a set of $\Sigma_P$-clauses. If $N$ is saturated w.r.t. $O_P$, then $\alpha(N)$ is saturated w.r.t. LA.

*Proof* Let $\iota = (\alpha(C_n), \dots, \alpha(C_1), \alpha(C_0)) \in SInf$ be an inference with premises in $\alpha(N)$. We will show that it is redundant w.r.t. $\alpha(N)$.

**CASE BASE:** We need to show that $\{\iota\} \subseteq FRed_I((\alpha(\mathcal{G}(N)))_\mathcal{J})$ for every propositional interpretations $\mathcal{J}$. The case where $\iota$ is disabled in $\mathcal{J}$ is trivial. Otherwise, let $\theta$ be a substitution such that $\iota\theta \in \mathcal{G}(\iota)$. We must show that $\{[C_n\theta], \dots, [C_2\theta]\} \cup \mathcal{E} \models \{[C_0\theta]\}$, where $\mathcal{E} = \{\alpha(C) \mid C \in \mathcal{G}(N) \text{ and } [C] \prec [C_1\theta]\}$. Because the premises' assertions are contained in the conclusion's, this is equivalent to showing that $\{\alpha(C_n\theta), \dots, \alpha(C_2\theta)\} \cup \mathcal{E} \models \{\alpha(C_0\theta)\}$.

By Lemma 79, there exists an inference $(C_n, \dots, C_1, C_0) \in FPInf$. Since $N$ is saturated, the inference is redundant—i.e., $\{C_n\theta, \dots, C_2\theta\} \cup \mathcal{F} \models \{C_0\theta\}$, where $\mathcal{F} = \{C \mid C \in \mathcal{G}(N) \text{ and } C \prec C_1\theta\}$. If $\alpha(\mathcal{F}) \subseteq \mathcal{E}$, we can invoke Lemma 78 to conclude. However, in the general case, we have only that $\alpha(\mathcal{F} \setminus \mathcal{F}_{eq}) \subseteq \mathcal{E}$, where $\mathcal{F}_{eq} = \{C \in \mathcal{F} \mid [C] = [C_1\theta]\}$, and thus there might be models of $\mathcal{E}$ that are models of $\mathcal{F} \setminus \mathcal{F}_{eq}$ but not of $\mathcal{F}_{eq}$. Fortunately, we can show that $\{C_n\theta, \dots, C_2\theta\} \cup (\mathcal{F} \setminus \mathcal{F}_{eq}) \models \{C_0\theta\}$. We proceed by removing from $\mathcal{F}$ each clause $D \in \mathcal{F}_{eq}$ in turn and by showing that the entailment is preserved by each step. Finally, we invoke Lemma 78. A slight complication is that $\mathcal{F}_{eq}$ may be infinite. However, by compactness, only a finite subset $\mathcal{F}'_{eq} \subseteq \mathcal{F}_{eq}$ is needed to have the desired entailment.

Let $D \in N$ be a clause that generalizes the ground, >-largest clause in $\mathcal{F}'_{eq}$. Then there exists an inference $(C_n, \dots, C_2, D, D_0) \in FPInf$ such that $[C_0\theta] \in [\mathcal{G}(D_0)]$ and the $P$-literals of $D_0$ are the union of those of $C_n, \dots, C_2, D$. By renaming the variables in $D$ and $D_0$, we can ensure that $[D\theta] = [C_1\theta]$ and $[D_0\theta] = [C_0\theta]$. Now, to prove the desired entailment, assume that $\mathcal{J}$ is a model of $\{C_n\theta, \dots, C_2\theta\} \cup (\mathcal{F} \setminus \{D\theta\})$. Since $N$ is saturated, $\{C_n\theta, \dots, C_2\theta\} \cup \{C \in \mathcal{G}(N) \mid C \prec D\theta\} \models \{D_0\theta\}$. Since we are proceeding from largest to smallest clause, we have $\{C \in \mathcal{G}(N) \mid C \prec D\theta\} \subseteq \mathcal{F} \setminus \{D\theta\}$, even if some clauses have been removed from $\mathcal{F}$ already. Thus, in both cases, $\mathcal{J} \models \{D_0\theta\}$. If $\mathcal{J}$ makes a $\Sigma$-literal of $D_0\theta$ true, $\mathcal{J}$ makes the same literal in $C_0\theta$ true. Otherwise, either $\mathcal{J}$ makes one of the $P$-literals of $C_n\theta, \dots, C_2\theta$ true, satisfying $C_0\theta$ for the same reason, or it makes one of the $P$-literals of $D$ true and then $\mathcal{J} \models \{C_n\theta, \dots, C_2\theta\} \cup \mathcal{F}$, which as noted above implies $\mathcal{J} \models \{C_0\theta\}$ by the saturation of $N$. In both cases, $\mathcal{J} \models \{C_0\theta\}$.

**CASE UNSAT:** The inference derives $\perp$ from a set of $P$-clauses $(\alpha(A_i))_{i=1}^n$ such that $\{\alpha(A_i)\}_i$ is propositionally unsatisfiable—i.e., $\{A_i\}_i \models \{\perp\}$ in $O_P$. Since $O_P$ is complete and $N \supseteq \{A_i\}_i$ is saturated, we have $\perp \in N$ and hence $\perp \in \alpha(N)$. Therefore, $\iota$ is redundant also in this case. $\square$
## 7.2 Labeled Splitting

Labeled splitting, as originally described by Fietzke and Weidenbach [13] and implemented in SPASS, is a first-order resolution-based calculus with binary splitting that traverses the split tree in a depth-first way, using an elaborate backtracking mechanism inspired by CDCL [20]. It works on pairs $(\Psi, \mathcal{N})$, where $\Psi$ is a stack storing the current state of the split tree and $\mathcal{N}$ is a set of labeled clauses—clauses annotated with finite sets of natural numbers.

We model labeled splitting as an instance of the locking prover L based on the splitting calculus LS = (SInf, SRed) induced by the resolution calculus R = (Finf, FRed), where $\models$ and $\vDash$ are as in Example 1 and $V = \cup_{i \in \mathbb{N}} \{l_i, r_i, s_i\}$. A-clauses are essentially the same as labeled clauses.

Splits are identified by unique split levels. Given a split on $C \vee D$ with level $k$, the propositional variables $l_k \in asn(C)$ and $r_k \in asn(D)$ represent the left and right branches, respectively. In practice, the prover would dynamically extend fml to ensure that $fml(l_k) = C$ and $fml(r_k) = D$.

When splitting, if we simply added the propositional clause $\perp \leftarrow \{\neg l_k, \neg r_k\}$, we would always need to consider either $C \leftarrow \{l_k\}$ or $D \leftarrow \{r_k\}$, depending on the interpretation. However, labeled splitting can undo splits when backtracking. Yet fairness would require us to perform inferences with either C or D, which Fietzke and Weidenbach avoid. We solve this as follows. Let $\top = \sim \perp$. We introduce the propositional variable $s_k \in asn(\top)$ so that we can enable or disable the split as we wish. The STRONGUNSAT rule then knows that $s_k$ is true and that the cases are exhaustive, but we can still switch to propositional models that disable both C and D. A-clauses are then split using the following binary variant of SPLIT:

$$ \frac{C \vee D \leftarrow A \quad C \leftarrow A \cup \{l_k\} \quad D \leftarrow A \cup \{r_k\}}{\perp \leftarrow \{\neg l_k, \neg r_k, s_k\}} \text{ SOFTSPLIT} $$

where C and D share no variables and k is the next split level. Unlike AVATAR, labeled splitting keeps the premise and might split it again with another level. We rely on locking to ensure that the premise is not split within either branch.

To emulate the original, the locking prover based on the LS calculus must repeatedly apply the following three steps in any order until saturation:

1. Apply BASE (via LIFT and DERIVE) to perform an inference from the enabled A-clauses. If an enabled $\perp \leftarrow A$ is derived with $A \subseteq \cup_i \{l_i, r_i\}$, apply SWITCH or STRONGUNSAT.

2. Use DERIVE (via LIFT) to delete a redundant enabled A-clause.

3. Use LOCK to temporarily remove a locally redundant enabled A-clause.

4. Use DERIVE (via LIFT) to simplify an enabled A-clause. If the original A-clause is made redundant, delete it; otherwise, use LOCK to temporarily remove it. If an enabled $\perp \leftarrow A$ is derived with $A \subseteq \cup_i \{l_i, r_i\}$, apply SWITCH or STRONGUNSAT.

5. Apply SOFTSPLIT (via LIFT and DERIVE) with split level $k$ on an A-clause $\mathcal{C}$. Then use SWITCH to enable the left branch and apply LOCK on $\mathcal{C}$ with $s_k$ as the lock.

Disabled A-clauses are the ones that occur in branches other than the current one and in disabled splits. As such, they should not be used when exploring the current branch.

SWITCH is powerful enough to support all of Fietzke and Weidenbach's backtracking rules, but to explore the tree in the same order as they do, we must choose the new model carefully. If a left branch is closed, the model must be updated so as to disable the splits that were not used to close this branch and to enable the right branch. If a right branch is
closed, the split must be disabled, and the model must switch to the right branch of the closest enabled split above it with an enabled left branch. If a right branch is closed but there is no split above with an enabled left branch, the entire tree has been visited. Then, a propositional clause $\perp \leftarrow A$ with $A \subseteq \cup_i \{s_i\}$ is $\models$-entailed by the A-clause set, and STRONGUNSAT can finish the refutation by exploiting $fml(s_i) = \top$.

We illustrate the strategy on an example.

**Example 82** Let $\mathcal{N}_0$ be the clause set

$$ \{\neg q(x), p(x) \lor q(y), r(x) \lor s(y), \neg p(x) \lor q(y)\} $$

It is unsatisfiable due to the first, second, and fourth clauses. Let $\mathcal{J}_0 = \neg \mathbf{V}$ be the initial model. The first disjunction is split into $p(x) \leftarrow \{l_0\}$, $q(y) \leftarrow \{r_0\}$ and $\perp \leftarrow \{-l_0, \neg r_0, s_0\}$ by SOFTSPLIT. Then a SWITCH transition replaces $\mathcal{J}_0$ with $(\mathcal{J}_0 \setminus \{-l_0, \neg s_0\}) \cup \{l_0, s_0\}$. This enables the A-clause $p(x) \leftarrow \{l_0\}$. Then LOCK removes $p(x) \lor q(y)$ from $\mathcal{N}_0$ for as long as $s_0$ is enabled. Splitting the other two disjunctions leads to the state $(\mathcal{J}', \mathcal{N}', \mathcal{L}')$, where

$$ \mathcal{J}' = (\mathcal{J}_0 \setminus \bigcup_{i=0}^2 \{\neg l_i, \neg s_i\}) \cup \bigcup_{i=0}^2 \{l_i, s_i\} $$

$$ \mathcal{N}' = \bigcup_{i=0}^{2} \{\perp \leftarrow \{\neg l_i, \neg r_i, s_i\}\} \cup \{\neg q(x), \quad p(x) \leftarrow \{l_0\}, \quad r(x) \leftarrow \{l_1\}, \quad \neg p(x) \leftarrow \{l_2\} \\ q(y) \leftarrow \{r_0\}, \quad s(y) \leftarrow \{r_1\}, \quad q(y) \leftarrow \{r_2\} \} $$

$$ \mathcal{L}' = \{((\mathbf{s}_0), \mathbf{p}(x) \lor \mathbf{q}(x)), \quad ((\mathbf{s}_1), \mathbf{r}(x) \lor \mathbf{s}(y)), \quad ((\mathbf{s}_2), \neg \mathbf{p}(x) \lor \mathbf{q}(y))\} $$

where the last three clauses listed in $\mathcal{N}'$ are disabled and thus currently unusable for inferences.

The first backtracking step happens after a BASE inference produces $\perp \leftarrow \{l_0, l_2\}$ from $p(x) \leftarrow \{l_0\}$ and $\neg p(x) \leftarrow \{l_2\}$. The SWITCH disables $s_1$, because this split was not useful in closing the branch, and it moves from branch $l_2$ to $r_2$. The new model disables $\neg p(x) \leftarrow \{l_2\}$, enables $q(y) \leftarrow \{r_2\}$, and unlocks $r(x) \lor s(y)$.

The second backtracking step happens after $\perp \leftarrow \{r_2\}$ is derived from $\neg q(x)$ and $q(y) \leftarrow \{r_2\}$. Since both branches of the split $s_2$ have now been closed, the SWITCH rule is invoked, producing the model $(\mathcal{J}_0 \setminus \{-r_0, \neg s_0\}) \cup \{r_0, s_0\}$. This unlocks $\neg p(x) \lor q(y)$, and now only $q(y) \leftarrow \{r_0\}$ is enabled in addition to the unlocked input clauses. The $r_0$ branch is immediately closed by the generation of $\perp \leftarrow \{r_0\}$ from $q(y) \leftarrow \{r_0\}$ and $\neg q(x)$.

Now, the resulting A-clause set contains the propositional clauses $\perp \leftarrow \{l_0, l_2\}$, $\perp \leftarrow \{r_2\}$, $\perp \leftarrow \{r_0\}$ derived by inferences as well as $\perp \leftarrow \{s_0, \neg l_0, \neg r_0\}$ and $\perp \leftarrow \{s_2, \neg l_2, \neg r_2\}$ produced by SPLIT. Clearly, it entails $\perp \leftarrow \{s_0, s_2\}$. Since $fml(s_0) = fml(s_2) = \sim \perp$, at this point STRONGUNSAT derives $\perp$.

By following the strategy presented above, LS closely simulates the original calculus, in the sense that it is possible to add and remove (or at least disable) exactly the same elements to the A-clause set as is done in the original, and in the same order. A subtle, inconsequential difference lies in the backtracking: Labeled splitting can move to a branch where $\perp$ is enabled, whereas our SWITCH rule requires that all propositional clauses are satisfied.

What about fairness? The above strategy helps achieve fairness by ensuring that there exists at most one limit point. It also uses locks in a well-behaved way. This means we can considerably simplify the notion of fairness for $\implies_L$-derivations and obtain a criterion that is almost identical to, but slightly more liberal than, Fietzke and Weidenbach's, thereby re-proving the completeness of labeled splitting.
For terminating derivations, their fairness criterion coincides with ours: Both require that the final A-clause set is locally saturated and all propositional clauses are satisfied by the interpretation. For diverging derivations, Fietzke and Weidenbach construct a limit subsequence $(\Phi'_i, \mathcal{N}'_i)_i$ of the derivation $(\Phi_i, \mathcal{N}_i)_i$ and demand that every persistent inference in it be made redundant, exactly as we do for $\Rightarrow_L$-derivations. The subsequence consists of all states that lie on the split tree's unique infinite branch. Therefore, this subsequence converges to a limit point of the full derivation. Locks are well behaved, with $\limsup_{j \to \infty} \|\mathcal{L}'_j\| = \|\mathcal{L}^{\to}\|$, because with the strategy above, once an A-clause is enabled on the rightmost branch, it remains enabled forever. Our definition of fairness allows more subsequences, although this is difficult to exploit without bringing in all the theoretical complexity of AVATAR.

**Example 83** Alternating age-based and unrestricted heuristic selection is incomplete for labeled splitting just as it is for AVATAR (Example 58). To see why, start with the clause set

$$ \{p(a, y), \neg p(x, y) \lor p(s(x), y), q(a), r(x) \lor q(y) \lor \neg p(x, y), s(x) \lor \neg q(x), \neg s(x)\} $$

and always select the negative literal if there is one. The prover begins by deriving $p(s(a), y)$ and $r(a) \lor q(y)$ using the age-based heuristic. Then it heuristically selects $r(a) \lor q(y)$ and splits it. In the left branch, where $q(y)$ is enabled, $q(a)$ is locally redundant and locked. Before age-based selection allows the prover to derive $\perp$ from the clauses $s(x) \lor \neg q(x)$, $q(y)$, and $\neg s(x)$, it will also have derived $p(s(a)), y)$ and $r(s(a)) \lor q(y)$. When the prover switches back to the right branch, it can heuristically select the newly derived disjunction and split it.

This process can be repeated to give rise to infinitely many splittable clauses of the form $r(s^i(a)) \lor q(y)$. In this way, no inferences are ever performed in the rightmost branch, only splits. The clause $q(a)$, which is necessary for a refutation, is never selected for inferences; most of the time, it is even locally redundant.

## 7.3 SMT with Quantifiers

SMT solvers based on DPLL(T) [20] combine a SAT solver with theory solvers, each responsible for reasoning about a specific quantifier-free theory (e.g., equality, linear integer arithmetic). In the classical setup, the theories are decidable, and the overall solver is a decision procedure for the union of the theories. Some SMT solvers, including cvc5 [3], veriT [8], and Z3 [18], also support quantified formulas via instantiation at the expense of decidability.

Complete instantiation strategies have been developed for various fragments of first-order logic [14, 23, 24]. In particular, enumerative quantifier instantiation [23] is complete under some conditions. An SMT solver following such a strategy ought to be refutationally complete, but this has never been proved. Although SMT is quite different from the architectures we have studied so far, we can instantiate our framework to show the completeness of an abstract SMT solver. The model-guided prover MG will provide a suitable starting point, since we will need neither L's locking mechanism nor AV's given clause procedure.

Let F be the set of first-order Σ-formulas with a distinguished falsehood $\perp$. We represent the SMT solver's underlying SAT solver by the UNSAT rule and complement it with an inference system Finf that classifies formulas, detects inconsistencies up to theories excluding quantifiers, and instantiates quantifiers. For FRed, we take an arbitrary instance of the standard redundancy criterion [2, Sect. 4.2.2]. It can be used to split disjunctions destructively and to
simplify formulas. We define the “theories with quantifiers” calculus TQ = (Finf, FRed). For the consequence relations $\models$ and $\vDash$, we use entailment in the supported theories including quantifiers.

Some theories such as linear integer arithmetic are not compact and thus cannot directly be used for the consequence relation. Instead, we define $M \models_{LIA} N$ to be true if and only if there exist finite sets $M' \subseteq M$ and $N' \subseteq N$ such that $\bigwedge M' \to \bigvee N'$ is valid modulo linear integer arithmetic. For finite sets, this relation coincides with noncompact entailment: If $M$ is finite, then $M \models_{LIA} \perp$ if and only if $M$ is inconsistent modulo linear integer arithmetic. Both completeness and soundness of a concrete prover are statements about the finite set of input formulas, so using a compactified version of the consequence relation is purely an implementation detail and poses no restriction.

The clausification rules work on logical symbols outside quantifiers; they derive $C$ and $D$ from a premise $C \wedge D$, among others. The theory rules can derive $\perp$ from some finite formula set $N$ if $N \models \{\perp\}$, ignoring quantifiers; this triggers a model switch. Finally, the instantiation rules derive formulas $p(t)$ from premises $\forall x. p(x)$, where $t$ is some ground term; the instantiation strategy determines which ground terms must be tried and in which order. A lot of complexity hidden in Finf—such as purification and theory-specific data structures and algorithms—is taken as a black box.

As with AVATAR, the initial problem is expressed using $\Sigma$-formulas. We use the same approximation function as in AVATAR to represent formulas as assertions (Example 8). Abusing terminology slightly, let us call an A-formula $C \leftarrow A$ a subunit if $C$ is not a disjunction. Whenever a (ground) disjunction $C \vee D \leftarrow A$ emerges, we immediately apply SPLIT. This delegates clausal reasoning to the SAT solver. It then suffices to assume that TQ is complete for subunits.

**Theorem 84 (Dynamic completeness)** Assume TQ is statically complete for subunit sets. Let $(\partial_i, \mathcal{N}_i)_i$ be a fair $\implies_{MG}$-derivation based on TQ. If $\mathcal{N}_0 \models \{\perp\}$ and $\mathcal{N}_\infty$ contains only subunits, then $\perp \in \mathcal{N}_j$ for some $j$.

*Proof* The proof is analogous to that of Theorem 28. Because we only have conditional static completeness of (Finf, FRed), we need the assumption that $\mathcal{N}_\infty$ contains only subunits. $\square$

Care must be taken to design a practical fair strategy. Like AVATAR-based provers, SMT solvers will typically not perform all $SInf$-inferences, not even up to $SRed_1$. Given $a \approx b \leftarrow \{v_0\}$, $b \approx c \leftarrow \{v_1\}$, $a \approx d \leftarrow \{v_2\}$, $c \approx d \leftarrow \{v_3\}$, and $a \not\approx c \leftarrow \{v_4\}$, an SMT solver will find only one of the conflicts $\perp \leftarrow \{v_0, v_1, v_4\}$ or $\perp \leftarrow \{v_2, v_3, v_4\}$ but not both. This leaves us in a similar predicament as with locking: A theory conflict might be nonredundant at the limit point, even though it is redundant at every point of the derivation. The SMT solver just happened to choose the wrong conflict every time.

**Example 85** Consider the initial clause set

$$ \{\forall x (x \le 0 \lor a > x), \quad a \approx 0, \quad a + 3 < 2\} $$

Eagerly applying quantifier instantiation, we get the instances

$$ i \le 0 \leftarrow \{[i \le 0]\}, \quad a > i \leftarrow \{[a > i]\}, \quad \perp \leftarrow \{\neg[i \le 0], \neg[a > 1]\} $$

for every $i \in \mathbb{N}$. The solver then starts in a model where each $[a > i]$ is true. Here it can derive the conflict $\perp \leftarrow \{[a > 0]\}$. Then it switches to the next model where $[a > 0]$ is false, but $[a > 1]$, $[a > 2]$, etc. are true, and derive the conflict $\perp \leftarrow \{[a > 1]\}$.
Iterating this process, we see that all conflicts are of the form $[a > i]$ for some $i$. However, at the limit point—where $[a > i]$ is false for every $i$—none of these conflicts is enabled. The only conflict which exists at the limit point is between $a \approx 0$ and $a + 3 < 2$, and the solver never finds it because it detects a different conflict first.

For decidable theories, a practical fair strategy is to first clausify and detect theory conflicts and to instantiate quantifiers only if no other rules are applicable. A similar case analysis as in the proof of Lemma 77 works to establish fairness for this strategy.

First consider the case where quantifier instantiation is invoked infinitely often. Then there exists an infinite subsequence $(\mathcal{J}'_j, \mathcal{N}'_j)_j$ of states such that $(1) (\mathcal{J}'_j)_j$ converges to a limit point, and (2) no $\mathcal{N}'_j$ has a theory conflict. To prove the $\implies_{\text{MG}}$-derivation fair, we need to show that $\iota \in \text{FInf}((\mathcal{N}_\infty)_\mathcal{J})$ implies $\iota \in \text{FRed}_1((\mathcal{N}_i)_\mathcal{J})$ for every $i$. If $\iota$ is a theory conflict or clausification inference, then its finitely many premises are in $\mathcal{N}'_j$ for some $j$, contradicting the strategy. Otherwise, $\iota$ is a quantifier instantiation. Here, it suffices to ensure that A-formulas that are enabled infinitely often at a quantifier instantiation step are also fully instantiated. (Just as with AV provers, it is possible that not all limit points are saturated.)

Otherwise, quantifier instantiation is only invoked finitely often—either because every encountered model had a theory conflict, or because there was nothing to instantiate. Here, it suffices to assume that clausification is a strongly finitary simplification bound (which means that a formula can only be clausified in a finite number of ways). Under this assumption only finitely many base formulas will be derived; this implies that only a finite number of models will be considered. The last model will then be saturated due to the strategy.

There is also the question of model soundness. If the SMT solver starts with the $\Sigma$-formula set $\mathcal{N}_0$ and ends in a state $(\mathcal{J}_i, \mathcal{N}_i)$ with $\mathcal{J}_i \models (\mathcal{N}_i)_\perp$, we would like the solver to generate a model of $(\mathcal{N}_i)_{\mathcal{J}_i}$, from which a model of $\mathcal{N}_0$ can be derived. This is possible if the solver performs only sound inferences and applies APPROX systematically. Then $(\mathcal{N}_i)_{\mathcal{J}_i}$ is fully exposed to the propositional level, and $\text{fml}(\mathcal{J}_i)$ is a theory model of $\mathcal{N}_{\mathcal{J}_i}$ and therefore of $\mathcal{N}_0$.

**Example 86** Consider an SMT solver equipped with the theory of uninterpreted functions and linear arithmetic. Let

$$ \{\forall x(f(x) \approx 0 \lor g(x) \approx 0), \quad f(1) \approx 1, \quad g(1) \approx 1\} $$

be the initial clause set. The SMT solver first considers the propositional model $\mathcal{J}_0 = \neg \mathbf{V}$. There is no theory conflict, so the solver uses quantifier instantiation and clausification to derive $f(0) \approx 0 \leftarrow \{v_0\}$, $g(0) \approx 0 \leftarrow \{v_1\}$, and $\perp \leftarrow \{\neg v_0, \neg v_1\}$. We have $\mathcal{J}_0 \not\models \perp \leftarrow \{\neg v_0, \neg v_1\}$, so the solver switches to the model $\mathcal{J}_1 = (\mathcal{J}_0 \setminus \{\neg v_0\}) \cup \{v_0\}$. There is still no theory conflict, so it instantiates a quantifier again, producing the A-clauses $f(1) \approx 0 \leftarrow \{v_2\}$, $g(1) \approx 0 \leftarrow \{v_3\}$, and $\perp \leftarrow \{\neg v_2, \neg v_3\}$. The solver now switches to $\mathcal{J}_2 = (\mathcal{J}_1 \setminus \{\neg v_2\}) \cup \{v_2\}$. It derives a theory conflict $\perp \leftarrow \{v_2\}$ and switches to $\mathcal{J}_3 = (\mathcal{J}_2 \setminus \{\neg v_3\}) \cup \{v_3\}$. For this model, there is also a conflict, $\perp \leftarrow \{v_3\}$, and the solver terminates by applying UNSAT.

Our mathematization of AVATAR and SMT with quantifiers exposes their dissimilarities. With SMT, splitting is mandatory, and there is no subsumption or simplification, locking, or active and passive sets. And of course, theory inferences are $n$-ary and quantifier instantiation is unary, whereas superposition is binary. Nevertheless, their completeness follows from the same principles.
## 8 Conclusion

Our framework captures splitting calculi and provers in a general way, independently of the base calculus. Users can conveniently derive a dynamic refutational completeness result for a splitting prover based on a given statically refutationally complete calculus. As we developed the framework, we faced some tension between constraining the SAT solver's behavior and the saturation prover's. It seemed preferable to constrain the prover, because the prover is typically easier to modify than an off-the-shelf SAT solver. To our surprise, we discovered counterexamples related to locking, formula selection, and simplification, which may affect Vampire's AVATAR implementation, depending on the SAT solver and prover heuristics used. We proposed some restrictions, but alternatives could be investigated.

We found that labeled splitting can be seen as a variant of AVATAR where the SAT solver follows a strict strategy and propositional variables are not reused across branches. A benefit of the strict strategy is that locking preserves completeness. As for the relationship between AVATAR and SMT, there are some glaring differences, including that splitting is necessary to support disjunctions in SMT but fully optional in AVATAR. For future work, we could try to complete the picture by considering other related architectures [5-7, 10, 19].

**Acknowledgements** Petar Vukmirović greatly helped us design the abstract notions connected to A-formulas. Giles Reger patiently explained AVATAR and revealed some of its secrets. Simon Cruanes did the same regarding lightweight AVATAR. Simon Robillard, Martin Suda, Andrei Voronkov, Uwe Waldmann, and Christoph Weidenbach discussed splitting with us. Haniel Barbosa, Pascal Fontaine, Andrew Reynolds, and Cesare Tinelli explained some fine points of SMT. Natarajan Shankar pointed us to his work on the Shostak procedure. Ahmed Bhayat, Nicolas Peltier, Martin Suda, Mark Summerfield, Dmitriy Traytel, Petar Vukmirović, and the anonymous reviewers suggested textual improvements. We thank them all.

This research has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). The research has also received funding from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

## References

1. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217-247 (1994)

2. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. I, pp. 19-99. Elsevier (2001)

3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: G. Gopalakrishnan, S. Qadeer (eds.) CAV 2011, LNCS, vol. 6806, pp. 171-177. Springer (2011)

4. Bjø[r]ner, N., Reger, G., Suda, M., Voronkov, A.: AVATAR modulo theories. In: C. Benzmüller, G. Sutcliffe, R. Rojas (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 39-52. EasyChair (2016)

5. Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Satisfiability modulo theories and assignments. In: L. de Moura (ed.) CADE-26, LNCS, vol. 10395, pp. 42-59. Springer (2017)

6. Bonacina, M.P., Lynch, C., de Moura, L.: On deciding satisfiability by DPLL($Γ + T$) and unsound theorem proving. In: R.A. Schmidt (ed.) CADE-22, LNCS, vol. 5663, pp. 35-50. Springer (2009)

7. Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: An exposition. In: S. Schulz, L. de Moura, B. Konev (eds.) PAAR-2014, EPiC Series in Computing, vol. 31, pp. 25-38. EasyChair (2014)

8. Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: R.A. Schmidt (ed.) CADE-22, LNCS, vol. 5663, pp. 151-156. Springer (2009)

9. Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique (2015)

10. Déharbe, D., Fontaine, P., Ranise, S., Ringeissen, C.: Decision procedures for the formal analysis of software. In: K. Barkaoui, A. Cavalcanti, A. Cerone (eds.) ICTAC 2006, LNCS, vol. 4281, pp. 366-370. Springer (2006)
11. Ebner, G., Blanchette, J., Tourret, S.: A unifying splitting framework. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS, vol. 12699, pp. 344–360. Springer (2021)

12. Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1(ICFP), 34:1–34:29 (2017)

13. Fietzke, A., Weidenbach, C.: Labelled splitting. Ann. Math. Artif. Intell. 55(1–2), 3–34 (2009)

14. Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: A. Bouajjani, O. Maler (eds.) CAV 2009, LNCS, vol. 5643, pp. 306–320. Springer (2009)

15. Gleiss, B., Kovács, L., Rath, J.: Subsumption demodulation in first-order theorem proving. In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 297–315. Springer (2020)

16. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: J. Leech (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)

17. McCune, W., Wos, L.: Otter—the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997)

18. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: C.R. Ramakrishnan, J. Rehof (eds.) TACAS 2008, LNCS, vol. 4963, pp. 337–340. Springer (2008)

19. de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: R. Giacobazzi, J. Berdine, I. Mastroeni (eds.) VMCAI 2013, LNCS, vol. 7737, pp. 1–12. Springer (2013)

20. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

21. Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer (2014)

22. Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: A.P. Felty, A. Middeldorp (eds.) CADE-25, LNCS, vol. 9195, pp. 399–415. Springer (2015)

23. Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: D. Beyer, M. Huisman (eds.) TACAS 2018, LNCS, vol. 10806, pp. 112–131. Springer (2018)

24. Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: N. Sharygina, H. Veith (eds.) CAV 2013, LNCS, vol. 8044, pp. 640–655. Springer (2013)

25. Riazanov, A., Voronkov, A.: Splitting without backtracking. In: B. Nebel (ed.) IJCAI 2001, pp. 611–617. Morgan Kaufmann (2001)

26. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)

27. Schlichtkrull, A., Blanchette, J.C., Traytel, D.: A verified prover based on ordered resolution. In: A. Mahboubi, M.O. Myreen (eds.) CPP 2019, pp. 152–165. ACM (2019)

28. Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: A. Biere, R. Bloem (eds.) CAV 2014, LNCS, vol. 8559, pp. 696–710. Springer (2014)

29. Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 316–334. Springer (2020)

30. Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving (technical report). Technical report (2020). https://matryoshka-project.github.io/pubs/saturate_report.pdf

31. Weidenbach, C.: Combining superposition, sorts and splitting. In: A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. II, pp. 1965–2013. Elsevier and MIT Press (2001)

32. Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER version 0.42. In: M.A. McRobbie, J.K. Slaney (eds.) CADE-13, Lecture Notes in Computer Science, vol. 1104, pp. 141–145. Springer (1996)