# A Comprehensive Framework for Saturation Theorem Proving

Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette

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

## To cite this version:

Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. A Comprehensive Framework for Saturation Theorem Proving. Journal of Automated Reasoning, 2022, 66 (4), pp.499-539. 10.1007/s10817-022-09621-7. hal-03909983

HAL Id: hal-03909983

https://inria.hal.science/hal-03909983

Submitted on 21 Dec 2022

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Comprehensive Framework for Saturation Theorem Proving

Uwe Waldmann · Sophie Tourret · Simon Robillard · Jasmin Blanchette

Received: date / Accepted: date

**Abstract** A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance $C \sigma$ redundant.

We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.

## 1 Introduction

Saturation is one of the most successful approaches to automatic theorem proving. Provers based on resolution, superposition, and related proof calculi all implement some saturation procedure that systematically derives conclusions of inferences up to a redundancy criterion.

<footnote>U. Waldmann · S. Tourret · J. Blanchette
Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany
E-mail: {uwe,tourret,jblanche} @ mpi-inf.mpg.de</footnote>

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

<footnote>S. Robillard
LIRMM, Université de Montpellier, CNRS, Montpellier, France
E-mail: simon.robillard@umontpellier.fr</footnote>

<footnote>J. Blanchette
Vrije Universiteit Amsterdam, Amsterdam, the Netherlands
E-mail: j.c.blanchette@vu.nl</footnote>
More specifically, a saturation prover starts with a problem to refute, typically given as a set of clauses, and draws inferences from the clauses, adding the conclusions to the set. The prover may remove redundant clauses at any point. The refutation attempt ends as soon as the empty clause $⊥$, denoting a contradiction, has been derived. The proof calculus specifies which inferences need to be performed and which clauses are redundant.

In their *Handbook of Automated Reasoning* chapter [6, Section 4], Bachmair and Ganzinger remark that “unfortunately, comparatively little effort has been devoted to a formal analysis of redundancy and other fundamental concepts of theorem proving strategies, while more emphasis has been placed on investigating the refutational completeness of a variety of modifications of inference rules, such as resolution.” As a remedy, they present an abstract framework for saturation up to redundancy. Briefly, theorem proving derivations take the form $N_0▷N_1▷…$, where $N_0$ is the initial clause set and each step either adds inferred clauses or deletes redundant clauses. Given a suitable notion of fairness, the limit $N_∞$ of a fair derivation is saturated up to redundancy. If the calculus is refutationally complete and $N_∞$ does not contain $⊥$, then $N_0$ has a model. We will refer to the calculus’ refutational completeness as *static* as opposed to a prover’s *dynamic* completeness.

Bachmair and Ganzinger also define a concrete prover, RP, based on a first-order ordered resolution calculus and the given clause procedure. However, like all realistic resolution provers, RP implements subsumption deletion: It will delete a clause *C* if it is subsumed by another clause *C'*, meaning that $C = C'σ ∨ D$ for some substitution σ and some clause *D*. Yet the case where *D* = $⊥$ is not covered by the standard definition of redundancy, according to which a clause *C* is redundant w.r.t. a clause set *N* if all its ground instances $Cθ$ are entailed by *strictly* smaller ground instances of clauses belonging to *N*. Concretely, we would like $P(x)$ to make $P(a)$ redundant, but this fails because the instance of $P(x)$ that entails $P(a)$, namely $P(a)$ itself, is not strictly smaller than $P(a)$. As a result, RP-derivations are *not* $▷$-derivations, and Bachmair and Ganzinger’s saturation framework is *not* applicable.

There are two ways to address this problem. In the *Handbook*, Bachmair and Ganzinger start from scratch and prove the dynamic refutational completeness of RP by relating nonground derivations to ground derivations. This proof, though, turns out to be rather nonmodular—it refers simultaneously to properties of the calculus, to properties of the prover, and to the fairness of the derivations. Extending it to other calculi or prover architectures would be costly. For this reason, most authors stop after proving static refutational completeness of their calculi.

An alternative approach is to extend the redundancy criterion so that subsumed clauses become redundant. As demonstrated by Bachmair and Ganzinger in 1990 [3], this is possible by redefining redundancy in terms of closures (*C*, $θ$) instead of ground instances $Cθ$. We show that this approach can be generalized and modularized: First, any redundancy criterion that is obtained by lifting a ground criterion can be extended to a redundancy criterion that supports subsumption without affecting static refutational completeness. Second, by applying this property to labeled formulas, it becomes possible to give generic completeness proofs for prover architectures in a straightforward way.

Most saturation provers implement a variant of the given clause procedure. We present an abstract version of the procedure that can be refined to obtain an Otter [28] or DISCOUNT [1] loop, and we prove it refutationally complete. We also present a generalization that decouples scheduling and computation of inferences, to support *orphan formula deletion* and *inference dovetailing*. A formula is an orphan when it has lost one of its parents to the redundancy criterion [24, 39]; removing such formulas reduces the search space. Dovetailing makes it possible to support infinitary inference rules, such as $λ$-superposition and its possibly infinite sequences of higher-order unifiers [13].
When users of the framework instantiate these prover architectures with a concrete saturation calculus, they obtain the dynamic refutational completeness of the combination from the properties of the prover architecture and the static refutational completeness proof for the calculus. The framework is applicable to a wide range of calculi, including ordered resolution [6], unfailing completion [2], standard superposition [5], constraint superposition [29], theory superposition [44], and hierarchic superposition [8]. It is already used in several published and ongoing works on combinatory superposition [15], $\lambda$-free superposition [14], $\lambda$-superposition [12, 13], superposition with interpreted Booleans [33], AVATAR-style splitting [21], and superposition with SAT-inspired inprocessing [43].

When Schlichtkrull, Blanchette, Traytel, and Waldmann [36] mechanized Bachmair and Ganzinger's chapter using the Isabelle/HOL proof assistant [32], they found quite a few mistakes, including one that compromised RP's dynamic refutational completeness [36, Section 7.1]. This motivated us to mechanize our framework as well.

This article is structured as follows:

- Section 2 introduces the basic notions of Bachmair-Ganzinger-style saturation theorem proving, which also form the basis of our framework. These include the notions of inferences, redundancy, and static and dynamic refutational completeness.

- Section 3 shows how to lift the refutational completeness of a ground calculus to the nonground level. This step adds support for subsumption and formula labels.

- Section 4 presents several prover architectures that are variants of the given clause procedure, showing how to cope with multiple formula sets.

- Section 5 briefly describes the Isabelle mechanization of the framework.

An earlier version of this work was presented at IJCAR 2020 [45]. This article extends the IJCAR paper with detailed proofs, more explanations and examples, and an index. The Isabelle mechanization is described in more detail in a CPP 2021 paper [41].

## 2 Preliminaries

Our framework is parameterized by abstract notions of formulas, inferences, and redundancy criteria, defined below. We also introduce various auxiliary concepts, notably static and dynamic refutational completeness, and study variations found in the literature.

### 2.1 Inferences and Redundancy

A set $\mathbf{F}$ of formulas is a nonempty set with a nonempty subset $\mathbf{F}_{\perp} \subseteq \mathbf{F}$. Elements of $\mathbf{F}_{\perp}$ represent false. Typically, $\mathbf{F}_{\perp}$ is a singleton—i.e., $\mathbf{F}_{\perp} = \{\perp\}$. The possibility to distinguish between several false elements will be useful when we model concrete prover architectures, where different elements of $\mathbf{F}_{\perp}$ represent different situations in which a contradiction has been derived.

A consequence relation $\models$ over $\mathbf{F}$ is a relation $\models \subseteq \mathcal{P}(\mathbf{F}) \times \mathcal{P}(\mathbf{F})$ with the following properties for all $N_1, N_2, N_3 \subseteq \mathbf{F}$:

(C1) $\{\perp\} \models N_1$ for every $\perp \in \mathbf{F}_{\perp}$;

(C2) $N_2 \subseteq N_1$ implies $N_1 \models N_2$;

(C3) if $N_1 \models \{C\}$ for every $C \in N_2$, then $N_1 \models N_2$;

(C4) if $N_1 \models N_2$ and $N_2 \models N_3$, then $N_1 \models N_3$.
It is easy to show that $N_1 \models N_2$ if and only if $N_1 \models \{C\}$ for every $C \in N_2$, and that $N \models \bigcup_{i \in I} N_i$ if and only if $N \models N_i$ for every $i \in I$. Moreover, all elements of $\mathbf{F}_{\perp}$ are logically equivalent: If $N \models \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$, then $N \models \{\perp'\}$ for every $\perp' \in \mathbf{F}_{\perp}$.

Consequence relations are used (1) when one discusses the soundness of a calculus (and hence, when we justify the addition of formulas) and (2) when one discusses the refutational completeness of a calculus (and hence, when we justify the deletion of redundant formulas). Perhaps unexpectedly, the consequence relations used for these purposes may be different ones. A typical example is theory superposition, where one may use entailment w.r.t. all theory axioms for (1), but only entailment w.r.t. a subset of the (instances of the) theory axioms for (2). Another example is constraint superposition, where one uses entailment w.r.t. the set of all ground instances for (1), but entailment w.r.t. a subset of those instances for (2). Typically, the consequence relation $\cong$ used for (1) is the intended one, and some additional calculus-dependent argument is necessary to show that refutational completeness w.r.t. the consequence relation $\models$ used for (2) implies refutational completeness w.r.t. $\cong$.

An **F-inference** $\iota$ is a tuple $(C_n, \dots, C_0) \in \mathbf{F}^{n+1}$, $n \ge 0$. The formulas $C_n, \dots, C_1$ are called *premises of* $\iota$; $C_0$ is called the *conclusion of* $\iota$, denoted by $\mathrm{concl}(\iota)$. An **F-inference system Inf** is a set of **F-inferences**. If $N \subseteq \mathbf{F}$, we write $\mathrm{Inf}(N)$ for the set of all inferences in $\mathrm{Inf}$ whose premises are contained in $N$. We write $\mathrm{Inf}(N, M) := \mathrm{Inf}(N \cup M) \setminus \mathrm{Inf}(N \setminus M)$ for the set of all inferences in $\mathrm{Inf}$ such that one premise is in $M$ (and possibly in $N$ as well) and the other premises are contained in $N \cup M$.

One can find several slightly differing definitions for redundancy criteria, fairness, and saturation in the literature [6, 8, 44]. We discuss the differences in Section 2.3. Here we mostly follow Waldmann [44].

A *redundancy criterion* for an inference system *Inf* and a consequence relation $\models$ is a pair *Red* = (*Red*<sub>*I*</sub>, *Red*<sub>*F*</sub>), where *Red*<sub>*I*</sub> : $\mathcal{P}(\mathbf{F}) \to \mathcal{P}(\mathrm{Inf})$ and *Red*<sub>*F*</sub> : $\mathcal{P}(\mathbf{F}) \to \mathcal{P}(\mathbf{F})$ are mappings from sets of formulas to sets of inferences and from sets of formulas to sets of formulas that satisfy the following conditions for all sets of formulas *N* and *N*':

(R1) if $N \models \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$, then $N \setminus \mathrm{Red}_{\mathbf{F}}(N) \models \{\perp\}$;

(R2) if $N \subseteq N'$, then $\mathrm{Red}_{\mathbf{F}}(N) \subseteq \mathrm{Red}_{\mathbf{F}}(N')$ and $\mathrm{Red}_{I}(N) \subseteq \mathrm{Red}_{I}(N')$;

(R3) if $N' \subseteq \mathrm{Red}_{\mathbf{F}}(N)$, then $\mathrm{Red}_{\mathbf{F}}(N) \subseteq \mathrm{Red}_{\mathbf{F}}(N \setminus N')$ and $\mathrm{Red}_{I}(N) \subseteq \mathrm{Red}_{I}(N \setminus N')$;

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

Inferences in $\mathrm{Red}_1(N)$ and formulas in $\mathrm{Red}_F(N)$ are called *redundant* w.r.t. $N$. In a prover, $\mathrm{Red}_1$ indicates which inferences need not be performed (e.g., because they have already been performed), whereas $\mathrm{Red}_F$ justifies the deletion and simplification of formulas. Intuitively, (R1) states that deleting redundant formulas preserves inconsistency. (R2) and (R3) state that formulas or inferences that are redundant w.r.t. a set $N$ remain redundant if arbitrary formulas are added to $N$ or redundant formulas are deleted from $N$. (R4) ensures that computing an inference makes it redundant. Note that $C \in \mathrm{Red}_F(\{C\})$ generally does not hold.

The connection between redundant inferences and redundant formulas is given by the second part of (R3). Together with (R4) it implies that inferences with a redundant conclusion are themselves redundant:

**Lemma 1** If $\iota \in \mathrm{Inf}$ and $\mathrm{concl}(\iota) \in \mathrm{Red}_F(N)$, then $\iota \in \mathrm{Red}_1(N)$.

*Proof* Let $\iota \in \mathrm{Inf}$ and $\mathrm{concl}(\iota) \in \mathrm{Red}_F(N)$. Then $\iota \in \mathrm{Red}_1(\mathrm{Red}_F(N)) \subseteq \mathrm{Red}_1(N \cup \mathrm{Red}_F(N))$. Since $\mathrm{Red}_F(N) \setminus N \subseteq \mathrm{Red}_F(N) \subseteq \mathrm{Red}_F(N \cup \mathrm{Red}_F(N))$, we obtain $\iota \in \mathrm{Red}_1(N \cup \mathrm{Red}_F(N)) \subseteq \mathrm{Red}_1((N \cup \mathrm{Red}_F(N)) \setminus (\mathrm{Red}_F(N) \setminus N)) = \mathrm{Red}_I(N)$. $\square$
Redundant inferences will play a central role in the definition of saturation and refutational completeness in Section 2.2.

**Example 2** The trivial redundancy criterion defined by $Red_1(N) = \{\iota \in Inf | concl(\iota) \in N\}$ and $Red_F(N) = \emptyset$ clearly meets requirements (R1)–(R4). According to this criterion, an inference becomes redundant once its conclusion has been added to the set of formulas (e.g., by performing the inference), whereas formulas are never redundant.

**Example 3** Assume $\models$ to be compact—i.e., $N \models \{C\}$ implies that $M \models \{C\}$ for some finite $M \subseteq N$. Given a well-founded ordering $>_{\models}$ on $\mathbf{F}$ and an inference system $Inf$ that satisfies $C_1 >_{\models} C_0$ for all $(C_n, \dots, C_1, C_0) \in Inf$, the standard redundancy criterion defined by

$$Red_1(N) := \{ (C_n, \dots, C_1, C_0) \in Inf \mid \{C_n, \dots, C_2\} \cup \{D \in N \mid C_1 >_{\models} D\} \models \{C_0\} \}$$

$$Red_F(N) := \{ C \in \mathbf{F} \mid \{D \in N \mid C >_{\models} D\} \models \{C\} \}$$

also meets requirements (R1)–(R4) [6, Section 4.2]. Intuitively, a formula is redundant if it is entailed by $>_{\models}$-smaller formulas in $N$, whereas an inference is redundant if it is entailed by the side premises $C_n, \dots, C_2$ together with some formulas $M \subseteq N$ that are $>_{\models}$-smaller than the main premise $C_1$. This criterion is used in conjunction with ordered resolution and superposition. Some authors require the subsets $M$ to be finite but this is not necessary if $\models$ is compact. $Inf$ often satisfies $C_1 >_{\models} C_k$ for all $k > 1$; the definition of $Red_1$ can then be simplified to $Red_1(N) := \{(C_n, \dots, C_1, C_0) \in Inf \mid \{D \in N \mid C_1 >_{\models} D\} \models \{C_0\}\}$.

**Example 4** It is always possible to conflate redundant inferences and formulas by defining $Red_1$ such that $\iota \in Red_1(N)$ if and only if $\iota \in Inf$ and $concl(\iota) \in N \cup Red_F(N)$ for all $\iota$ and $N$. This is, however, needlessly weak for many calculi. Consider superposition, which is based on the standard redundancy criterion. Let $d > c > b > a$ be the atom ordering, and assume the premises of the superposition inference

$$\frac{\frac{d \approx b \quad d \approx c \lor d \approx a}{b \approx c \lor d \approx a}}{d \approx b}$$

are in the clause set. Instead of performing the inference, we would like to exhaustively rewrite the second premise using the first premise, to $b \approx c \lor b \approx a$, using either demodulation or a simultaneous superposition inference [11]. Notice that the conclusion does not become redundant in this way: It is entailed by $b \approx c \lor b \approx a$ and $d \approx b$, but $d \approx b$ is $>_{\models}$-larger than the conclusion and cannot be used. Nevertheless, with the standard redundancy criterion, the superposition inference becomes redundant, since the clause $d \approx b$ is smaller than the larger premise of the inference.

## 2.2 Refutational Completeness

Let $\models$ be a consequence relation, let $Inf$ be an inference system, and let $Red$ be a redundancy criterion for $\models$ and $Inf$.

A set $N \subseteq \mathbf{F}$ is called saturated w.r.t. $Inf$ and $Red$ if $Inf(N) \subseteq Red_1(N)$. The pair $(Inf, Red)$ is called statically refutationally complete w.r.t. $\models$ if for every saturated set $N \subseteq \mathbf{F}$ such that $N \models \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$, there exists a $\perp' \in \mathbf{F}_{\perp}$ such that $\perp' \in N$.

Let $A$ be a set. An $A$-sequence is a finite sequence $(a_i)_{i=0}^k = a_0, a_1, \dots, a_k$ or an infinite sequence $(a_i)_{i=0}^{\infty} = a_0, a_1, \dots$ with $a_i \in A$ for all indices $i$. We use the notation $(a_i)_{i \ge 0}$ or $(a_i)_i$ for both finite and infinite sequences. A nonempty sequence $(a_i)_i$ can be decomposed
into a head $a_0$ and a tail $(a_i)_{i \ge 1}$. Given a relation $\triangleright \subseteq A \times A$, a $\triangleright$-derivation is a nonempty $A$-sequence such that $a_i \triangleright a_{i+1}$ for all valid indices.

We define the relation $\triangleright_{Red} \subseteq \mathcal{P}(\mathbf{F}) \times \mathcal{P}(\mathbf{F})$ such that $N \triangleright_{Red} N'$ if and only if $N \setminus N' \subseteq Red_F(N')$. In other words, when taking a transition, we may add arbitrary formulas $(N' \setminus N)$ and remove redundant formulas $(N \setminus N')$. In practice, the added formulas would normally be entailed by $N$. But since our framework is designed to establish only dynamic refutational completeness, we impose no soundness restrictions on added formulas. If dynamic soundness of a prover is desired, it can be derived immediately from the soundness of the inferences and does not require its own framework.

Let $(N_i)_i$ be a $\mathcal{P}(\mathbf{F})$-sequence. Its limit (inferior) is the set $N_\infty := \bigcup_i \bigcap_{j \ge i} N_j$. The limit consists of the persistent formulas: These are formulas that eventually emerge in some $N_i$ and remain present in all the following sets $N_j$ with $j \ge i$. The sequence is called (weakly) fair if $\text{Inf}(N_\infty) \subseteq \bigcup_i Red_1(N_i)$. The pair $(\text{Inf}, \text{Red})$ is called dynamically refutationally complete w.r.t. $\models$ if for every fair $\triangleright_{Red}$-derivation $(N_i)_i$ such that $N_0 \models \{\perp\}$ for some $\perp \in \mathbf{F}_\perp$, we have $\perp' \in N_i$ for some $i$ and some $\perp' \in \mathbf{F}_\perp$.

**Example 5** Let $\Sigma$ be a signature consisting of a binary predicate $P$, a unary function $f$, and a constant $a$. Let $\text{Inf}$ be the set of inferences of the ordered resolution calculus with selection on $\Sigma$-clauses, and let $\text{Red}$ be the trivial redundancy criterion (Example 2). This calculus is refutationally complete [6, Section 3].

Consider the initial set $N = \{\mathcal{P}(a, a), \neg\mathcal{P}(x, x), \mathcal{P}(f(x), y) \lor \neg\mathcal{P}(x, y)\}$, where the second literal of the third clause is selected and no other literals are selected. The inference $\iota = (\neg\mathcal{P}(x, x), \mathcal{P}(a, a), \perp)$ belongs to $\text{Inf}(N)$ and derives $\perp$, so $N$ is clearly unsatisfiable. However, without fairness, a derivation may never perform this inference. One such example is the infinite derivation

$$N \triangleright_{Red} N \cup \{\mathcal{P}(f(a), a)\} \triangleright_{Red} N \cup \{\mathcal{P}(f(a), a), \mathcal{P}(f(f(a)), a)\} \triangleright_{Red} \dots$$

where the clause $\neg\mathcal{P}(x, x)$ is always ignored in favor of inferences between $\mathcal{P}(f(x), y) \lor \neg\mathcal{P}(x, y)$ and a clause of the form $\mathcal{P}(f^1(a), a)$. This derivation is not fair because $\iota \in \text{Inf}(N_\infty)$, where $N_\infty = N \cup \{\mathcal{P}(f^1(a), a)\}_{i \in \mathbb{N}}$, but $\iota \notin \bigcup_i Red_1(N_i)$. In contrast, any derivation that is similar to the previous one but that performs the inference $\iota$ at some step would be fair.

Now consider the satisfiable set $N' = \{\mathcal{P}(a, a), \mathcal{P}(f(x), y) \lor \neg\mathcal{P}(x, y)\}$. The derivation

$$N' \triangleright_{Red} N' \cup \{\mathcal{P}(f(a), a)\} \triangleright_{Red} N' \cup \{\mathcal{P}(f(a), a), \mathcal{P}(f(f(a)), a)\} \triangleright_{Red} \dots$$

is clearly fair.

Using properties (R1)–(R3), it is possible to show that static and dynamic refutational completeness agree [6]:

**Lemma 6** If $(N_i)_i$ is a $\triangleright_{Red}$-derivation, then $(\bigcup_i N_i) \setminus N_\infty \subseteq Red_F(\bigcup_i N_i)$.

*Proof* If $C \in (\bigcup_i N_i) \setminus N_\infty$, then there must exist some $i$ such that $C \in N_i \setminus N_{i+1}$. Consequently, $C \in Red_F(N_{i+1})$. By property (R2), $C \in Red_F(\bigcup_i N_i)$. $\square$

**Lemma 7** If $(N_i)_i$ is a $\triangleright_{Red}$-derivation, then $Red_1(N_i) \subseteq Red_1(N_\infty)$ and $Red_F(N_i) \subseteq Red_F(N_\infty)$ for every $i$.

*Proof* By property (R2), $Red_1(N_i) \subseteq Red_1(\bigcup_i N_i)$; by Lemma 6 and property (R3), $Red_1(\bigcup_i N_i) \subseteq Red_1((\bigcup_i N_i) \setminus ((\bigcup_i N_i) \setminus N_\infty)) = Red_1(N_\infty)$. Analogously, $Red_F(N_i) \subseteq Red_F(\bigcup_i N_i) \subseteq Red_F((\bigcup_i N_i) \setminus ((\bigcup_i N_i) \setminus N_\infty)) = Red_F(N_\infty)$. $\square$
**Lemma 8** If $(N_i)_i$ is a $\triangleright_{Red}$-derivation, then $N_i \subseteq N_\infty \cup Red_F(N_\infty)$ for every $i$.

*Proof* Let $C \in N_i$. If $C \notin N_\infty$, then there exists some $j \ge i$ such that $C \in N_j \setminus N_{j+1}$. Consequently, $C \in Red_F(N_{j+1})$ and therefore $C \in Red_F(N_\infty)$ by Lemma 7. $\square$

**Lemma 9** If $(N_i)_i$ is a fair $\triangleright_{Red}$-derivation, then the limit $N_\infty$ is saturated w.r.t. Inf and Red.

*Proof* By fairness, every $\iota \in Inf(N_\infty)$ is contained in $\cup_i Red_1(N_i)$, so there exists some $i$ such that $\iota \in Red_1(N_i)$, and thus $\iota \in Red_1(N_\infty)$ by Lemma 7. $\square$

Since fairness implies saturation of the limit, we could imagine simplifying the theory by defining dynamic refutational completeness in terms of derivations with saturated limits, instead of in terms of fair derivations. However, fairness more closely captures how provers work and is therefore easier to establish. A prover may delete formulas at different moments, without knowing the limit. This intuition is captured by the right-hand side $\cup_i Red_1(N_i)$ of the definition of fairness.

**Lemma 10** If (Inf,Red) is statically refutationally complete w.r.t. $\models$, then it is dynamically refutationally complete w.r.t. $\models$.

*Proof* Assume (Inf,Red) is statically refutationally complete w.r.t. $\models$, and let $(N_i)_i$ be a $\triangleright_{Red}$-derivation. Assume that $N_0 \models \{\perp\}$ for some $\perp \in F_\perp$. Since $N_0 \subseteq \cup_i N_i$, we get $\cup_i N_i \models N_0 \models \{\perp\}$, and by property (R1), this implies $(\cup_i N_i) \setminus Red_F(\cup_i N_i) \models \{\perp\}$. By Lemma 6, we know that $(\cup_i N_i) \setminus N_\infty \subseteq Red_F(\cup_i N_i)$, or equivalently, $(\cup_i N_i) \setminus Red_F(\cup_i N_i) \subseteq N_\infty$; hence $N_\infty \models (\cup_i N_i) \setminus Red_F(\cup_i N_i) \models \{\perp\}$.

If the sequence is fair, then $N_\infty$ is saturated, so by static refutational completeness, $\perp' \in N_\infty$ for some $\perp' \in F_\perp$. Consequently, $\perp' \in N_i$ for some $i$, implying dynamic refutational completeness. $\square$

In fact, the converse holds as well:

**Lemma 11** If (Inf,Red) is dynamically refutationally complete w.r.t. $\models$, then it is statically refutationally complete w.r.t. $\models$.

*Proof* Assume (Inf,Red) is dynamically refutationally complete w.r.t. $\models$, and let $N_0 \subseteq F$ be saturated w.r.t. Inf and Red. Assume that $N_0 \models \perp$ for some $\perp \in F_\perp$. Now consider the one-element sequence $(N_i)_{i=0}^0$. Since $N_\infty = N_0$ and $N_0$ is saturated, we know that $Inf(N_\infty) = Inf(N_0) \subseteq Red_1(N_0) = \cup_i Red_1(N_i)$, so the sequence is fair. By dynamic refutational completeness, this implies $\perp' \in N_0$ for some $\perp' \in F_\perp$. Therefore (Inf,Red) is statically refutationally complete. $\square$

**Example 12** Some popular preprocessing techniques, such as pure literal elimination and blocked clause elimination [26], are not covered by redundancy. These require inspecting the entire formula set and are not compatible with (R2). For example, P is pure in $\{P\}$ but not in the larger set $\{P, \neg P\}$.

In some situations, we may wish to apply techniques that delete clauses even if they are not redundant. If such techniques are used at most finitely many times, we can incorporate them in the framework by letting the initial set $N_0$ correspond to the set of formulas after all inprocessing has been performed, effectively considering all the transitions that happened before $N_0$ as one big preprocessing step. For example, a first-order prover might discover a clause that contains a pure predicate symbol (a predicate symbol that always occurs with the same polarity in the clause set) and delete it. If the signature is finite, this can be done only finitely many times and is hence compatible with the framework. We only need to show that inprocessing preserves unsatisfiability.
## 2.3 Variations on a Theme

For some of the notions in Sections 2.1 and 2.2 one can find alternative definitions in the literature.

**Redundancy Criteria** As in Bachmair and Ganzinger's chapter [6, Section 4.1], we have specified in condition (R1) of redundancy criteria that the deletion of redundant formulas must preserve inconsistency. Alternatively, one can require that redundant formulas must be entailed by the nonredundant ones—i.e., $N \setminus Red_F(N) \models Red_F(N)$—leading to some obvious changes in Lemmas 10 and 37.

Bachmair and Ganzinger's definition of a redundancy criterion differs from ours in that they require only conditions (R1)–(R3). They call a redundancy criterion *effective* if an inference $\iota \in Inf$ is in $Red_I(N)$ whenever $concl(\iota) \in N \cup Red_F(N)$. As demonstrated by Lemma 1, that condition is equivalent to our condition (R4).

**Inferences from Redundant Premises** Inferences from redundant premises are sometimes excluded in the definitions of saturation, fairness, and refutational completeness [6], and sometimes not [5, 10, 30, 44].<fnref n="1" /> Similarly, redundancy of inferences is sometimes defined in such a way that inferences from redundant premises are necessarily redundant themselves [5, 10], and sometimes not [6, 30, 44]. There are good arguments for each of these choices. On the one hand, one can argue that the saturation of a set of formulas should not depend on the presence or absence of redundant formulas, and that inferences from redundant formulas should be redundant as well. On the other hand, in any reasonable proof system, formulas are deleted from the set of formulas as soon as they are shown to be redundant, so why should we care whether the set is saturated even if we do not delete formulas that have been proved to be redundant?

To clarify how the different definitions found in the literature relate to each other, we define “reduced” variants of the definitions in Sections 2.1 and 2.2. A set $N \subseteq \mathbf{F}$ is called *reducedly saturated* w.r.t. $Inf$ and $Red$ if $Inf(N \setminus Red_F(N)) \subseteq Red_I(N)$. The pair $(Inf, Red)$ is *reducedly statically refutationally complete* w.r.t. $\models$ if for every reducedly saturated set $N \subseteq \mathbf{F}$ with $N \models \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$, there exists a $\perp' \in \mathbf{F}_{\perp}$ such that $\perp' \in N$. A sequence $(N_i)_i$ is called *reducedly fair* if $Inf(N_\infty \setminus \bigcup_i Red_F(N_i)) \subseteq \bigcup_i Red_I(N_i)$. The pair $(Inf, Red)$ is *reducedly dynamically refutationally complete* w.r.t. $\models$ if for every reducedly fair $\triangleright_{Red-}$ derivation $(N_i)_i$ such that $N_0 \models \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$, we have $\perp' \in N_i$ for some $i$ and some $\perp' \in \mathbf{F}_{\perp}$. A *reduced redundancy criterion* for $\models$ and $Inf$ is a redundancy criterion $Red = (Red_I, Red_F)$ that additionally satisfies $Inf(\mathbf{F}, Red_F(N)) \subseteq Red_I(N)$ for every $N \subseteq \mathbf{F}$. Recall that $Inf(N, M)$ denotes the set of $Inf$-inferences with at least one premise in $M$ and the others in $N \cup M$.

For reduced redundancy criteria, saturation and reduced saturation agree:

**Lemma 13** If $Red$ is a reduced redundancy criterion, then $N$ is saturated w.r.t. $Inf$ and $Red$ if and only if $N$ is reducedly saturated w.r.t. $Inf$ and $Red$.

*Proof* If $N$ is saturated w.r.t. $Inf$ and $Red$, then $Inf(N) \subseteq Red_I(N)$, so $Inf(N \setminus Red_F(N)) \subseteq Inf(N) \subseteq Red_I(N)$, which implies that $N$ is reducedly saturated w.r.t. $Inf$ and $Red$.

<footnote n="1">¹ Note that Bachmair and Ganzinger's *J. Log. Comput.* article [5] uses a terminology that differs from most later publications in this area: Their “composite” corresponds to “redundant,” and their “complete” corresponds to “saturated.”</footnote>
Conversely, assume that $N$ is reducedly saturated w.r.t. Inf and Red—i.e., $Inf(N \ \ Red_F(N)) \subseteq Red_I(N)$. Let $\iota \in Inf(N)$. If no premise of $\iota$ is contained in $Red_F(N)$, then $\iota \in Inf(N \ \ Red_F(N)) \subseteq Red_I(N)$. Otherwise $\iota \in Inf(F, Red_F(N))$, and since Red is reduced, we get again $\iota \in Red_I(N)$. $\square$

**Corollary 14** If Red is a reduced redundancy criterion, then (Inf, Red) is statically refutationally complete if and only if it is reducedly statically refutationally complete.

An arbitrary redundancy criterion $Red = (Red_1, Red_F)$ can always be extended to a reduced redundancy criterion $Red' = (Red'_1, Red_F)$, where $Red'_1$ is defined by $Red'_1(N) := Red_I(N) \cup Inf(F, Red_F(N))$ for all $N$.

**Lemma 15** $Red'$ is a reduced redundancy criterion.

*Proof* Since $Red_F$ is left unchanged, (R1) and the first parts of (R2) and (R3) are obvious. (R4) holds because $\iota \in Red_I(N) \subseteq Red'_I(N)$ for every inference $\iota$ with $concl(\iota) \in N$. Moreover, $Red'$ is clearly reduced. It remains to prove the second parts of (R2) and (R3).

For (R2), assume $N \subseteq N'$. Then $Red_I(N) \subseteq Red_I(N')$ and $Red_F(N) \subseteq Red_F(N')$. Moreover, Inf is clearly monotonic, so $Inf(F, Red_F(N)) \subseteq Inf(F, Red_F(N'))$, and therefore $Red'_I(N) \subseteq Red'_I(N')$.

For (R3), assume $N' \subseteq Red_F(N)$. Then $Red_F(N) \subseteq Red_F(N \setminus N')$ and $Red_I(N) \subseteq Red_I(N \setminus N')$. By monotonicity of Inf, we have $Inf(F, Red_F(N)) \subseteq Inf(F, Red_F(N \setminus N'))$, so $Red'_I(N) \subseteq Red'_I(N \setminus N')$. $\square$

**Lemma 16** If $N \subseteq F$ is saturated w.r.t. Inf and Red, then $N$ is saturated w.r.t. Inf and $Red'$.

*Proof* Since $Red_I(N) \subseteq Red'_I(N)$, $Inf(N) \subseteq Red_I(N)$ implies $Inf(N) \subseteq Red'_I(N)$. $\square$

The converse does not hold:

**Example 17** Consider a signature consisting of the four propositional variables (or nullary predicate symbols) P, Q, R, S. Let Inf be the set of inferences of the ordered resolution calculus with selection over clauses over the signature. Define $Red_F$ such that a clause $C$ is contained in $Red_F(N)$ if it is entailed by clauses in $N$ that are smaller than $C$. Define $Red_I$ such that an inference is contained in $Red_I(N)$ if its conclusion is entailed by clauses in $N$ that are smaller than its largest premise. Then $Red := (Red_1, Red_F)$ is a redundancy criterion.

Let $N$ be the set of clauses (1) $\neg Q \lor P$, (2) $\neg S \lor R \lor Q$, (3) $\neg S \lor Q$, where the atom ordering is $P > Q > R > S$ and the first literals of (1) and (3) are selected. Due to the selection, $Inf(N)$ contains only a single inference, namely the ordered resolution inference $\iota$ between (2) and (1). The largest premise of $\iota$ is (1). The premise (2) is entailed by the smaller clause (3) and therefore contained in $Red_F(N)$. Consequently, $\iota \in Red'_I(N)$, which means that $N$ is saturated w.r.t. $Red'$. On the other hand, the conclusion $\neg S \lor R \lor P$ is not entailed by the clauses in $N$ that are smaller than (1)—i.e., (2) and (3)—so $\iota \notin Red_I(N)$. Therefore, $N$ is not saturated w.r.t. $Red$.

**Lemma 18** The following properties are equivalent for every $N \subseteq F$:

(i) $N$ is reducedly saturated w.r.t. Inf and Red;

(ii) $N$ is saturated w.r.t. Inf and $Red'$;

(iii) $N \setminus Red_F(N)$ is saturated w.r.t. Inf and Red.
**Proof** To show that (i) implies (ii), assume that $N$ is reducedly saturated w.r.t. Inf and Red— i.e., $Inf(N \ Red_F(N)) \subseteq Red_I(N)$. We must show that $Inf(N) \subseteq Red_I'(N)$. Let $\iota \in Inf(N)$. If no premise of $\iota$ is contained in $Red_F(N)$, then $\iota \in Inf(N \ Red_F(N)) \subseteq Red_I(N)$. Otherwise, $\iota \in Inf(F, Red_F(N))$. In both cases, we conclude $\iota \in Red_I'(N)$.

To show that (ii) implies (i), assume that $N$ is saturated w.r.t. Inf and Red'—i.e., $Inf(N) \subseteq Red_I'(N)$. We must show that $Inf(N \ Red_F(N)) \subseteq Red_I(N)$. Let $\iota \in Inf(N \ Red_F(N))$. Observe first that $\iota \in Inf(N \ Red_F(N)) \subseteq Inf(N) \subseteq Red_I'(N) = Red_I(N) \cup Inf(F, Red_F(N))$. Moreover, $\iota \in Inf(N \ Red_F(N))$ implies $\iota \notin Inf(F, Red_F(N))$. Combining both, we get $\iota \in Red_I(N)$.

The equivalence of (i)—i.e., $Inf(N \ Red_F(N)) \subseteq Red_I(N)$—and (iii)—i.e., $Inf(N \ Red_F(N)) \subseteq Red_I(N \ Red_F(N))$—follows from the fact that $Red_I(N) \subseteq Red_I(N \ Red_F(N))$ by (R3) and $Red_I(N \ Red_F(N)) \subseteq Red_I(N)$ by (R2). $\square$

Even though Red and Red' are not equivalent as far as saturation is concerned, they are equivalent w.r.t. refutational completeness:

**Theorem 19** The following properties are equivalent:

(i) $(Inf, Red)$ is statically refutationally complete w.r.t. $\models$;

(ii) $(Inf, Red)$ is reducedly statically refutationally complete w.r.t. $\models$;

(iii) $(Inf, Red')$ is statically refutationally complete w.r.t. $\models$;

(iv) $(Inf, Red')$ is reducedly statically refutationally complete w.r.t. $\models$.

**Proof** To show that (iii) implies (i), assume that $(Inf, Red')$ is statically refutationally complete. That is, the property

$$N \models \{\perp\} \text{ for some } \perp \in F_{\perp} \text{ implies } \perp' \in N \text{ for some } \perp' \in F_{\perp} \quad (*)$$

holds for every set $N \subseteq F$ that is saturated w.r.t. Inf and Red'. By Lemma 16, every set $N \subseteq F$ that is saturated w.r.t. Inf and Red is also saturated w.r.t. Inf and Red', so property (*) holds in particular for every set $N \subseteq F$ that is saturated w.r.t. Inf and Red.

To show that (i) implies (iii), assume that $(Inf, Red)$ is statically refutationally complete. Assume $N$ is saturated w.r.t. Inf and Red' and suppose that $N \models \{\perp\}$ for some $\perp \in F_{\perp}$. By Lemma 18, $N \ Red_F(N)$ is saturated w.r.t. Inf and Red. Furthermore, by (R1), $N \ Red_F(N) \models \{\perp\}$. So the static refutational completeness of $(Inf, Red)$ implies that $\perp' \in N \ Red_F(N)$ for some $\perp' \in F_{\perp}$; hence $\perp' \in N$. Thus, $(Inf, Red')$ is statically refutationally complete.

The equivalence of (iii) and (iv) follows from Lemma 15 and Corollary 14.

It remains to show the equivalence of (ii) and (iii). Observe that (ii) means that (*) holds for every set $N \subseteq F$ that is reducedly saturated w.r.t. Inf and Red, and that (iii) means that (*) holds for every set $N \subseteq F$ that is saturated w.r.t. Inf and Red'. By Lemma 18, these two properties are equivalent. $\square$

The limit of a reducedly fair $\triangleright_{Red}$-derivation is a reducedly saturated set.<fnref n="2" /> This is proved analogously to Lemma 9:

**Lemma 20** If $(N_i)_i$ is a reducedly fair $\triangleright_{Red}$-derivation, then the limit $N_{\infty}$ is reducedly saturated w.r.t. Inf and Red.

<footnote n="2">² The limit need not be saturated, though. In Example 17, the one-element sequence $(N_i)_{i=0}^0$ with $N_0 = N$ is reducedly fair w.r.t. Red, and its limit $N_{\infty} = N$ is reducedly saturated w.r.t. Red, but not saturated w.r.t. Red.</footnote>
*Proof* Since $\text{Red}_F(N_i) \subseteq \text{Red}_F(N_\infty)$ for every $i$, we have $\text{Inf}(N_\infty \setminus \text{Red}_F(N_\infty)) \subseteq \text{Inf}(N_\infty \cup \text{Red}_F(N_i))$. By reduced fairness, every inference $\iota \in \text{Inf}(N_\infty \setminus \text{Red}_F(N_\infty))$ is contained in $\cup_i \text{Red}_I(N_i)$. Therefore there exists some $i$ with $\iota \in \text{Red}_I(N_i)$, implying $\iota \in \text{Red}_I(N_\infty)$. $\square$

Lemmas 10 and 11 can then be reproved for reduced static and reduced dynamic refutational completeness. Together with Theorem 19, we obtain this result:

**Theorem 21** *The properties (i)–(iv) of Theorem 19 and the following four properties are equivalent:*

(v) $(\text{Inf}, \text{Red})$ is dynamically refutationally complete w.r.t. $\models$;

(vi) $(\text{Inf}, \text{Red})$ is reducedly dynamically refutationally complete w.r.t. $\models$;

(vii) $(\text{Inf}, \text{Red}')$ is dynamically refutationally complete w.r.t. $\models$;

(viii) $(\text{Inf}, \text{Red}')$ is reducedly dynamically refutationally complete w.r.t. $\models$.

Summarizing, we see that there are some differences between the “reduced” and the “nonreduced” approach, but that these differences are restricted to the intermediate notions, notably saturation. As far as (static or dynamic) refutational completeness is concerned, both approaches agree. Furthermore, Theorem 21 demonstrates that we can mix and match definitions from both worlds. Consequently, when we want to build on an existing refutational completeness proof for some saturation calculus, it does not matter which approach has been used there.

Given that the “nonreduced” definitions in Sections 2.1 and 2.2 are simpler than the “reduced” ones in the current section, there is usually little reason to prefer the “reduced” ones. For our purposes, a major advantage of the “nonreduced” definitions is that $\text{Red}_F$ and $\text{Red}_I$ are separated as much as possible. In particular, our definitions of saturation and static refutational completeness do not depend on redundant formulas, but only on redundant inferences. This property will be crucial for the proof of Theorem 45 in Section 3.

**Fairness in the Limit** Bachmair and Ganzinger consider a sequence $(N_i)_i$ fair if $\text{concl}(\text{Inf}(N') \setminus \text{Red}_I(N')) \subseteq (\cup_i N_i) \cup \text{Red}_F(\cup_i N_i)$, where $N' = N_\infty \setminus \text{Red}_F(N_\infty)$ [6, Section 4.1]. This is a quite peculiar property. First of all, it is overly complicated: If the conclusion of an inference $\iota \in \text{Inf}(N') \setminus \text{Red}_I(N')$ is contained in $(\cup_i N_i) \cup \text{Red}_F(\cup_i N_i)$, then $\iota \in \text{Red}_I(\cup_i N_i)$ by Lemma 1 and (R4), and by Lemma 6 and (R3) we have $\iota \in \text{Red}_I(\cup_i N_i) \subseteq \text{Red}_I((\cup_i N_i) \setminus ((\cup_i N_i) \setminus N_\infty)) = \text{Red}_I(N_\infty) \subseteq \text{Red}_I(N_\infty \setminus \text{Red}_F(N_\infty)) = \text{Red}_I(N')$. But this contradicts the assumption that $\iota \in \text{Inf}(N') \setminus \text{Red}_I(N')$. So the condition can be simplified to $\text{Inf}(N') \subseteq \text{Red}_I(N')$, and since $\text{Red}_I(N') = \text{Red}_I(N_\infty \setminus \text{Red}_F(N_\infty)) = \text{Red}_I(N_\infty)$, this is equivalent to $\text{Inf}(N_\infty \setminus \text{Red}_F(N_\infty)) \subseteq \text{Red}_I(N_\infty)$.

Since $\text{Inf}(N_\infty \setminus \text{Red}_F(N_\infty)) \subseteq \text{Inf}(N_\infty \cup \text{Red}_F(N_i))$ and $\cup_i \text{Red}_I(N_i) \subseteq \text{Red}_I(N_\infty)$, the (simplified) condition is entailed by reduced fairness. There is a crucial difference, though: While reduced fairness requires that every inference from $N_\infty$ is redundant or has a redundant premise at some finite step of the derivation, the Bachmair–Ganzinger definition also admits derivations where redundancy is achieved only in the limit.

**Example 22** Consider a signature consisting of two unary predicate symbols P, Q, a unary function symbol f, and a constant b. Let $\text{Inf}$ be the set of inferences of the ordered resolution calculus with selection over clauses over the signature.

Let $N$ be the set of clauses (1) $P(b)$, (2) $\neg P(x) \lor P(f(x))$, (3) $Q(b)$, (4) $\neg Q(b) \lor P(f(x))$, where the atom ordering is a lexicographic path ordering with precedence $P > Q > f > b$ and the first literals of (2) and (4) are selected. From (1) and (2), we obtain in the first derivation
step P(f(b)), in the second step P(f(f(b))), and so on. The limit $N_\infty$ consists of the four initial clauses (1)–(4) and all clauses of the form P(f^i(b)) with $i \ge 1$. The resolution inference between (3) and (4), yielding P(f(x)), is therefore redundant w.r.t. $N_\infty$, since for each of its ground instances the conclusion P(f^i(b)) is contained in $N_\infty$. However, it is not redundant w.r.t. any set $N_j$. Similarly, the premise (4) is redundant w.r.t. $N_\infty$ but not w.r.t. any set $N_j$. Therefore, the sequence of clause sets is fair according to the definition in Bachmair and Ganzinger [6, Section 4.1], but neither fair nor reducedly fair according to our definitions.

Of course, a redundancy property that holds only for the limit of an infinite sequence generally cannot be checked effectively. In other words, Bachmair and Ganzinger's definition is more permissive than our alternative definition, but the additional degree of freedom can hardly be exploited in a theorem prover.

**Semi-redundancy** Bachmair, Ganzinger, and Waldmann [8] use a definition of redundancy criteria that requires (R2) only for formulas and (R3) only for inferences. With their definition of fairness, this is sufficient to show that the limit of a fair $▷_{Red}$-derivation is saturated, and thus, to show that static refutational completeness implies dynamic refutational completeness. Their definition of fairness, however, requires essentially that inferences from formulas in the limit $N_\infty$ are redundant w.r.t. the limit, and since they do not enforce that an inference that is redundant at some step of the derivation is redundant w.r.t. the limit, this cannot be checked effectively in a theorem prover.

**Nonstrict Redundancy** Nieuwenhuis and Rubio [29, 30] and Peltier [34] define a ground clause C to be nonstrictly redundant w.r.t. a set N of ground clauses if C is entailed by smaller or equal clauses in N. This definition does not satisfy our condition (R3). Consequently, it can be used for proving the static completeness of a calculus, but it is insufficient to establish the connection between static and dynamic completeness (unless the notion of fairness is strengthened).

## 2.4 Intersections of Redundancy Criteria

In descriptions of concrete saturation calculi, we frequently encounter the situation that the calculus is parameterized in some way and that exactly one value of the parameter is used to show that every saturated $N \subseteq \mathbf{F}$ with $N \models \{\perp\}$ contains $\perp$, but that this value is still unknown during the actual saturation process. Consequently, inferences and formulas may be considered as redundant during the saturation only if they are redundant for every possible value of the parameter. To model this situation in our framework, it is useful to define consequence relations and redundancy criteria as intersections of previously defined consequence relations or redundancy criteria.

Let $\mathcal{Q}$ be an arbitrary nonempty set, and let $(\models^q)_{q \in \mathcal{Q}}$ be a $\mathcal{Q}$-indexed family of consequence relations over $\mathbf{F}$. Define $\models^\perp := \bigcap_{q \in \mathcal{Q}} \models^q$.

**Lemma 23** $\models^\perp$ is a consequence relation.

*Proof* Obvious. □

Let $\mathbf{Inf}$ be an inference system, and let $(Red^q)_{q \in \mathcal{Q}}$ be a $\mathcal{Q}$-indexed family of redundancy criteria, where each $Red^q = (Red_1^q, Red_\mathbf{F}^q)$ is a redundancy criterion for $\mathbf{Inf}$ and $\models^q$. Let $Red_1^\perp(N) := \bigcap_{q \in \mathcal{Q}} Red_1^q(N)$ and $Red_\mathbf{F}^\perp(N) := \bigcap_{q \in \mathcal{Q}} Red_\mathbf{F}^q(N)$ for all $N$. Define $Red^\perp := (Red_1^\perp, Red_\mathbf{F}^\perp)$.
**Lemma 24** *Red*<sub>I</sub> is a redundancy criterion for $|\models|$ and Inf.

*Proof* (R1) Assume that $N \models_G^{\emptyset} \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$—i.e., $N \models^q \{\perp\}$ for every $q \in Q$. As $\mathrm{Red}_{\mathbf{F}}^I(N) \subseteq \mathrm{Red}_{\mathbf{F}}^q(N)$, we have $N \setminus \mathrm{Red}_{\mathbf{F}}^I(N) \supseteq N \setminus \mathrm{Red}_{\mathbf{F}}^q(N)$, and by (C2) $N \setminus \mathrm{Red}_{\mathbf{F}}^I(N) \models^q N \setminus \mathrm{Red}_{\mathbf{F}}^q(N)$. Furthermore, $N \setminus \mathrm{Red}_{\mathbf{F}}^q(N) \models^q \{\perp\}$ by (R1) for $\mathrm{Red}^q$. So $N \setminus \mathrm{Red}_{\mathbf{F}}^I(N) \models^q \{\perp\}$ by (C4) for every $q \in Q$ and therefore $N \setminus \mathrm{Red}_{\mathbf{F}}(N) \models_G^{\emptyset} \{\perp\}$.

(R2) Let $N \subseteq N'$. Since $\mathrm{Red}_{\mathbf{F}}^q(N) \subseteq \mathrm{Red}_{\mathbf{F}}^q(N')$ for every $q$, we have $\mathrm{Red}_{\mathbf{F}}^I(N) = \bigcap_{q \in Q} \mathrm{Red}_{\mathbf{F}}^q(N) \subseteq \bigcap_{q \in Q} \mathrm{Red}_{\mathbf{F}}^q(N') = \mathrm{Red}_{\mathbf{F}}^I(N')$ and analogously for $\mathrm{Red}_{\mathbf{F}}^I$.

(R3) Let $N' \subseteq \mathrm{Red}_{\mathbf{F}}(N)$. Since $\mathrm{Red}_{\mathbf{F}}^q(N) \subseteq \mathrm{Red}_{\mathbf{F}}^q(N \setminus N')$ for every $q$, we have $\mathrm{Red}_{\mathbf{F}}^I(N) = \bigcap_{q \in Q} \mathrm{Red}_{\mathbf{F}}^q(N) \subseteq \bigcap_{q \in Q} \mathrm{Red}_{\mathbf{F}}^q(N \setminus N') = \mathrm{Red}_{\mathbf{F}}^I(N \setminus N')$ and analogously for $\mathrm{Red}_{\mathbf{F}}^I$.

(R4) If $\iota \in \mathrm{Inf}$ and $\mathrm{concl}(\iota) \in N$, then $\iota \in \mathrm{Red}_1^q(N)$ for every $q \in Q$; hence $\iota \in \bigcap_{q \in Q} \mathrm{Red}_1^q(N) = \mathrm{Red}_1^I(N)$. $\square$

**Lemma 25** A set $N \subseteq \mathbf{F}$ is saturated w.r.t. Inf and $\mathrm{Red}^I$ if and only if it is saturated w.r.t. Inf and $\mathrm{Red}^q$ for every $q \in Q$.

*Proof* If $N$ is saturated w.r.t. Inf and $\mathrm{Red}^I$, then $\mathrm{Inf}(N) \subseteq \mathrm{Red}_1^I(N) = \bigcap_{q \in Q} \mathrm{Red}_1^q(N)$; hence $\mathrm{Inf}(N) \subseteq \mathrm{Red}_1^q(N)$ for every $q \in Q$, implying that $N$ is saturated w.r.t. Inf and $\mathrm{Red}^q$.

Conversely, if $N$ is saturated w.r.t. Inf and $\mathrm{Red}^q$ for every $q \in Q$, then $\mathrm{Inf}(N) \subseteq \mathrm{Red}_1^q(N)$ for every $q \in Q$; hence $\mathrm{Inf}(N) \subseteq \mathrm{Red}_1^I(N) = \bigcap_{q \in Q} \mathrm{Red}_1^q(N)$, which implies that $N$ is saturated w.r.t. Inf and $\mathrm{Red}^I$.

In many cases where a redundancy criterion $\mathrm{Red}^I$ is defined as the intersection of other criteria, the consequence relations $\models^q$ agree for all $q \in Q$. There are some exceptions, though, for example constraint superposition [29], where the parameter $q$ is a convergent rewrite system $R$ and $\models^q$ is entailment modulo $R$. For such calculi, one can typically demonstrate the static refutational completeness of $(\mathrm{Inf}, \mathrm{Red}^I)$ in the following form:

**Lemma 26** If for every set $N \subseteq \mathbf{F}$ that is saturated w.r.t. Inf and $\mathrm{Red}^I$ and does not contain any $\perp' \in \mathbf{F}_{\perp}$ there exists some $q \in Q$ such that $N \not\models^q \{\perp'\}$ for some $\perp \in \mathbf{F}_{\perp}$, then $(\mathrm{Inf}, \mathrm{Red}^I)$ is statically refutationally complete w.r.t. $\models^I$.

*Proof* Suppose that $N \subseteq \mathbf{F}$ is saturated w.r.t. Inf and $\mathrm{Red}^I$ and $N \models^{\emptyset} \{\perp'\}$ for some $\perp' \in \mathbf{F}_{\perp}$. Consequently, $N \models^q \{\perp'\}$ for every $q \in Q$. By (C1), $N \models^q \{\perp'\} \models^q \{\perp\}$ for every $\perp \in \mathbf{F}_{\perp}$. If the condition of the lemma holds, then $N$ must contain some $\perp'' \in \mathbf{F}_{\perp}$. Therefore, $(\mathrm{Inf}, \mathrm{Red}^I)$ is statically refutationally complete w.r.t. $\models^I$. $\square$

### 3 Lifting

A standard approach for establishing the refutational completeness of a calculus is to first concentrate on the ground case and then lift the results to the nonground case. In this section, we show how to perform this lifting abstractly, given a suitable grounding function $G$. The function maps every formula $C \in \mathbf{F}$ to a set $G(C)$ of formulas from a set of formulas $G$. Depending on the logic and the calculus, $G(C)$ may be, for example, the set of all ground instances of $C$, a subset of the set of ground instances of $C$, or even a set of formulas from another logic. Similarly, $\mathrm{Finf}$-inferences are mapped to sets of $\mathrm{GInf}$-inferences, and saturation w.r.t. $\mathrm{Finf}$-inferences is related to saturation w.r.t. $\mathrm{GInf}$-inferences.

There are calculi where some $\mathrm{Finf}$-inferences $\iota$ do not have a counterpart in $\mathrm{GInf}$, such as the POSEXT inferences of $\lambda$-free superposition [14]. In these cases, we set $G(\iota) = \mathrm{undef}$.
## 3.1 Standard Lifting

Given two sets of formulas **F** and **G**, an **F**-inference system *Finf*, a **G**-inference system *Ginf*, and a redundancy criterion *Red* for *Ginf*, let *G* be a function that maps every formula in **F** to a subset of **G** and every **F**-inference in *Finf* to *undef* or to a subset of *Ginf*. The function *G* is called a *grounding function* if

(G1) for every $\perp \in \mathbf{F}_{\perp}$, $\emptyset \neq \mathcal{G}(\perp) \subseteq \mathbf{G}_{\perp}$;

(G2) for every $C \in \mathbf{F}$, if $\perp \in \mathcal{G}(C)$ and $\perp \in \mathbf{G}_{\perp}$ then $C \in \mathbf{F}_{\perp}$;

(G3) for every $\iota \in Finf$, if $\mathcal{G}(\iota) \neq undef$, then $\mathcal{G}(\iota) \subseteq Red_1(\mathcal{G}(concl(\iota)))$.

The function $\mathcal{G}$ is extended to sets $N \subseteq \mathbf{F}$ by defining $\mathcal{G}(N) := \bigcup_{C \in N} \mathcal{G}(C)$ for all $N$. Analogously, for a set $I \subseteq Finf$, $\mathcal{G}(I) := \bigcup_{\iota \in I, \mathcal{G}(\iota) \neq undef} \mathcal{G}(\iota)$.

**Remark 27** Conditions (G1) and (G2) express that *false* formulas may only be mapped to sets of *false* formulas, and that only *false* formulas may be mapped to sets of *false* formulas. For most applications, it would be possible to replace condition (G3) by

(G3') for every $\iota \in Finf$, if $\mathcal{G}(\iota) \neq undef$, then $concl(\mathcal{G}(\iota)) \subseteq \mathcal{G}(concl(\iota))$,

which implies (G3) by property (R4). There are some calculi, however, for which (G3') is too strong. Typical examples are calculi where the **F**-inferences include some normalization or abstraction step that does not have a counterpart in the **G**-inferences. So an **F**-inference $\iota$ may have a conclusion $C \lor t \approx t'$, where the literal $t \approx t'$ results from the normalization step, but the conclusions of the instances of $\iota$ have the form $C\theta$ for a substitution $\theta$ that unifies $t$ and $t'$. In this case, (G3) is still satisfied, but (G3') is not.

**Example 28** In standard superposition, **F** is the set of all universally quantified first-order clauses over some signature $\Sigma$, **G** is the set of all ground first-order clauses over $\Sigma$, and $\mathcal{G}$ maps every clause **C** to the set of its ground instances $C\theta$ and every superposition inference $\iota$ to the set of its ground instances $\iota\theta$.

Let $\mathcal{G}$ be a grounding function from **F** and *Finf* to **G** and *Ginf*, and let $\models = \mathcal{G}(\mathbf{G}) \times \mathcal{P}(\mathbf{G})$ be a consequence relation over **G**. We define the relation $\models_G = \mathcal{G}(\mathbf{F}) \times \mathcal{P}(\mathbf{F})$ such that $N_1 \models_G N_2$ if and only if $\mathcal{G}(N_1) \models_G \mathcal{G}(N_2)$. We call $\models_G$ the *G-lifting* of $\models$. It corresponds to Herbrand entailment. If Tarski entailment (i.e., $N_1 \models_T N_2$ if and only if any model of $N_1$ is also a model of $N_2$) is desired, the mismatch can be repaired by showing that the two notions of entailment are equivalent as far as refutations are concerned.

**Lemma 29** $\models_G$ is a consequence relation over **F**.

*Proof* (C1) Let $\perp \in \mathbf{F}_{\perp}$. Then by property (G1) of grounding functions, $\mathcal{G}(\{\perp\})$ contains some $\perp' \in \mathbf{G}_{\perp}$. So $\mathcal{G}(\{\perp\}) \models_G \{\perp'\} \models_G \mathcal{G}(N_1)$ for every $N_1$, and hence $\{\perp\} \models_G N_1$ as required.

(C2) Let $N_2 \subseteq N_1$. Then $\mathcal{G}(N_2) \subseteq \mathcal{G}(N_1)$, so $\mathcal{G}(N_1) \models_G \mathcal{G}(N_2)$, and thus $N_1 \models_G N_2$.

(C3) Suppose that $N_1 \models_G \{C\}$ for every $C \in N_2$. Then $\mathcal{G}(N_1) \models_G \mathcal{G}(\{C\})$ for every $C \in N_2$ and therefore $\mathcal{G}(N_1) = \bigcup_{C \in N_2} \mathcal{G}(\{C\}) = \mathcal{G}(N_2)$; hence $N_1 \models_G N_2$.

(C4) Suppose that $N_1 \models_G N_2$ and $N_2 \models_G N_3$. Then $\mathcal{G}(N_1) \models_G \mathcal{G}(N_2)$ and $\mathcal{G}(N_2) \models_G \mathcal{G}(N_3)$; therefore $\mathcal{G}(N_1) \models_G \mathcal{G}(N_3)$, and therefore $N_1 \models_G N_3$. $\square$
Let Red = (Red<sub>I</sub>, Red<sub>F</sub>) be a redundancy criterion for $|=$ and GInf. We define functions Red<sub>I</sub><sup>G</sup> : P(F) → P(FInf) and Red<sub>F</sub><sup>G</sup> : P(F) → P(F) by

$$
\begin{align*}
\iota \in \mathrm{Red}_I^G(N) \text{ if and only if} \\
\begin{aligned}[t]
  \mathcal{G}(\iota) &\neq \mathrm{undef} \text{ and } \mathcal{G}(\iota) \subseteq \mathrm{Red}_I(\mathcal{G}(N)) \\
  \mathcal{G}(\iota) &= \mathrm{undef} \text{ and } \mathcal{G}(\mathrm{concl}(\iota)) \subseteq \mathcal{G}(N) \cup \mathrm{Red}_F(\mathcal{G}(N));
\end{aligned}
\end{align*}
\[
C \in \mathrm{Red}_F^G(N) \text{ if and only if}
\]
\[
\mathcal{G}(C) \subseteq \mathrm{Red}_F(\mathcal{G}(N)).
\]
$$

We call Red<sup>G</sup> := (Red<sub>I</sub><sup>G</sup>, Red<sub>F</sub><sup>G</sup>) the G-lifting of Red.

**Theorem 30** Red<sup>G</sup> is a redundancy criterion for $|\models_G$ and FInf.

We omit the proof at this point since we will prove a more general result (Theorem 42)
in Section 3.2.

The following folklore lemma connects a nonground calculus with a ground calculus it
overapproximates.

**Lemma 31** If $N \subseteq \mathbf{F}$ is saturated w.r.t. FInf and $Red^G$ and GInf($\mathcal{G}(N)$) $\subseteq \mathcal{G}$(FInf$(N)) \cup Red_1(\mathcal{G}(N))$, then $\mathcal{G}(N)$ is saturated w.r.t. GInf and Red.

*Proof* Suppose that *N* is saturated w.r.t. *FInf* and *Red*^*G*—i.e., *FInf*(*N*) ⊆ *Red*^*G*<sub>1</sub>(*N*). We must show that *G*(*N*) is saturated w.r.t. *GINf* and *Red*—i.e., *GINf*(*G*(*N*)) ⊆ *Red*<sub>1</sub>(*G*(*N*)).

Let $\iota' \in GInf(\mathcal{G}(N))$. By assumption, $\iota'$ is contained in $\mathcal{G}(FInf(N))$ or $\mathrm{Red}_1(\mathcal{G}(N))$. In the second case, we are done immediately. In the first case, $\iota' \in \mathcal{G}(\iota)$ for some $\iota \in FInf(N) \subseteq \mathrm{Red}_1^G(N)$ with $\mathcal{G}(\iota) \neq \mathrm{undef}$, so by definition of $\mathrm{Red}_1^G$ we have again $\iota' \in \mathrm{Red}_1(\mathcal{G}(N))$. $\square$

An inference in GInf(G(N)) is called *liftable* if it is contained in G(FInf(N)). Using this terminology, we can rephrase the lemma as follows: If *N* is saturated and every unliftable inference from *G*(*N*) is redundant w.r.t. *G*(*N*), then *G*(*N*) is saturated.

**Theorem 32** If (GINf,Red) is statically refutationally complete w.r.t. $|=$, and if we have GInf(G(N)) ⊆ G(FInf(N)) ∪ Red₁(G(N)) for every N ⊆ F that is saturated w.r.t. FInf and Red<sup>G</sup>, then (FInf,Red<sup>G</sup>) is statically refutationally complete w.r.t. $|\models_G$.

*Proof* Assume (GINf,Red) is statically refutationally complete w.r.t. $|=$. Assume $N \subseteq \mathbf{F}$ is saturated w.r.t. FInf and Red<sup>G</sup> and assume that $N \models_G \perp$ for some $\perp \in \mathbf{F}_\perp$. We must show that $\perp' \in N$ for some $\perp' \in \mathbf{F}_\perp$.

By definition of $|\models_G$, we know that $\mathcal{G}(N) \models_G \mathcal{G}(\perp)$. By property (G1) of grounding functions, $\mathcal{G}(\perp)$ is a nonempty subset of $\mathbf{G}_\perp$. Let $\perp_G \in \mathcal{G}(\perp)$. Then $\mathcal{G}(N) \models_G \mathcal{G}(\perp) \models_G \{\perp_G\}$.

By the previous lemma, we know that $\mathcal{G}(N)$ is saturated w.r.t. GInf and Red, so there exists some $\perp'_G \in \mathbf{G}_\perp$ such that $\perp'_G \in \mathcal{G}(N)$. Hence $\perp'_G \in \mathcal{G}(C)$ for some $C \in N$, which implies $C \in \mathbf{F}_\perp$ by property (G2) of grounding functions. Now define $\perp' := C$. $\square$

**Example 33** In ordered binary resolution without selection [6, 35], all inferences are lift-
able, as demonstrated below. Let Σ be a first-order signature containing at least one constant,
let F be the set of all Σ-clauses without equality, and let G be the set of all ground Σ-clauses
without equality. Let FInf and GInf be the sets of all resolution or factoring inferences from
clauses in respectively F and G that satisfy the given ordering restrictions, and let G be
the function that maps every clause C ∈ F to the set of all its ground instances Cθ and that
maps every inference $(C_n, ..., C_0) \in Finf$ to the set of all $(C_n\theta, ..., C_0\theta) \in GInf$. Then every resolution inference in $GInf$ from ground instances of clauses in $N$ has the form

$$ \frac{D'\theta \lor B\theta \quad C'\theta \lor \neg A\theta}{D'\theta \lor C'\theta} $$

with $A\theta = B\theta$ and is contained in $G(\iota)$ for some inference $\iota \in Finf(N)$ of the form

$$ \frac{D' \lor B \quad C' \lor \neg A}{(D' \lor C')\sigma} $$

with $\sigma = \text{mgu}(A, B)$, and analogously for factoring inferences.

Therefore, the static refutational completeness of $GInf$ implies the static refutational completeness of $Finf$.

The liftability result above holds also for ordered binary resolution with selection, provided that the selection function $fsel$ on $F$ and the selection function $gsel$ on $G$ are such that every clause $D \in G(N)$ inherits the selection of at least one clause $C \in N$ for which $D \in G(C)$. One can show that for every $N \subseteq G$ and $fsel$, such a $gsel$ exists. However, this $gsel$ depends on $N$, and therefore Theorem 32 is not applicable. We will discuss this issue further in Section 3.3.

**Example 34** In the superposition calculus without selection [5], all inferences are liftable, except superpositions at or below a variable position. Let $\Sigma$ be a first-order signature containing at least one constant and no predicate symbols except $\approx$, let $F$ be the set of all $\Sigma$-clauses with equality, and let $G$ be the set of all ground $\Sigma$-clauses with equality. Let $Finf$ and $GInf$ be the sets of all superposition, equality resolution, and equality factoring inferences from clauses in respectively $F$ and $G$ that satisfy the given ordering restrictions, and let $G$ be the function that maps every clause $C \in F$ to the set of all its ground instances $C\theta$ and that maps every inference $(C_n, ..., C_0) \in Finf$ to the set of all $(C_n\theta, ..., C_0\theta) \in GInf$. Then every equality resolution or equality factoring inference from ground instances of clauses in $N$ is contained in $G(\iota)$ for some inference $\iota \in Finf(N)$. The same applies to superposition inferences

$$ \frac{D'\theta \lor t\theta \approx t'\theta \quad C'\theta \lor [-]s\theta \approx s'\theta}{D'\theta \lor C'\theta \lor [-]s\theta[t'\theta]_p \approx s'\theta} $$

with $s\theta|_p = t\theta$, provided that $p$ is a position of $s$ and $s|_p$ is not a variable. Otherwise, $p = p_1p_2$ for some variable $x$ occurring in $s$ at the position $p_1$, so $x\theta|_{p_2} = t\theta$. In this case, define $\theta'$ such that $x\theta' = x\theta[t'\theta]_{p_2}$ and $y\theta' = y\theta$ for $y \neq x$. By congruence, the conclusion of the inference is entailed by the first premise (which is necessarily smaller than the second) and $C'\theta' \lor [-]s\theta' \approx s'\theta'$. The ordering restrictions of the calculus require that $t\theta \succ t'\theta$; hence the latter clause is also smaller than the second premise. By the usual redundancy criterion for superposition, this renders the inference redundant w.r.t. $N$.

Like for ordered resolution, the static refutational completeness of $GInf$ implies the static refutational completeness of $Finf$.

## 3.2 Adding Tiebreaker Orderings

We now strengthen the $G$-lifting of redundancy criteria introduced in the previous subsection to also support subsumption deletion. Let $\Box = (\Box_D)_{D \in G}$ be a $G$-indexed family of strict
partial orderings on $\mathbf{F}$ that are well founded (i.e., for every $D, \sqsupset_D$ there exists no infinite descending chain $C_0 \sqsupset_D C_1 \sqsupset_D \cdots$). We define $\mathrm{Red}_F^{G, \sqsupset} : \mathcal{P}(\mathbf{F}) \to \mathcal{P}(\mathbf{F})$ as follows:

$C \in \mathrm{Red}_F^{G, \sqsupset}(N)$ if and only if
for every $D \in \mathcal{G}(C)$,
$D \in \mathrm{Red}_F(\mathcal{G}(N))$ or there exists $C' \in N$ such that $C \sqsupset_D C'$ and $D \in \mathcal{G}(C')$.

Notice how $\sqsupset_D$ is used to break ties between $C$ and $C'$, possibly making $C$ redundant. We call $\mathrm{Red}^{G, \sqsupset} := (\mathrm{Red}_I^G, \mathrm{Red}_F^{G, \sqsupset})$ the $(\mathcal{G}, \sqsupset)$-lifting of $\mathrm{Red}$.

For nearly all applications (with a notable exception in Example 49 below), the orderings $\sqsupset_D$ agree for all $D \in \mathbf{G}$. In these cases, we may take $\sqsupset$ as a single well-founded strict partial ordering, rather than as a $\mathbf{G}$-indexed family of such orderings. We get the previously defined $\mathrm{Red}^G = (\mathrm{Red}_I^G, \mathrm{Red}_F^G)$ as a special case of $\mathrm{Red}^{G, \sqsupset} = (\mathrm{Red}_I^G, \mathrm{Red}_F^{G, \sqsupset})$ by setting $\sqsupset_D := \emptyset$— i.e., the empty strict partial ordering on $\mathbf{F}$—for every $D \in \mathbf{G}$.

As demonstrated by the following lemma, we may assume without loss of generality that the formula $C'$ in the definition of $\mathrm{Red}_F^{G, \sqsupset}$ is contained in $N \setminus \mathrm{Red}_F^{G, \sqsupset}(N)$:

**Lemma 35** $C \in \mathrm{Red}_F^{G, \sqsupset}(N)$ if and only if for every $D \in \mathcal{G}(C)$ we have $D \in \mathrm{Red}_F(\mathcal{G}(N))$ or there exists $C' \in N \setminus \mathrm{Red}_F^{G, \sqsupset}(N)$ such that $C \sqsupset_D C'$ and $D \in \mathcal{G}(C')$.

*Proof* The “if” direction is trivial. For the “only if” direction, assume that $C \in \mathrm{Red}_F^{G, \sqsupset}(N)$ and $D \in \mathcal{G}(C)$. By definition, $D \in \mathrm{Red}_F(\mathcal{G}(N))$ or there exists $C' \in N$ such that $C \sqsupset_D C'$ and $D \in \mathcal{G}(C')$. If $D \in \mathrm{Red}_F(\mathcal{G}(N))$, we are done. Let $D \notin \mathrm{Red}_F(\mathcal{G}(N))$. By well-foundedness of $\sqsupset_D$, there exists a minimal formula $C' \in N$ w.r.t. $\sqsupset_D$ such that $C \sqsupset_D C'$ and $D \in \mathcal{G}(C')$. Assume that $C'$ were contained in $\mathrm{Red}_F^{G, \sqsupset}(N)$. Since $D \notin \mathrm{Red}_F(\mathcal{G}(N))$, there exists $C'' \in N$ such that $C' \sqsupset_D C''$ and $D \in \mathcal{G}(C'')$. But then $C \sqsupset_D C''$, contradicting the minimality of $C'$. So $C' \in N \setminus \mathrm{Red}_F^{G, \sqsupset}(N)$. $\square$

Next, we show that $(\mathrm{Red}_I^G, \mathrm{Red}_F^{G, \sqsupset})$ is a redundancy criterion. We start with a technical lemma:

**Lemma 36** $\mathcal{G}(N) \setminus \mathrm{Red}_F(\mathcal{G}(N)) \subseteq \mathcal{G}(N \setminus \mathrm{Red}_F^{G, \sqsupset}(N))$.

*Proof* Let $D \in \mathcal{G}(N) \setminus \mathrm{Red}_F(\mathcal{G}(N))$. Since $D \in \mathcal{G}(N)$, there exists $C \in N$ with $D \in \mathcal{G}(C)$. Let $C$ be a minimal formula with this property w.r.t. $\sqsupset_D$.

Assume that $C \in \mathrm{Red}_F^{G, \sqsupset}(N)$. Then, by definition, $D \in \mathrm{Red}_F(\mathcal{G}(N))$ or there exists $C' \in N$ such that $C \sqsupset_D C'$ and $D \in \mathcal{G}(C')$. The first property contradicts our initial assumption, whereas the second property contradicts the minimality of $C$. So $C \notin \mathrm{Red}_F^{G, \sqsupset}(N)$ and thus $D \in \mathcal{G}(N \setminus \mathrm{Red}_F^{G, \sqsupset}(N))$. $\square$

We can now show that $(\mathrm{Red}_I^G, \mathrm{Red}_F^{G, \sqsupset})$ satisfies the properties (R1)–(R4) of redundancy criteria:

**Lemma 37** If $N \models_G \{\perp\}$ for some $\perp \in \mathbf{F}_\perp$, then $N \setminus \mathrm{Red}_F^{G, \sqsupset}(N) \models_G \{\perp\}$.

*Proof* Let $\perp \in \mathbf{F}_\perp$ and suppose that $N \models_G \{\perp\}$—i.e., $\mathcal{G}(N) \models_G \{\perp\}$. Since $\mathcal{G}(\{\perp\})$ contains some $\perp' \in \mathbf{G}_\perp$ by property (G1) of grounding functions, we have $\mathcal{G}(N) \models_G \{\perp\} \models \{\perp'\}$. By property (R1) of redundancy criteria, this implies $\mathcal{G}(N) \setminus \mathrm{Red}_F(\mathcal{G}(N)) \models \{\perp'\}$. Furthermore, by Lemma 36, $\mathcal{G}(N) \setminus \mathrm{Red}_F(\mathcal{G}(N)) \subseteq \mathcal{G}(N \setminus \mathrm{Red}_F^{G, \sqsupset}(N))$, and therefore
$G(N \setminus Red_F^{G, \sqsupset}(N)) \models G(N) \setminus Red_F(G(N))$. Combining the two relations, we obtain $G(N \setminus Red_F^{G, \sqsupset}(N)) \models \{\perp'\} \models G(\{\perp\})$. By definition of $\models_G$ and property (G1) of grounding functions, this means $N \setminus Red_F^{G, \sqsupset}(N) \models_G \{\perp\}$, as required. $\square$

**Lemma 38** If $N \subseteq N'$, then $Red_F^{G, \sqsupset}(N) \subseteq Red_F^{G, \sqsupset}(N')$ and $Red_I^G(N) \subseteq Red_I^G(N')$.

*Proof* Obvious. $\square$

**Lemma 39** If $N' \subseteq Red_F^{G, \sqsupset}(N)$, then $Red_F^{G, \sqsupset}(N) \subseteq Red_F^{G, \sqsupset}(N \setminus N')$.

*Proof* Let $N' \subseteq Red_F^{G, \sqsupset}(N)$, let $C \in Red_F^{G, \sqsupset}(N)$. Then, by Lemma 35, for every $D \in G(C)$ we have $D \in Red_F(G(N))$ or there exists $C' \in N \setminus Red_F^{G, \sqsupset}(N)$ such that $C \sqsupset D$, $C'$ and $D \in G(C')$.

**CASE 1:** $D \in Red_F(G(N))$. By property (R3), $D \in Red_F(G(N) \setminus Red_F(G(N)))$. Since $G(N) \setminus Red_F(G(N)) \subseteq G(N \setminus Red_F^{G, \sqsupset}(N)) \subseteq G(N \setminus N')$, this implies $D \in Red_F(G(N \setminus N'))$.

**CASE 2:** $D \notin Red_F(G(N))$ and there exists $C' \in N \setminus Red_F^{G, \sqsupset}(N)$ such that $C \sqsupset D$, $C'$ and $D \in G(C')$. Since $N \setminus Red_F^{G, \sqsupset}(N) \subseteq N \setminus N'$, we get $C' \in N \setminus N'$.

Since every $D \in G(C)$ is either contained in $Red_F(G(N \setminus N'))$ or in $G(C')$ for some $C' \in N \setminus N'$ with $C \sqsupset D$, we conclude that $C \in Red_F^{G, \sqsupset}(N \setminus N')$. $\square$

**Lemma 40** If $N' \subseteq Red_F^{G, \sqsupset}(N)$, then $Red_I^G(N) \subseteq Red_I^G(N \setminus N')$.

*Proof* Let $N' \subseteq Red_F^{G, \sqsupset}(N)$, let $\iota \in Red_I^G(N)$.

If $G(\iota) \neq \text{undef}$, then every $\iota' \in G(\iota)$ is contained in $Red_I(G(N))$, and by property (R3) also in $Red_I(G(N) \setminus Red_F(G(N)))$. Furthermore, since $G(N) \setminus Red_F(G(N)) \subseteq G(N \setminus Red_F^{G, \sqsupset}(N)) \subseteq G(N \setminus N')$ by Lemma 36, this implies $\iota' \in Red_I(G(N \setminus N'))$ by (R2). Since every $\iota' \in G(\iota)$ is contained in $Red_I(G(N \setminus N'))$, we conclude that $\iota \in Red_I^G(N \setminus N')$.

Otherwise $G(\iota) = \text{undef}$. Then $G(concl(\iota)) \subseteq G(N) \cup Red_F(G(N)) = (G(N) \setminus Red_F(G(N))) \cup Red_F(G(N))$. Let $D \in G(concl(\iota))$. We consider two cases: If $D \in G(N) \setminus Red_F(G(N))$, then by Lemma 36, $D \in G(N \setminus Red_F^{G, \sqsupset}(N)) \subseteq G(N \setminus N')$. Otherwise $D \in Red_F(G(N))$, then by (R3) $D \in Red_F(G(N) \setminus Red_F(G(N)))$. Since $G(N) \setminus Red_F(G(N)) \subseteq G(N \setminus Red_F^{G, \sqsupset}(N)) \subseteq G(N \setminus N')$, this implies $D \in Red_F(G(N \setminus N'))$. Combining both cases, we obtain $G(concl(\iota)) \in G(N \setminus N') \cup Red_F(G(N \setminus N'))$, hence $\iota \in Red_I^G(N \setminus N')$. $\square$

**Lemma 41** If $\iota \in FInf$ and $concl(\iota) \in N$, then $\iota \in Red_I^G(N)$.

*Proof* Let $\iota \in FInf$ such that $concl(\iota) \in N$. If $G(\iota) \neq \text{undef}$, then by property (G3) of grounding functions, $G(\iota)$ is a subset of $Red_I(G(concl(\iota)))$, which in turn is a subset of $Red_I(G(N))$. So $\iota \in Red_I^G(N)$.

Otherwise, $G(\iota) = \text{undef}$. Then $concl(\iota) \in N$ implies $G(concl(\iota)) \subseteq G(N)$, so again $\iota \in Red_I^G(N)$. $\square$

By combining Lemmas 37–41, we obtain our first main result, generalizing Theorem 30:

**Theorem 42** Let Red be a redundancy criterion for $\models$ and $GInf$, let $G$ be a grounding function from $F$ and $FInf$ to $G$ and $GInf$, and let $\sqsupset = (\sqsupset_D)_{D \in G}$ be a $G$-indexed family of well-founded strict partial orderings on $F$. Then the $(G, \sqsupset)$-lifting $Red^{G, \sqsupset}$ of Red is a redundancy criterion for $\models_G$ and $FInf$.
Observe that $\Box$ appears only in the second component of $Red^{G,\Box} = (Red_I^G, Red_F^{G,\Box})$ and that the definitions of a saturated set and of static refutational completeness do not depend on the second component of a redundancy criterion. The following lemmas are immediate consequences of these observations:

**Lemma 43** A set $N \subseteq \mathbf{F}$ is saturated w.r.t. $\mathbf{Inf}$ and $Red^{G,\Box}$ if and only if it is saturated w.r.t. $\mathbf{Inf}$ and $Red^{G,\emptyset}$.

**Lemma 44** $(\mathbf{Inf}, Red^{G,\Box})$ is statically refutationally complete w.r.t. $\models_G$ if and only if $(\mathbf{Inf}, Red^{G,\emptyset})$ is statically refutationally complete w.r.t. $\models_G$.

Combining Lemmas 10 and 44, we obtain our second main result:

**Theorem 45** Let $Red$ be a redundancy criterion for $\models$ and $\mathbf{Inf}$, let $G$ be a grounding function from $\mathbf{F}$ and $\mathbf{Inf}$ to $G$ and $\mathbf{Inf}$, and let $\Box = (\Box_D)_{D \in G}$ be a $G$-indexed family of well-founded strict partial orderings on $\mathbf{F}$. If $(\mathbf{Inf}, Red^{G,\emptyset})$ is statically refutationally complete w.r.t. $\models_G$, then $(\mathbf{Inf}, Red^{G,\Box})$ is dynamically refutationally complete w.r.t. $\models_G$.

**Example 46** For resolution or superposition in standard first-order logic, we can define the instantiation quasi-ordering $\geq$ on clauses by $C \geq C'$ if and only if $C = C'\sigma$ for some substitution $\sigma$. In particular, if $C$ and $C'$ are $\alpha$-renamings of each other, then $C \geq C'$ and $C \leq C'$. The instantiation ordering $\succ := \geq \setminus \leq$ is well founded. By choosing $\Box := \succ$, we obtain a criterion $Red^{G,\Box}$ that includes standard redundancy (Example 3) and also supports subsumption deletion. (It is customary to define subsumption so that $C$ is subsumed by $C'$ if $C = C'\sigma \lor D$ for some substitution $\sigma$ and some possibly empty clause $D$, but since the case where $D$ is nonempty is already supported by the standard redundancy criterion, the instantiation ordering $\succ$ is sufficient.)

Similarly, for proof calculi modulo commutativity (C) or associativity and commutativity (AC), we can let $C \geq C'$ be true if there exists a substitution $\sigma$ such that $C$ equals $C'\sigma$ up to the equational theory (C or AC). The relation $\succ = \geq \setminus \leq$ is then again well founded.

**Example 47** For higher-order calculi such as higher-order resolution [25] and $\lambda$-superposition [13], the instantiation ordering is not well founded, as witnessed by the chain

$$ Pxx \succ P(xa)(xb_1) \succ P(xaa)(xb_1b_2) \succ \dots $$

**Example 48** In constraint superposition with ordering constraints [29], a ground instance of a constrained clause $C[[K]]$ is defined as a ground clause $C\theta$ for which the constraint $K\theta$ evaluates to true. One can then define the quasi-ordering $\geq$ by stating that $C[[K]] \geq C'[[K']]$ if and only if every ground instance of $C[[K]]$ is a ground instance of $C'[[K']]$. Again, the ordering $\succ := \geq \setminus \leq$ is not well founded, since

$$ P(x) [[x \prec b]] \succ P(x) [[x \prec f(b)]] \succ P(x) [[x \prec f(b))] \succ \dots $$

is an infinite chain if $\succ$ is a simplification ordering.

Even if the instantiation ordering for some logic is not well founded, as in the two examples above, we can always define $\Box$ as the intersection of the instantiation quasi-ordering and an appropriate ordering based on formula sizes or weights, such as

$C \sqsubseteq C'$ if and only if

$$ C \geq C' $$

and $(\text{size}(C) > \text{size}(C'))$

or $(\text{size}(C) = \text{size}(C'))$

and $C$ contains fewer distinct variables than $C'$).
Conversely, the $\sqsupset$ relation can be more general than subsumption. In Section 4, we will use it to justify the movement of formulas between sets in the given clause procedure.

**Example 49** There are a few applications, notably for superposition-based decision procedures [7], where one would like to define $Red_F^{G, \sqsupset}$ using the reverse instantiation ordering $\prec$. In this way, a clause $P(x)$ would for example become redundant in the presence of the clauses $P(b)$ and $P(c)$, provided that $b$ and $c$ are the only two ground terms. The reverse instantiation ordering is not well founded on the set of all first-order clauses: $P(x) \prec P(f(x)) \prec P(f(f(x))) \prec \dots$. However, it is well founded if we restrict it to the set of generalizations $gen(D) := \{C \mid D = C\theta \text{ for some } \theta\}$ of a fixed ground clause $D$, so that we may in fact define $\sqsupset := (\sqsupset_D)_D$ where $\sqsupset_D := \prec \cap (gen(D) \times gen(D))$. For this application, the possibility of taking $\sqsupset$ to be a $G$-indexed family of well-founded strict partial orderings, as opposed to a single such ordering, is vital.

### 3.3 Intersections of Liftings

The results of the previous subsection can be extended in a straightforward way to intersections of lifted redundancy criteria. As before, let $F$ and $G$ be two sets of formulas, and let $Finf$ be an $F$-inference system. In addition, let $Q$ be a nonempty set. For every $q \in Q$, let $\models^q$ be a consequence relation over $G$, let $GInf^q$ be a $G$-inference system, let $Red^q$ be a redundancy criterion for $\models^q$ and $GInf^q$, and let $G^q$ be a grounding function from $F$ and $Finf$ to $G$ and $GInf^q$. Let $\sqsupset := (\sqsupset_D)_D$ be a $G$-indexed family of well-founded strict partial orderings on $F$.<fnref n="3" />

For each $q \in Q$, we know by Theorem 42 that the $(G^q, \emptyset)$-lifting $Red^{q, G^q, \emptyset} = (Red_1^{q, G^q}, Red_F^{q, G^q, \emptyset})$ and the $(G^q, \sqsupset)$-lifting $Red^{q, G^q, \sqsupset} = (Red_1^{q, G^q}, Red_F^{q, G^q, \sqsupset})$ of $Red^q$ are redundancy criteria for $\models^q$ and $Finf$. Consequently, by Lemma 24 the intersections

$$Red^{\sqcap G} := (Red_1^{\sqcap G}, Red_F^{\sqcap G}) := (\bigcap_{q \in Q} Red_1^{q, G^q}, \bigcap_{q \in Q} Red_F^{q, G^q, \emptyset})$$

and

$$Red^{\sqcap G, \sqsupset} := (Red_1^{\sqcap G, \sqsupset}, Red_F^{\sqcap G, \sqsupset}) := (\bigcap_{q \in Q} Red_1^{q, G^q}, \bigcap_{q \in Q} Red_F^{q, G^q, \sqsupset})$$

are redundancy criteria for $\models^q := \bigcap_{q \in Q} \models^q$ and $Finf$.

We get the following analogue of Theorem 32.

**Theorem 50** If $(GInf^q, Red^q)$ is statically refutationally complete w.r.t. $\models^q$ for every $q \in Q$, and if for every $N \subseteq F$ that is saturated w.r.t. $Finf$ and $Red^{\sqcap G}$ there exists a $q$ such that $GInf^q(G^q(N)) \subseteq G^q(FInf(N)) \cup Red_1^q(G^q(N))$, then $(Finf, Red^{\sqcap G})$ is statically refutationally complete w.r.t. $\models^q$.

*Proof* Assume that $(GInf^q, Red^q)$ is statically refutationally complete w.r.t. $\models^q$ for every $q \in Q$ and that for every $N \subseteq F$ that is saturated w.r.t. $Finf$ and $Red^{\sqcap G}$ there exists a $q$ such that $GInf^q(G^q(N)) \subseteq G^q(FInf(N)) \cup Red_1^q(G^q(N))$.

<footnote n="3">³ We could also use a $Q$-indexed family of sets $(G^q)_{q \in Q}$ instead of a single set $G$, and a $(Q, G^q)$-indexed family of well-founded strict partial orderings on $F$ instead of a $G$-indexed family, but we are not aware of applications where this is necessary.</footnote>
Let $N \subseteq \mathbf{F}$ be saturated w.r.t. $\mathbf{Inf}$ and $\mathbf{Red}^{\cap G}$ and assume that $N \models_G^{\cap} \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$. We must show that $\perp' \in N$ for some $\perp' \in \mathbf{F}_{\perp}$. First, we know that there exists a $q$ such that $\mathbf{GInf}^q(\mathbf{G}^q(N)) \subseteq \mathbf{G}^q(\mathbf{Inf}(N)) \cup \mathbf{Red}_1^q(\mathbf{G}^q(N))$. Since $\mathbf{Red}^{\cap G} = \bigcap_{q \in Q} \mathbf{Red}^{q, \mathbf{G}^q, \emptyset}$, we know by Lemma 25 that $N$ is saturated w.r.t. $\mathbf{Inf}$ and the $(\mathbf{G}^q, \emptyset)$-lifting $\mathbf{Red}^{q, \mathbf{G}^q, \emptyset}$ of $\mathbf{Red}^q$. Therefore, by Lemma 31, $\mathbf{G}^q(N)$ is saturated w.r.t. $\mathbf{Inf}$ and $\mathbf{Red}^q$.

Furthermore, $N \models_G^{\cap} \{\perp\}$ implies $N \models_{\mathbf{G}^q}^{\cap} \{\perp\}$, and since $\models_{\mathbf{G}^q}^{\cap}$ is the $\mathbf{G}^q$-lifting of $\models^q$, this is equivalent to $\mathbf{G}^q(N) \models^q \mathbf{G}^q(\perp)$. By property (G1) of grounding functions, $\mathbf{G}^q(\perp)$ is a nonempty subset of $\mathbf{G}_{\perp}$. Let $\perp_G \in \mathbf{G}^q(\perp)$. Then $\mathbf{G}^q(N) \models \mathbf{G}^q(\perp) \models \{\perp_G\}$.

Since $\mathbf{G}^q(N)$ is saturated w.r.t. $\mathbf{Inf}$ and $\mathbf{Red}^q$, there must exist some $\perp'_G \in \mathbf{G}_{\perp}$ such that $\perp'_G \in \mathbf{G}^q(N)$. Hence $\perp'_G \in \mathbf{G}^q(C)$ for some $C \in N$, which implies $C \in \mathbf{F}_{\perp}$ by property (G2) of grounding functions. Now define $\perp' := C$. $\square$

Since the first components of $\mathbf{Red}^{\cap G}$ and $\mathbf{Red}^{\cap G, \sqsupset}$ agree, we obtain the analogues of Lemmas 43 and 44 and Theorem 45:

**Lemma 51** A set $N \subseteq \mathbf{F}$ is saturated w.r.t. $\mathbf{Inf}$ and $\mathbf{Red}^{\cap G, \sqsupset}$ if and only if it is saturated w.r.t. $\mathbf{Inf}$ and $\mathbf{Red}^{\cap G}$.

**Lemma 52** $(\mathbf{Inf}, \mathbf{Red}^{\cap G, \sqsupset})$ is statically refutationally complete w.r.t. $\models_G^{\cap}$ if and only if $(\mathbf{Inf}, \mathbf{Red}^{\cap G})$ is statically refutationally complete w.r.t. $\models_G^{\cap}$.

**Theorem 53** If $(\mathbf{Inf}, \mathbf{Red}^{\cap G})$ is statically refutationally complete w.r.t. $\models_G^{\cap}$, then $(\mathbf{Inf}, \mathbf{Red}^{\cap G, \sqsupset})$ is dynamically refutationally complete w.r.t. $\models_G^{\cap}$.

**Example 54** Intersections of liftings are needed to support selection functions in ordered resolution [6] and superposition [5]. The calculus $\mathbf{Inf}$ is parameterized by a function $f_{sel}$ on the set $\mathbf{F}$ of first-order clauses that selects a subset of the negative literals in each $C \in \mathbf{F}$. There are several ways to extend $f_{sel}$ to a selection function $g_{sel}$ on the set $\mathbf{G}$ of ground clauses such that for every $D \in \mathbf{G}$ there exists some $C \in \mathbf{F}$ such that $D = C\theta$ and $D$ and $C$ have corresponding selected literals.

For example, if $f_{sel}$ selects the first literal in $C_1 = \neg P(x) \lor \neg Q(c)$ and the second literal in $C_2 = \neg P(b) \lor \neg Q(y)$, then $g_{sel}$ could select the first literal in $D = \neg P(b) \lor \neg Q(c)$ (as in $C_1$) or the second literal (as in $C_2$). For every such $g_{sel}$, $\models_{g_{sel}}^{\sqsupset}$ is first-order entailment, $\mathbf{Inf}_{g_{sel}}$ is the set of ground inferences satisfying $g_{sel}$, and $\mathbf{Red}_{g_{sel}}$ is the redundancy criterion for $\mathbf{Inf}_{g_{sel}}$. The grounding function $\mathbf{G}_{g_{sel}}$ maps $C \in \mathbf{F}$ to $\{D \in \mathbf{G} \mid D = C\theta \text{ for some } \theta\}$ and $\iota \in \mathbf{Inf}$ to the set of ground instances of $\iota$ in $\mathbf{Inf}_{g_{sel}}$ with corresponding literals selected in the premises. If $\iota$ is the $\mathbf{Inf}$-inference

$$ \frac{\frac{\mathbf{P}(b) \quad \neg \mathbf{P}(x) \lor \neg \mathbf{Q}(c)}{\neg \mathbf{Q}(c)}}{\mathbf{P}(b) \quad \neg \mathbf{P}(b) \lor \neg \mathbf{Q}(c)} $$

where the first literal in the second premise $C_1$ is selected by $f_{sel}$, then

$$ \frac{\frac{\mathbf{P}(b) \quad \neg \mathbf{P}(b) \lor \neg \mathbf{Q}(c)}{\neg \mathbf{Q}(c)}}{\mathbf{P}(b) \quad \neg \mathbf{P}(b) \lor \neg \mathbf{Q}(c)} $$

is contained in $\mathbf{G}_{g_{sel}}(\iota) \subseteq \mathbf{Inf}_{g_{sel}}$ if $g_{sel}$ selects the first literal in the right premise (as in $C_1$) but it is not contained in $\mathbf{Inf}_{g_{sel}}$ (and hence not in $\mathbf{G}_{g_{sel}}(\iota)$) if $g_{sel}$ selects the second literal in the right premise (as in $C_2$).
In the static refutational completeness proof, only one *gsel* is needed, but this *gsel* depends on the limit of a derivation and is not known *during* the derivation. Therefore, fairness must be guaranteed w.r.t. $Red_1^{gsel, G^{gsel}}$ for every possible extension *gsel* of *fsel*. Checking $Red_1^{\cap G}$ amounts to a worst-case analysis, where we must assume that every ground instance $C\theta \in G$ of a premise $C \in F$ inherits the selection of *C*.

**Example 55** Intersections of liftings are also necessary for constraint superposition calculi (Nieuwenhuis and Rubio [29]). Here the calculus *Finf* operates on the set **F** of first-order clauses with (ordering and equality) constraints. For a convergent rewrite system *R*, $|-^R$ is first-order entailment up to *R* on the set **G** of unconstrained ground clauses, *GInf*<sup>*R*</sup> is the set of ground superposition inferences, and *Red*<sup>*R*</sup> is redundancy up to *R*. The grounding function *G*<sup>*R*</sup> maps $C[[K]] \in \mathbf{F}$ to {$D \in \mathbf{G} \mid D = C\theta, K\theta = \text{true}, x\theta \text{ is } \mathbf{R}\text{-irreducible for all } x$} (except in degenerate cases where *x* occurs only in positive literals *x* ≈ *t*) and *ι* ∈ *Finf* to the set of ground instances of *ι* where the premises and conclusion of *G*<sup>*R*</sup>(*ι*) are the *G*<sup>*R*</sup>-ground instances of the premises and conclusion of *ι*. In the static refutational completeness proof, only one particular *R* is needed, but this *R* is not known during a derivation, so fairness must be guaranteed w.r.t. $Red_1^{R, G^R}$ for every convergent rewrite system *R*. To obtain a practically useful criterion, the intersection $Red_1^{\cap G}$ must be approximated appropriately; compare Nieuwenhuis and Rubio's Definition 6.5 (which corresponds to our $Red_1^{\cap G}$) to their Lemma 6.18.

**Example 56** Some calculi have inference rules that introduce Skolem function symbols. An example is the $\delta$-elimination rule of Ganzinger and Stuber [23]. At the nonground level, the difficulty is that whenever we generate a conclusion with a fresh symbol $sk_j$, we need to mark all other instances of the rule with $sk_j$ ($j \neq i$) as redundant; otherwise, we would end up generating lots of needless conclusions. This determinism can be avoided by encoding enough information to identify the rule instance in the subscript *i*.

At the ground level, a second difficulty arises. The ground inference cannot simply introduce a nullary Skolem symbol—in general, this would not match the behavior of the corresponding nonground inference. Instead, it must guess both the Skolem symbol and its argument list. This guessing can be achieved using a selection function that takes the rule instance as argument and returns the Skolem term. We can then lift the ground inference by taking the intersection of all possible selection functions.

Almost every redundancy criterion for a nonground inference system *Finf* that can be found in the literature can be written as *Red*<sup>*G*, θ*</sup> for some grounding function *G* from **F** and *Finf* to **G** and *GInf*, and some redundancy criterion *Red* for *GInf*, or as an intersection *Red*<sup>*∩G*</sup> of such criteria. As Theorem 53 demonstrates, every static refutational completeness result for *Finf* and *Red*<sup>*∩G*</sup>—which does not generally support the deletion of subsumed formulas during a run—immediately yields a dynamic refutational completeness result for *Finf* and *Red*<sup>*∩G, ∩□*</sup>—which permits the deletion of subsumed formulas during a run, provided that they are larger according to ∩.

## 3.4 Adding Labels

In practice, the orderings $\square_D$ used in $(G, \square)$-liftings often depend on meta-information about a formula, such as its age or the way in which it has been processed so far during a derivation.
To capture this meta-information, we extend formulas and inference systems in a rather trivial way with labels.

As before, let **F** and **G** be two sets of formulas, let *Finf* be an **F**-inference system, let *GInf* be a **G**-inference system, let $|\subseteq P(\mathbf{G}) \times P(\mathbf{G})$ be a consequence relation over **G**, let *Red* be a redundancy criterion for $|=$ and *GInf*, and let **G** be a grounding function from **F** and *Finf* to **G** and *GInf*.

Let **L** be a nonempty set of labels. Define **FL** := **F** × **L** and **FL**<sub>⊥</sub> := **F**<sub>⊥</sub> × **L**. Notice that there are at least as many false values in **FL** as there are labels in **L**. We use *M*, *N* to denote labeled formula sets. Given a set *N* ⊆ **FL**, let |*N*| := {C | (C, l) ∈ *N*} denote the set of formulas without their labels.

We call an **FL**-inference system *FLInf* a labeled version of *Finf* if it has the following properties:

(L1) for every inference $(C_n, \dots, C_0) \in Finf$ and every tuple $(l_1, \dots, l_n) \in L^n$, there exists an $l_0 \in L$ and an inference $((C_n, l_n), \dots, (C_0, l_0)) \in FLInf$;

(L2) if $\iota = ((C_n, l_n), \dots, (C_0, l_0))$ is an inference in $FLInf$, then $(C_n, \dots, C_0)$ is an inference in $Finf$, denoted by $|\iota|$.

In other words, whenever there is an *Finf*-inference from some premises, there is a corresponding *FLInf*-inference from the labeled premises (regardless of the labeling), and whenever there is an *FLInf*-inference from labeled premises, there is a corresponding *Finf*-inference from the unlabeled premises.

Let *FLInf* be a labeled version of *Finf*. Define $G_L$ by $G_L(C, l) := G(C)$ for every $(C, l) \in FL$ and by $G_L(\iota) := G(|\iota|)$ for every $\iota \in FLInf$. The following lemmas are then obvious:

**Lemma 57** $G_L$ is a grounding function from $FL$ and $FLInf$ to $G$ and $GInf$.

Let $|\models_G$ be the $G_L$-lifting of $|\models$. Let $Red^{G_L, \emptyset}$ be the $(G_L, \emptyset)$-lifting of $Red$.

**Lemma 58** $\mathcal{N} \models_{G_L} \mathcal{N}'$ if and only if $|\mathcal{N}| \models_G |\mathcal{N}'|$.

**Lemma 59** If a set $\mathcal{N} \subseteq FL$ is saturated w.r.t. $FLInf$ and $Red^{G_L, \emptyset}$, then $|\mathcal{N}| \subseteq F$ is saturated w.r.t. $Finf$ and $Red^{G, \emptyset}$.

**Lemma 60** If $(Finf, Red^{G, \emptyset})$ is statically refutationally complete w.r.t. $|\models$, then $(FLInf, Red^{G_L, \emptyset})$ is statically refutationally complete w.r.t. $|\models_{G_L}$.

The extension to intersections of redundancy criteria is also straightforward. Let **F** and **G** be two sets of formulas, and let *Finf* be an **F**-inference system. Let *Q* be a nonempty set. For every *q* ∈ *Q*, let $|\models^q$ be a consequence relation over **G**, let *GInf*<sup>*q*</sup> be a **G**-inference system, let *Red*<sup>*q*</sup> be a redundancy criterion for $|\models^q$ and *GInf*<sup>*q*</sup>, and let **G**<sup>*q*</sup> be a grounding function from **F** and *Finf* to **G** and *GInf*<sup>*q*</sup>. Then for every *q* ∈ *Q*, the $(\mathcal{G}^q, \emptyset)$-lifting $Red^{q, \mathcal{G}^q, \emptyset}$ of *Red*<sup>*q*</sup> is a redundancy criterion for the $\mathcal{G}^q$-lifting $|\models_{\mathcal{G}^q}$ of $|\models$ and *Finf*, and so $Red^{\bigcap \mathcal{G}^q}$ is a redundancy criterion for $|\models_{\bigcap \mathcal{G}^q}$ and *Finf*.

Now let **L** be a nonempty set of labels, and define **FL**, **FL**<sub>⊥</sub>, and *FLInf* as above. For every *q* ∈ *Q*, define the function $G_L^q$ by $G_L^q(C, l) := G^q(C)$ for every $(C, l) \in FL$ and by $G_L^q(\iota) := G^q(|\iota|)$ for every $\iota \in FLInf$. By Lemma 57, every $G_L^q$ is a grounding function from **FL** and *FLInf* to **G** and *GInf*<sup>*q*</sup>. Then for every *q* ∈ *Q*, the $(G_L^q, \emptyset)$-lifting $Red^{q, G_L^q}$ = $(Red_1^{q, G_L^q}, Red_F^{q, G_L^q, \emptyset})$ of $Red^q$ is a redundancy criterion for the $G_L^q$-lifting $|\models_{G_L^q}$ of $|\models$ and *FLInf*, and so

$$Red^{\bigcap G_L} := (Red_1^{\bigcap G_L}, Red_F^{\bigcap G_L}) := \left( \bigcap_{q \in Q} Red_1^{q, G_L^q}, \bigcap_{q \in Q} Red_F^{q, G_L^q, \emptyset} \right)$$
is a redundancy criterion for $|\mathcal{G}_L^\cap| := \bigcap_{q \in Q} |\mathcal{G}_L^q|$ and *FLInf*.

Analogously to Lemmas 58–60, we obtain the following results:

**Lemma 61** *If $\mathcal{N} \models_{\mathcal{G}_L^\cap} \mathcal{N}'$ if and only if $[\mathcal{N}] \models_{\mathcal{G}} [\mathcal{N}']$.*

**Lemma 62** If a set $\mathcal{N} \subseteq \mathbf{FL}$ is saturated w.r.t. $\mathbf{FLInf}$ and $\mathbf{Red}^{\cap \mathcal{G}_L}$, then $[\mathcal{N}] \subseteq \mathbf{F}$ is saturated w.r.t. $\mathbf{Finf}$ and $\mathbf{Red}^{\cap \mathcal{G}}$.

**Theorem 63** If $(\mathbf{Finf}, \mathbf{Red}^{\cap \mathcal{G}})$ is statically refutationally complete w.r.t. $|\mathcal{G}|$, then $(\mathbf{FLInf}, \mathbf{Red}^{\cap \mathcal{G}_L})$ is statically refutationally complete w.r.t. $|\mathcal{G}_L^\cap|$.

# 4 Prover Architectures

We now use the above results to prove the refutational completeness of a popular prover architecture: the given clause procedure invented by McCune and Wos [28]. The architecture is parameterized by an inference system and a redundancy criterion. A generalization of the architecture decouples scheduling and computation of inferences, which has several benefits.

## 4.1 Given Clause Procedure

For this section, we fix the following. Let **F** and **G** be two sets of formulas, and let *Finf* be an **F**-inference system without premise-free inferences. Let *Q* be a nonempty set. For every *q* ∈ *Q*, let $|\cdot|^{=q}$ be a consequence relation over **G**, let *GInf*<sup>*q*</sup> be a **G**-inference system, let *Red*<sup>*q*</sup> be a redundancy criterion for $|\cdot|^{=q}$ and *GInf*<sup>*q*</sup>, and let *G*<sup>*q*</sup> be a grounding function from **F** and *Finf* to **G** and *GInf*<sup>*q*</sup>. Assume (*Finf*, *Red*<sup>∩G</sup>) is statically refutationally complete w.r.t. $|\cdot|^{\cap G}$.

Let **L** be a nonempty set of labels, let **FL** := **F** × **L**, and let the **FL**-inference system *FLInf* be a labeled version of *Finf*. By Theorem 63, (*FLInf*, *Red*<sup>∩G<sub>L</sub></sup>) is statically refutationally complete w.r.t. $|\cdot|^{\cap G<sub>L</sub>}$.

Let $\dot{=}^-$ be an equivalence relation on **F**, let $\succ$ be a well-founded strict partial ordering on **F** such that $\succ$ is compatible with $\dot{=}^-$ (i.e., $C \succ D$, $C \dot{=}^-$ $C'$, $D \dot{=}^-$ $D'$ implies $C' \succ D'$), such that $C \dot{=}^-$ D implies $\mathcal{G}^q(C) = \mathcal{G}^q(D)$ for all $q \in Q$, and such that $C \succ D$ implies $\mathcal{G}^q(C) \subseteq \mathcal{G}^q(D)$ for all $q \in Q$. We define $\dot{=}^+ := \succ \cup \dot{=}^-$$. In practice, $\dot{=}^-$ is typically $\alpha$-renaming (or equality if formulas are considered up to $\alpha$-equivalence), $\succ$ is either the instantiation ordering $\succ$ (Example 46), provided it is well founded, or some well-founded ordering included in $\succ$, and for every $q \in Q$, $\mathcal{G}^q$ maps every formula $C \in \mathbf{F}$ to the set of ground instances of $C$, possibly modulo some theory.

Let $\Box$ be a well-founded strict partial ordering on **L**. We define the ordering $\Box$ on **FL** by $(C, l) \Box (C', l')$ if either $C \succ C'$ or else $C \dot{=}^-$ $C'$ and $l \Box l'$. By Lemma 52, the static refutational completeness of $(\mathbf{FLInf}, \mathbf{Red}^{\cap \mathcal{G}_L})$ w.r.t. $|\cdot|^{\cap \mathcal{G}_L}$ implies the static refutational completeness of $(\mathbf{FLInf}, \mathbf{Red}^{\cap \mathcal{G}_L, \Box})$, which by Lemma 10 implies the dynamic refutational completeness of $(\mathbf{FLInf}, \mathbf{Red}^{\cap \mathcal{G}_L, \Box})$.

This result may look intimidating, so let us unroll it. The **FL**-inference system *FLInf* is a labeled version of *Finf*, which means that we get an *FLInf*-inference by first omitting the labels of the premises (*C*<sub>*n*</sub>, *l*<sub>*n*</sub>), ..., (*C*<sub>1</sub>, *l*<sub>1</sub>), then performing an *Finf*-inference (*C*<sub>*n*</sub>, ..., *C*<sub>0</sub>), and finally attaching an arbitrary label *l*<sub>0</sub> to the conclusion *C*<sub>0</sub>. Since the labeled grounding functions $\mathcal{G}_L^q$ differ from the corresponding unlabeled grounding functions $\mathcal{G}^q$ only by the omission of the labels and the first components of $\mathbf{Red}^{\cap \mathcal{G}_L, \Box}$ and $\mathbf{Red}^{\cap \mathcal{G}_L}$ agree, we get this result:
**Lemma 64** An FLInf-inference $\iota$ is redundant w.r.t. $\mathrm{Red}^{\cap G, \sqsupset}$ and $\mathcal{N}$ if and only if the underlying FInf-inference $\lceil \iota \rceil$ is redundant w.r.t. $\mathrm{Red}^{\cap G}$ and $\lceil \mathcal{N} \rceil$.

For $\mathrm{Red}_F^{\cap G, \sqsupset}$, we can show that a labeled formula $(C, l)$ is redundant if (i) $C$ itself is redundant w.r.t. $\mathrm{Red}_F^{\cap G}$, or if (ii) $C$ is $\Rightarrow$-subsumed, or if (iii) $C$ is a variant of another formula that occurs with a $\sqsupset$-smaller label. More formally:

**Lemma 65** Let $\mathcal{N} \subseteq \mathrm{FL}$, and let $(C, l)$ be a labeled formula. Then $(C, l) \in \mathrm{Red}_F^{\cap G, \sqsupset}(\mathcal{N})$ if one of the following conditions hold:

(i) $C \in \mathrm{Red}_F^{\cap G}(\lceil \mathcal{N} \rceil)$;

(ii) $C \Rightarrow C'$ for some $C' \in \lceil \mathcal{N} \rceil$;

(iii) $C \cong C'$ for some $(C', l') \in \mathcal{N}$ with $l \sqsupset l'$.

*Proof* (i) Let $C \in \mathrm{Red}_F^{\cap G}(\lceil \mathcal{N} \rceil)$. Then $C \in \mathrm{Red}_F^{q, G^q, \emptyset}(\lceil \mathcal{N} \rceil)$ for every $q \in \mathcal{Q}$, which means that $G^q(C) \subseteq \mathrm{Red}_F^q(G^q(\lceil \mathcal{N} \rceil))$. Now $G_L^q(C, l) = G^q(C)$ and $G^q(\lceil \mathcal{N} \rceil) = G_L^q(\mathcal{N})$; hence $G_L^q(C, l) \subseteq \mathrm{Red}_F^q(G_L^q(\mathcal{N}))$, which implies $(C, l) \in \mathrm{Red}_F^{q, G_L^q, \sqsupset}(\mathcal{N})$ for every $q \in \mathcal{Q}$ and thus $(C, l) \in \mathrm{Red}_F^{\cap G_L, \sqsupset}(\mathcal{N})$.

(ii) Assume that $C \Rightarrow C'$ for some $C' \in \lceil \mathcal{N} \rceil$. Then there exists a label $l'$ such that $(C', l') \in \mathcal{N}$. By the definition of $\sqsupset$, we have $(C, l) \sqsupset (C', l')$. Furthermore, $G^q(C) \subseteq G^q(C')$ for all $q \in \mathcal{Q}$. Therefore $G_L^q(C, l) = G^q(C) \subseteq G^q(C') = G_L^q(C', l')$, which implies $(C, l) \in \mathrm{Red}_F^{q, G_L^q, \sqsupset}(\mathcal{N})$ for every $q \in \mathcal{Q}$ and thus $(C, l) \in \mathrm{Red}_F^{\cap G_L, \sqsupset}(\mathcal{N})$.

(iii) If $C \Rightarrow C'$, the result follows from (ii). Otherwise $C \stackrel{\cdot}{=} C'$ for some $(C', l') \in \mathcal{N}$ with $l \sqsupset l'$. Then $(C, l) \sqsupset (C', l')$ and $G^q(C) = G^q(C')$, so $G_L^q(C, l) = G^q(C) = G^q(C') = G_L^q(C', l')$. This implies $(C, l) \in \mathrm{Red}_F^{q, G_L^q, \sqsupset}(\mathcal{N})$ for every $q \in \mathcal{Q}$; therefore, $(C, l) \in \mathrm{Red}_F^{\cap G_L, \sqsupset}(\mathcal{N})$. $\square$

The given clause procedure that lies at the heart of saturation provers can be presented and studied abstractly.<fnref n="4" /> We assume that the set of labels **L** contains at least two values, one of which is a distinguished $\sqsupset$-smallest value denoted by active, and that the labeled version *FLInf* of *FInf* never assigns the label active to a conclusion.

The state of a prover is a set of labeled formulas. The label identifies to which formula set each formula belongs. The active label identifies the active formula set from the given clause procedure. The other, unspecified formula sets are considered passive. Given a set $\mathcal{N}$ and a label $l$, we define the projection $\mathcal{N} \downarrow_l$ as consisting only of the formulas labeled by $l$.

The given clause prover GC is defined as the following transition system:

PROCESS $\mathcal{N} \cup \mathcal{M} \Rightarrow_{\mathrm{GC}} \mathcal{N} \cup \mathcal{M}'$
where $\mathcal{M} \subseteq \mathrm{Red}_F^{\cap G_L, \sqsupset}(\mathcal{N} \cup \mathcal{M}')$ and $\mathcal{M}' \downarrow_{\mathrm{active}} = \emptyset$

INFER $\mathcal{N} \cup \{(C, l)\} \Rightarrow_{\mathrm{GC}} \mathcal{N} \cup \{(C, \mathrm{active})\} \cup \mathcal{M}$
where $l \neq \mathrm{active}$, $\mathcal{M} \downarrow_{\mathrm{active}} = \emptyset$, and
$\mathrm{FLInf}(\lceil \mathcal{N} \downarrow_{\mathrm{active}} \rceil, \{C\}) \subseteq \mathrm{Red}_1^{\cap G}(\lceil \mathcal{N} \rceil \cup \{C\} \cup \lceil \mathcal{M} \rceil)$

The initial state consists of the input formulas, paired with arbitrary labels different from active. A key invariant of the given clause procedure is that all inferences from active formulas are redundant w.r.t. the current set of formulas.

The PROCESS rule covers most operations performed in a theorem prover. By Lemma 65, this includes

<footnote n="4">⁴ We keep the traditional term “given clause procedure” even though our framework is not restricted to clauses.</footnote>
- deleting $Red_F^{\cap G}$-redundant formulas with arbitrary labels and adding formulas that make other formulas $Red_F^{\cap G}$-redundant (i.e., simplifying w.r.t. $Red_F^{\cap G}$), by (i);

- deleting formulas that are $\triangleright$-subsumed by other formulas with arbitrary labels, by (ii);

- deleting formulas that are $\succeq$-subsumed by other formulas with smaller labels, by (iii);

- replacing the label of a formula by a smaller label different from active, also by (iii).

Like for $\triangleright_{Red}$, in practice the added formulas would normally be entailed by $N$, but we impose no soundness restrictions.

INFER is the only rule that puts a formula in the active set. It relabels a passive formula $C$ to active and ensures that all inferences between $C$ and the active formulas, including $C$ itself, become redundant. Recall that by Lemma 64, $FLInf(\mathcal{N}_{\downarrow active}, \{(C, active)\}) \subseteq Red_1^{\cap G_L}(\mathcal{N} \cup \{(C, active)\} \cup \mathcal{M})$ if and only if $Finf(\lfloor \mathcal{N}_{\downarrow active} \rfloor, \{C\}) \subseteq Red_1^{\cap G}(\lfloor \mathcal{N} \rfloor \cup \{C\} \cup \lfloor \mathcal{M} \rfloor)$. By property (R4) of redundancy criteria, every inference is redundant if its conclusion is contained in the set of formulas, and typically, inferences are in fact made redundant by adding their conclusions to any of the passive sets. Then, $\lfloor \mathcal{M} \rfloor$ equals $concl(FInf(\lfloor \mathcal{N}_{\downarrow active} \rfloor, \{C\}))$. There are, however, some techniques commonly implemented in theorem provers for which we need INFER's side condition in full generality.

**Lemma 66** Every $\implies \text{GC}$-derivation is a $\triangleright_{Red}^{\cap G_L}$-derivation.

*Proof* We need to show that every labeled formula that is deleted in a $\implies \text{GC}$-step is $Red^{\cap G_L}$-redundant w.r.t. the remaining labeled formulas. For PROCESS, this is trivial. For INFER, the only deleted formula is $(C, l)$, which is $Red^{\cap G_L}$-redundant w.r.t. $(C, active)$ by part (iii) of Lemma 65, since $l \sqsupseteq$ active. $\square$

Since $(FLInf, Red^{\cap G_L})$ is dynamically refutationally complete, it now suffices to show fairness to prove the refutational completeness of GC. Given $k \in \mathbb{N} \cup \{\infty\}$, let $Inv_{\mathcal{N}}(k)$ denote the condition

$$FLInf(\mathcal{N}_k \downarrow \text{active}) \subseteq \bigcup_{i=0}^{k} Red_1^{\cap G_L}(\mathcal{N}_i).$$

If $(\mathcal{N}_i)_i$ is a $\triangleright_{Red}^{\cap G_L}$-derivation and $k \in \mathbb{N}$, by (R2) and (R3), the right-hand side is equal to $Red_1^{\cap G_L}(\mathcal{N}_k)$. We will show that $Inv_{\mathcal{N}}(i)$ is an invariant of GC and that it extends to the limit, enabling us to establish fairness: $FLInf(\mathcal{N}_{\infty}) \subseteq \bigcup_i Red_1^{\cap G_L}(\mathcal{N}_i)$.

**Lemma 67** Let $(\mathcal{N}_i)_i$ be a $\implies \text{GC}$-derivation. If $\mathcal{N}_0 \downarrow \text{active} = \emptyset$, then $Inv_{\mathcal{N}}(k)$ holds for all indices $k$.

*Proof* BASE CASE: The hypothesis $\mathcal{N}_0 \downarrow \text{active} = \emptyset$ and the exclusion of premise-free inferences ensure that $FLInf(\downarrow \text{active}) = \emptyset$ and hence $Inv_{\mathcal{N}}(0)$ holds.

CASE PROCESS: Consider the step $\mathcal{N}_k = \mathcal{N} \cup \mathcal{M} \implies \text{GC} \mathcal{N} \cup \mathcal{M}' = \mathcal{N}_{k+1}$. We have the inclusion chain $FLInf(\mathcal{N}_{k+1} \downarrow \text{active}) \subseteq FLInf(\mathcal{N}_k \downarrow \text{active}) \subseteq \bigcup_{i=0}^k Red_1^{\cap G_L}(\mathcal{N}_i) \subseteq \bigcup_{i=0}^{k+1} Red_1^{\cap G_L}(\mathcal{N}_i)$. The first inclusion relies on PROCESS's side condition that $\mathcal{M}' \downarrow \text{active} = \emptyset$. The second inclusion corresponds to the induction hypothesis.

CASE INFER: Consider the step $\mathcal{N}_k = \mathcal{N} \cup \{(C, l)\} \implies \text{GC} \mathcal{N} \cup \{(C, active)\} \cup \mathcal{M} = \mathcal{N}_{k+1}$. We assume $l \in FLInf(\mathcal{N}_{k+1} \downarrow \text{active})$ for some $l$ and show $l \in \bigcup_{i=0}^{k+1} Red_1^{\cap G_L}(\mathcal{N}_i)$. If $l \in FLInf(\lfloor \mathcal{N}_{\downarrow active} \rfloor, (C, active))$, then $l \in Red_1^{\cap G_L}(\mathcal{N}_{k+1})$ by INFER's last side condition. Otherwise, $l \in FLInf(\lfloor \mathcal{N}_{\downarrow active} \rfloor)$ by INFER's side condition that $\mathcal{M} \downarrow \text{active} = \emptyset$. By the induction hypothesis, $l \in \bigcup_{i=0}^k Red_1^{\cap G_L}(\mathcal{N}_i)$. In both cases, $l \in \bigcup_{i=0}^{k+1} Red_1^{\cap G_L}(\mathcal{N}_i)$. $\square$
**Lemma 68** Let $(\mathcal{N}_i)_i$ be a nonempty $\mathcal{P}(\mathbf{FL})$-sequence. If $\mathrm{Inv}_{\mathcal{N}}(i)$ holds for all indices $i$, then $\mathrm{Inv}_{\mathcal{N}}(\infty)$ holds.

*Proof* We assume $\iota \in \mathrm{FLInf}(\mathcal{N}_{\infty}\downarrow_{\mathrm{active}})$ for some $\iota$ and show $\iota \in \bigcup_i \mathrm{Red}_1^{\cap \mathcal{G}_L}(\mathcal{N}_i)$. For $\iota$ to be in $\mathrm{FLInf}(\mathcal{N}_{\infty}\downarrow_{\mathrm{active}})$, all of its finitely many premises must be in $\mathcal{N}_{\infty}\downarrow_{\mathrm{active}}$. Therefore, there must exist an index $k$ such that $\mathcal{N}_{k}\downarrow_{\mathrm{active}}$ contains all of them, and therefore $\iota \in \mathrm{FLInf}(\mathcal{N}_{k}\downarrow_{\mathrm{active}})$. Since $\mathrm{Inv}_{\mathcal{N}}(k)$ holds, $\iota \in \bigcup_{i=0}^k \mathrm{Red}_1^{\cap \mathcal{G}_L}(\mathcal{N}_i) \subseteq \bigcup_i \mathrm{Red}_1^{\cap \mathcal{G}_L}(\mathcal{N}_i)$. $\square$

**Lemma 69** Let $(\mathcal{N}_i)_i$ be a $\implies_{\mathrm{GC}}$-derivation. If $\mathcal{N}_0\downarrow_{\mathrm{active}} = \emptyset$ and $\mathcal{N}_{\infty}\downarrow_l = \emptyset$ for all $l \neq$ active, then $(\mathcal{N}_i)_i$ is fair.

*Proof* By Lemmas 67 and 68, $\mathrm{FLInf}(\mathcal{N}_{\infty}\downarrow_{\mathrm{active}}) \subseteq \bigcup_i \mathrm{Red}_1^{\cap \mathcal{G}_L}(\mathcal{N}_i)$. By the second hypothesis, this inclusion simplifies to $\mathrm{FLInf}(\mathcal{N}_{\infty}) \subseteq \bigcup_i \mathrm{Red}_1^{\cap \mathcal{G}_L}(\mathcal{N}_i)$. $\square$

**Theorem 70** Let $(\mathcal{N}_i)_i$ be a $\implies_{\mathrm{GC}}$-derivation, where $\mathcal{N}_0\downarrow_{\mathrm{active}} = \emptyset$ and $\mathcal{N}_{\infty}\downarrow_l = \emptyset$ for all $l \neq$ active. If $\lfloor \mathcal{N}_0 \rfloor \models_G^{\cap} \{\perp\}$ for some $\perp \in \mathbf{F}_{\perp}$, then some $\mathcal{N}_i$ contains $(\perp', l)$ for some $\perp' \in \mathbf{F}_{\perp}$ and $l \in \mathbf{L}$.

*Proof* By Lemma 61, $\lfloor \mathcal{N}_0 \rfloor \models_G^{\cap} \{\perp\}$ is equivalent to $\mathcal{N}_0 \models_G^{\cap} \{(\perp, \mathrm{active})\}$. By Lemmas 66 and 69, we know that $(\mathcal{N}_i)_i$ is a fair $\triangleright_{\mathrm{Red}^{\cap \mathcal{G}_L, \sqsupset}}$-derivation. Since $(\mathrm{FLInf}, \mathrm{Red}^{\cap \mathcal{G}_L, \sqsupset})$ is dynamically refutationally complete, we can conclude that some $\mathcal{N}_i$ contains $(\perp', l)$ for some $\perp' \in \mathbf{F}_{\perp}$ and $l \in \mathbf{L}$. $\square$

**Example 71** The following Otter loop [28, Section 2.3.1] prover OL is an instance of the given clause prover GC. This loop design is inspired by Weidenbach's prover without splitting from his *Handbook* chapter [46, Tables 4–6]. The prover's state is a five-tuple $N | X | P | Y | A$ of formula sets. The $N$, $P$, and $A$ sets store the new, passive, and active formulas, respectively. The $X$ and $Y$ sets are subsingletons (i.e., sets of at most one element) that can store a chosen new or passive formula, respectively. Initial states are of the form $N | \emptyset | \emptyset | \emptyset | \emptyset$.

CHOOSEN $N \uplus \{C\} | \emptyset | P | \emptyset | A \implies_{\mathrm{OL}} N | \{C\} | P | \emptyset | A$

DELETEFWD $N | \{C\} | P | \emptyset | A \implies_{\mathrm{OL}} N | \emptyset | P | \emptyset | A$ \\
\qquad if $C \in \mathrm{Red}_F^{\cap G}(P \cup A)$ or $C \supseteq C'$ for some $C' \in P \cup A$

SIMPLIFYFWD $N | \{C\} | P | \emptyset | A \implies_{\mathrm{OL}} N | \{C'\} | P | \emptyset | A$ \\
\qquad if $C \in \mathrm{Red}_F^{\cap G}(P \cup A \cup \{C'\})$

DELETEBWDP $N | \{C\} | P \uplus \{C'\} | \emptyset | A \implies_{\mathrm{OL}} N | \{C\} | P | \emptyset | A$ \\
\qquad if $C' \in \mathrm{Red}_F^{\cap G}(\{C\})$ or $C' \succ C$

SIMPLIFYBWDP $N | \{C\} | P \uplus \{C'\} | \emptyset | A \implies_{\mathrm{OL}} N \cup \{C''\} | \{C\} | P | \emptyset | A$ \\
\qquad if $C' \in \mathrm{Red}_F^{\cap G}(\{C, C''\})$

DELETEBWDA $N | \{C\} | P | \emptyset | A \uplus \{C'\} \implies_{\mathrm{OL}} N | \{C\} | P | \emptyset | A$ \\
\qquad if $C' \in \mathrm{Red}_F^{\cap G}(\{C\})$ or $C' \succ C$

SIMPLIFYBWDA $N | \{C\} | P | \emptyset | A \uplus \{C'\} \implies_{\mathrm{OL}} N \cup \{C''\} | \{C\} | P | \emptyset | A$ \\
\qquad if $C' \in \mathrm{Red}_F^{\cap G}(\{C, C''\})$

TRANSFER $N | \{C\} | P | \emptyset | A \implies_{\mathrm{OL}} N | \emptyset | P \cup \{C\} | \emptyset | A$

CHOOSEP $\emptyset | \emptyset | P \uplus \{C\} | \emptyset | A \implies_{\mathrm{OL}} \emptyset | \emptyset | P | \{C\} | A$
$$
\begin{array}{l}
\text{INFER } \emptyset | \emptyset | P | \{C\} | A \implies_{\text{OL}} M | \emptyset | P | \emptyset | A \cup \{C\} \\
\text{if } F\text{Inf}(A, \{C\}) \subseteq \text{Red}_1^{\cap G}(A \cup \{C\} \cup M)
\end{array}
$$

Weidenbach identifies the X and Y components of OL's five-tuples; this is possible since
the former is used only in his inner loop, whereas the latter is used only in his outer loop.

If we are interested in soundness, we can require that the formulas added by simplifica-
tion and `INFER` are `≈`-entailed by the formulas in the state before the transition. This can be
relaxed to consistency preservation—e.g., for calculi that perform skolemization.

A reasonable strategy for applying the OL rules is presented below. It relies on a well-
founded ordering ≻ on formulas to ensure that the simplification rules actually “simplify”
their target, preventing nontermination of the inner loop. It also assumes that $F\text{Inf}(N, \{C\})$
is finite if $N$ is finite.

1. Repeat while $N \cup P \neq \emptyset$ and $\perp \notin N \cup P \cup A$:

1.1. Repeat while $N \neq \emptyset$:

1.1.1. Apply `CHOOSEN` to retrieve the next formula `C` from the state's `N` compo-
nent, which is organized as a queue.

1.1.2. Apply SIMPLIFYFWD as long as the simplified formula $C'$ is ≻-smaller than the original formula $C$.

1.1.3. If DELETEFWD is applicable, apply it.

1.1.4. Otherwise:

1.1.4.1. Apply DELETEBWDP and DELETEBWDA exhaustively.

1.1.4.2. Apply SIMPLIFYBWDP and SIMPLIFYBWDA as long as the sim-
plified formula $C''$ is ≻-smaller than the original formula $C'$.

1.1.4.3. Apply TRANSFER.

1.2. If $P \neq \emptyset$:

1.2.1. Apply `CHOOSEP`. Make sure that the choice of `C` is fair.

1.2.2. Apply `INFER` with $M = \text{concl}(F\text{Inf}(A, \{C\}))$.

Let $(N_i | X_i | P_i | Y_i | A_i)_i$ be a $\implies_{\text{OL}}$-derivation that follows the strategy, where $N_0$ is finite and $X_0 = P_0 = Y_0 = A_0 = \emptyset$. If the outer loop terminates because $\perp \in N \cup P \cup A$, the condition of dynamic refutational completeness is trivially satisfied. Otherwise, the argument is as follows. With each application of a rule other than `INFER`, the state, viewed as a multiset of labeled formulas, decreases w.r.t. the multiset extension of a relation that compares formulas using $\succ$ and breaks ties using $\sqsupseteq$ on the labels. This ensures no formula is left in $N$ or $X$ forever. The fair choice of $C$ ensures that no formula is left in $P$ forever, and the application of `INFER` following `CHOOSEP` ensures the same about $Y$. As a result, we have $N_\infty = X_\infty = P_\infty = Y_\infty = \emptyset$. Therefore, by Theorem 70, OL is dynamically refutationally complete.

In most saturation calculi, *Red* is defined in terms of some total well-founded ordering ≻<sub>G</sub> on **G**. We can then define ≻ so that *C* ≻ *C'* if the smallest element of *G*<sup>*q*</sup>(*C*) is greater than the smallest element of *G*<sup>*q*</sup>(*C'*). w.r.t. ≻<sub>G</sub>, for some arbitrary fixed *q* ∈ *Q*. This allows a wide range of simplifications implemented in resolution or superposition provers.

To ensure fairness, the heuristic used to apply `CHOOSEP` must guarantee that no formula
remains indefinitely in `P`. Fair choice strategies typically rely on formula age, which can be
represented through labels. Consider labeled formulas `(C,t)`, where `t` is the timestamp, and
a labeled version of OL where formulas introduced by simplification or `INFER` are labeled
with strictly increasing timestamps.
**Example 72** One fair formula choice strategy is to alternate between heuristically choosing $n$ formulas and taking the formula with the smallest timestamp [28, Section 2.3.1].

*Proof* By contradiction. Assume $P_{\infty} \neq \emptyset$. Consider the formula $(C,t) \in P_{\infty}$ with the smallest timestamp $t$. There exists an index $i$ such that $C$ is the formula with the smallest timestamp in $P_i$. After at most $n+1$ applications of CHOOSEP, $C$ will be chosen. $\square$

**Example 73** Another fair option is to use an $\mathbb{N}$-valued weight function $w$ that is strictly monotonic in the timestamp—i.e., for any unlabeled formula $C$, if $t < t'$, then $w(C,t) < w(C,t')$—and take a formula with the smallest weight [37, Section 4].

*Proof* Consider the labeled formula $(C,t)$ with the smallest weight in $P_{\infty}$. The weight function satisfies the inequation $n \le w(D,n)$ for every $n$ and every unlabeled $D$. Therefore, after $w(C,t)$ applications of INFER, new formulas introduced by simplification or INFER all have a weight larger than $(C,t)$, and thus CHOOSEP will eventually have to choose $(C,t)$. $\square$

**Example 74** In its superposition module [20], iProver implements a rule that eliminates the chosen passive clause, or *given clause*, if it is redundant w.r.t. a subset of its child clauses together with the active set. The following iProver loop proves this. It is based on GC and consists of all the OL transition rules and of the following rule:

$$ \begin{array}{l} \text{REPLACE } \emptyset | \emptyset | P | \{C\} | A \quad \Rightarrow_{\text{IL}} \quad M | \emptyset | P | \emptyset | A \\ \text{if either } C \in \text{Red}_{\text{F}}^{\cap G}(A \cup M) \text{ or else } M = \{C'\} \text{ and } C \leadsto C' \end{array} $$

As $M$, iProver would use a set of possibly simplified clauses from $concl(FInf(A, \{C\}))$.

**Example 75** Bachmair and Ganzinger's resolution prover RP [6, Section 4.3] is another instance of GC. It embodies both a concrete prover architecture and a concrete inference system: ordered resolution with selection ($O_S^>$). States are triples $N | P | O$ of finite clause sets consisting of new, processed, and old (active) clauses, respectively. The instantiation relies on three labels $l_3 \sqsubseteq l_2 \sqsubseteq l_1$ = active. Subsumption can be supported as described in Example 46.

$$ \begin{array}{l} \text{TAUTO} \quad N \cup \{C\} | P | O \quad \Rightarrow_{\text{RP}} \quad N | P | O \\ \text{if } C \text{ is a tautology} \end{array} $$

$$ \begin{array}{l} \text{DELETEFWD} \quad N \cup \{C\} | P | O \quad \Rightarrow_{\text{RP}} \quad N | P | O \\ \text{if some clause in } P \cup O \text{ subsumes } C \end{array} $$

$$ \begin{array}{l} \text{REDUCEFWD} \quad N \cup \{C \lor L\} | P | O \quad \Rightarrow_{\text{RP}} \quad N \cup \{C\} | P | O \\ \text{if there is a clause } D \lor L' \text{ in } P \cup O \text{ such that } \bar{L} = L'\sigma \text{ and } D\sigma \subseteq C \end{array} $$

$$ \begin{array}{l} \text{DELETEBWDP} \quad N | P \cup \{C\} | O \quad \Rightarrow_{\text{RP}} \quad N | P | O \\ \text{if some clause in } N \text{ properly subsumes } C \end{array} $$

$$ \begin{array}{l} \text{REDUCEBWDP} \quad N | P \cup \{C \lor L\} | O \quad \Rightarrow_{\text{RP}} \quad N | P \cup \{C\} | O \\ \text{if there is a clause } D \lor L' \text{ in } N \text{ such that } \bar{L} = L'\sigma \text{ and } D\sigma \subseteq C \end{array} $$

$$ \begin{array}{l} \text{DELETEBWDO} \quad N | P | O \cup \{C\} \quad \Rightarrow_{\text{RP}} \quad N | P | O \\ \text{if some clause in } N \text{ properly subsumes } C \end{array} $$

$$ \begin{array}{l} \text{REDUCEBWDO} \quad N | P | O \cup \{C \lor L\} \quad \Rightarrow_{\text{RP}} \quad N | P \cup \{C\} | O \\ \text{if there is a clause } D \lor L' \text{ in } N \text{ such that } \bar{L} = L'\sigma \text{ and } D\sigma \subseteq C \end{array} $$

$$ \text{CHOOSE} \quad N \cup \{C\} | P | O \quad \Rightarrow_{\text{RP}} \quad N | P \cup \{C\} | O $$

$$ \begin{array}{l} \text{INFER} \quad \emptyset | P \cup \{C\} | O \quad \Rightarrow_{\text{RP}} \quad N | P | O \cup \{C\} \\ \text{if } N = \text{concl}(O_S^>(O,C)) \end{array} $$
Let $(N_i | P_i | O_i)_i$ be a $\Rightarrow \mathbb{R}$-derivation, where $P_0 = O_0 = \emptyset$. Since the transition system excluding `INFER` terminates [37, Section 4] and we can always apply `CHOOSE` to empty $N$, we have $N_\infty = \emptyset$. The key restriction that is needed to ensure fairness is that the choice of $C$ in `INFER` must be fair. This ensures $P_\infty = \emptyset$. Thus, by Theorem 70, RP is dynamically refutationally complete. Incidentally, our version of RP repairs a small mistake in Bachmair and Ganzinger's definition of the notation $Inf(N, \{C\})$, used in the `INFER` rule [36, Section 7.1].

## 4.2 Delayed Inferences

The given clause prover GC presented in the previous subsection is sufficient to describe a prover based on an Otter loop as well as a basic DISCOUNT loop prover—which differs from the Otter loop prover OL in that the passive formulas are neither simplified or deleted using SIMPLIFYBWDP or DELETEBWDP, nor are they used to simplify or delete other formulas in SIMPLIFYFWD or DELETEFWD. To describe a DISCOUNT loop prover with orphan formula deletion, however, we need to extend GC.

An orphan formula is a passive formula generated by an inference for which at least one premise is no longer active. To model orphan formula deletion, we need to decouple the scheduling of inferences and their computation. The same scheme can be used to model provers based on inference systems that contain premise-free inferences or that may generate infinitely many conclusions from finitely many premises. Yet another use of the scheme is to save memory: A delayed inference can be stored more compactly than a new formula, as a tuple of premises together with instructions on how to compute the conclusion.

The lazy given clause prover LGC generalizes GC. It is defined as the following transition system on pairs $(T, \mathcal{N})$, where $T$ ("to do") is a set of scheduled inferences and $\mathcal{N}$ is a set of labeled formulas. We use the same assumptions as for GC except that we now permit premise-free inferences in $Finf$.

$$ \textbf{PROCESS} \quad (T, \mathcal{N} \cup \mathcal{M}) \Rightarrow_{\text{LGC}} (T, \mathcal{N} \cup \mathcal{M}') \\ \text{where } \mathcal{M} \subseteq \text{Red}_{\text{F}}^{\mathcal{G}, \vdash} (\mathcal{N} \cup \mathcal{M}') \text{ and } \mathcal{M}' \downarrow_{\text{active}} = \emptyset $$

$$ \textbf{SCHEDULEINFER} \quad (T, \mathcal{N} \cup \{(C, l)\}) \Rightarrow_{\text{LGC}} (T \cup T', \mathcal{N} \cup \{(C, \text{active})\}) \\ \text{where } l \neq \text{active} \text{ and } T' = \text{Finf}(\lfloor \mathcal{N} \downarrow_{\text{active}} \rfloor, \{C\}) $$

$$ \textbf{COMPUTEINFER} \quad (T \cup \{\iota, \mathcal{N}\}) \Rightarrow_{\text{LGC}} (T, \mathcal{N} \cup \mathcal{M}) \\ \text{where } \mathcal{M} \downarrow_{\text{active}} = \emptyset \text{ and } \iota \in \text{Red}_{\text{I}}^{\mathcal{G}} (\lfloor \mathcal{N} \cup \mathcal{M} \rfloor) $$

$$ \textbf{DELETEORPHANS} \quad (T \cup T', \mathcal{N}) \Rightarrow_{\text{LGC}} (T, \mathcal{N}) \\ \text{where } T' \cap \text{Finf}(\lfloor \mathcal{N} \downarrow_{\text{active}} \rfloor) = \emptyset $$

Initial states are states $(T, \mathcal{N})$ such that $T$ consists of all premise-free inferences of $Finf$ and $\mathcal{N}$ contains the input formulas paired with arbitrary labels different from active. A key invariant of LGC is that all inferences from active formulas are either scheduled in $T$ or redundant w.r.t. $\mathcal{N}$.

`PROCESS` has the same behavior as the corresponding GC rule, except for the additional $T$ component, which it ignores.

The `INFER` rule of GC is split into two parts in LGC: `SCHEDULEINFER` relabels a passive formula $C$ to active and puts all inferences between $C$ and the active formulas, including $C$ itself, into the set $T$. `COMPUTEINFER` removes an inference from $T$ and ensures that it becomes redundant by adding appropriate labeled formulas to $\mathcal{N}$ (typically the conclusion of the inference).
DELETEORPHANS can delete scheduled inferences from T if some of their premises have been deleted from $\mathcal{N}_{\downarrow\text{active}}$ in the meantime by an application of PROCESS. Note that the rule cannot delete premise-free inferences, since the side condition is then trivially false.

Abstractly, the T component of the state is a set of inferences $(C_n, \dots, C_0)$. In an actual implementation, it can be represented in different ways: as a set of compactly encoded recipes for computing the conclusion $C_0$ from the premises $(C_n, \dots, C_1)$ as in Waldmeister [24], or as a set of explicit formulas $C_0$ with information about their parents $(C_n, \dots, C_1)$ as in E [39]. In the latter case, some presimplifications may be performed on $C_0$; this could be modeled more faithfully by defining T as a set of pairs $(\iota, \text{simp}(C_0))$.

**Lemma 76** If $(T_i, \mathcal{N}_i)_i$ is an $\implies_{\text{LGC}}$-derivation, then $(\mathcal{N}_i)_i$ is a $\triangleright_{\text{Red}^\cap\text{G}_L, \sqsupset\sqcap}$-derivation.

*Proof* We must show that every labeled formula that is deleted in an $\implies_{\text{LGC}}$-step from the $\mathcal{N}$ component is $\text{Red}^\cap\text{G}_L, \sqsupset\sqcap$-redundant w.r.t. the remaining labeled formulas. For PROCESS this is trivial. For SCHEDULEINFER, the only deleted formula is $(C, l)$, which is $\text{Red}^\cap\text{G}_L, \sqsupset\sqcap$-redundant w.r.t. (C, active) by part (iii) of Lemma 65, since $l \sqsupset\sqcap$ active. Finally, the rules COMPUTEINFER and DELETEORPHANS do not delete any formulas. $\square$

Given $k \in \mathbb{N} \cup \{\infty\}$, let $\text{Inv}_{T, \mathcal{N}}(k)$ denote the condition

$$ \text{FLInf}(\mathcal{N}_{k \downarrow \text{active}}) \subseteq [T_k] \cup \bigcup_{i=0}^{k} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i) $$

where $\iota \in [T]$ if and only if $\lceil \iota \rceil \in T$ for every $\iota$ and every $T$. We will show that $\text{Inv}_{T, \mathcal{N}}(i)$ is an invariant of LGC and that it extends to the limit, enabling us to establish fairness.

**Lemma 77** Let $(T_i, \mathcal{N}_i)_i$ be an $\implies_{\text{LGC}}$-derivation. If $\mathcal{N}_{0 \downarrow \text{active}} = \emptyset$ and $T_0 \supset \text{FLInf}(\emptyset)$, then $\text{Inv}_{T, \mathcal{N}}(k)$ holds for all indices $k$.

*Proof* BASE CASE: The hypotheses ensure that $\text{FLInf}(\mathcal{N}_{0 \downarrow \text{active}}) = \text{FLInf}(\emptyset) \subseteq [T_0]$.

CASE PROCESS: This case is essentially as in the proof of Lemma 67.

CASE SCHEDULEINFER: Consider the step $(T_k, \mathcal{N}_k) = (T, \mathcal{N} \cup \{(C, l)\}) \implies_{\text{LGC}} (T \cup T', \mathcal{N} \cup \{(C, \text{active})\}) = (T_{k+1}, \mathcal{N}_{k+1})$. We assume $\iota \in \text{FLInf}(\mathcal{N}_{k+1} \downarrow \text{active})$ for some $\iota$ and show $\iota \in [T \cup T'] \cup \bigcup_{i=0}^{k+1} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. If $\iota \in \text{FLInf}(\mathcal{N}_{\downarrow \text{active}}, (C, \text{active}))$, then $\lceil \iota \rceil \in T'$ by definition of $T'$ and thus $\iota \in [T \cup T']$. Otherwise, $\iota \in \text{FLInf}(\mathcal{N}_{\downarrow \text{active}})$. By the induction hypothesis, $\iota \in [T] \cup \bigcup_{i=0}^{k} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. In both cases, $\iota \in [T \cup T'] \cup \bigcup_{i=0}^{k+1} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$.

CASE COMPUTEINFER: Consider the step $(T_k, \mathcal{N}_k) = (T \cup \{\iota'\}, \mathcal{N}) \implies_{\text{LGC}} (T, \mathcal{N} \cup \mathcal{M}) = (T_{k+1}, \mathcal{N}_{k+1})$. We assume $\iota \in \text{FLInf}(\mathcal{N}_{k+1} \downarrow \text{active})$ for some $\iota$ and show $\iota \in [T] \cup \bigcup_{i=0}^{k+1} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. By COMPUTEINFER's side condition that $\mathcal{M}_{\downarrow\text{active}} = \emptyset$, we have that $\iota \in \text{FLInf}(\mathcal{N}_{\downarrow\text{active}})$. By the induction hypothesis, $\iota \in [T \cup \{\iota'\}] \cup \bigcup_{i=0}^{k} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. If $\iota \in [\{\iota'\}]$, then $\iota \in \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N} \cup \mathcal{M})$ by COMPUTEINFER's last side condition. Otherwise, $\iota \in [T] \cup \bigcup_{i=0}^{k} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. In both cases, $\iota \in [T] \cup \bigcup_{i=0}^{k+1} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$.

CASE DELETEORPHANS: Consider the transition $(T_k, \mathcal{N}_k) = (T \cup T', \mathcal{N}) \implies_{\text{LGC}} (T, \mathcal{N}) = (T_{k+1}, \mathcal{N}_{k+1})$. We assume $\iota \in \text{FLInf}(\mathcal{N}_{\downarrow\text{active}})$ for some $\iota$. By the induction hypothesis, $\iota \in [T \cup T'] \cup \bigcup_{i=0}^{k+1} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. Since $\iota \notin [T']$ by DELETEORPHANS's side condition, we have $\iota \in [T] \cup \bigcup_{i=0}^{k+1} \text{Red}_{1}^{\cap \text{G}_L}(\mathcal{N}_i)$. $\square$

**Lemma 78** Let $(T_i, \mathcal{N}_i)_i$ be a nonempty $(\mathcal{P}(\text{FLinf}) \times \mathcal{P}(\text{FL}))$-sequence. If $\text{Inv}_{T, \mathcal{N}}(i)$ holds for all indices $i$, then $\text{Inv}_{T, \mathcal{N}}(\infty)$ holds.
**Proof** We assume $ι ∈ FLInf(\mathcal{N}_{∞}↓_{active})$ for some $ι$ and show $ι ∈ [T_∞] ∪ ∪_i Red_1^{∩G_L}(\mathcal{N}_i)$. Assume $ι ∉ [T_∞]$. Clearly, there must exist an index $k$ such that $\mathcal{N}_{k↓_{active}}$ contains all of $ι$'s premises and $ι ∉ [T_k]$. Therefore $ι ∈ FLInf(\mathcal{N}_{k↓_{active}})$. Since $Inv_{T,\mathcal{N}}(k)$ holds, $ι ∈ ∪_{i=0}^k Red_1^{∩G_L}(\mathcal{N}_i) ⊆ ∪_i Red_1^{∩G_L}(\mathcal{N}_i)$. □

**Lemma 79** Let $(T_i, \mathcal{N}_i)_i$ be an $⇒_{LGC}$-derivation. If $\mathcal{N}_{0↓_{active}} = \emptyset$, $\mathcal{N}_{∞↓_l} = \emptyset$ for all $l \neq$ active, $T_0 \supseteq FInf(\emptyset)$, and $T_∞ = \emptyset$, then $(\mathcal{N}_i)_i$ is fair.

**Proof** By Lemmas 67 and 68, $FLInf(\mathcal{N}_{0↓_{active}}) ⊆ [T_∞] ∪ ∪_i Red_1^{∩G_L}(\mathcal{N}_i)$. By the second and fourth hypotheses, this inclusion simplifies to $FLInf(\mathcal{N}_{∞}) ⊆ ∪_i Red_1^{∩G_L}(\mathcal{N}_i)$. □

**Theorem 80** Let $(T_i, \mathcal{N}_i)_i$ be an $⇒_{LGC}$-derivation, where $\mathcal{N}_{0↓_{active}} = \emptyset$, $\mathcal{N}_{∞↓_l} = \emptyset$ for all $l \neq$ active, $T_0 \supseteq FInf(\emptyset)$, and $T_∞ = \emptyset$. If $[\mathcal{N}_0] = ∩_G \{⊥\}$ for some $⊥ ∈ F_⊥$, then some $\mathcal{N}_i$ contains $(⊥', l)$ for some $⊥' ∈ F_⊥$ and $l ∈ L$.

**Proof** By Lemma 61, $[\mathcal{N}_0] = ∩_G \{⊥\}$ is equivalent to $\mathcal{N}_0 = ∩_{G_L} \{(⊥, \text{active})\}$. By Lemmas 76 and 79, we know that $(\mathcal{N}_i)_i$ is a fair $▷_{Red∩G_L, ⊢}^-$-derivation. Since $(FLInf, Red^{∩G_L, ⊢})$ is dynamically refutationally complete, we can conclude that some $\mathcal{N}_i$ contains $(⊥', l)$ for some $⊥' ∈ F_⊥$ and $l ∈ L$. □

**Example 81** The following DISCOUNT loop [1] prover DL is an instance of the lazy given clause prover LGC. This loop design is inspired by Schulz's description of E [39] but omits E's presimplification of $concl(ι)$. The prover's state is a four-tuple $T | P | Y | A$, where $T$ is a set of inferences and $P, Y, A$ are sets of formulas. The $T, P$, and $A$ sets correspond to the scheduled inferences, the passive formulas, and the active formulas, respectively. The $Y$ set is a subsingleton that can store a chosen passive formula. Initial states have the form $T | P | ∅ | ∅$, where $T$ is the set of all premise-free inferences of $Finf$.

COMPUTEINFER $T ⊎ \{ι\} | P | ∅ | A \implies_{DL} T | P | \{C\} | A$ if $ι ∈ Red_1^{∩G}(A ∪ \{C\})$

CHOOSEP $T | P ⊎ \{C\} | ∅ | A \implies_{DL} T | P | \{C\} | A$

DELETEFWD $T | P | \{C\} | A \implies_{DL} T | P | ∅ | A$ if $C ∈ Red_F^{∩G}(A)$ or $C \succ C'$ for some $C' ∈ A$

SIMPLIFYFWD $T | P | \{C\} | A \implies_{DL} T | P | \{C'\} | A$ if $C ∈ Red_F^{∩G}(A ∪ \{C'\})$

DELETEBWD $T | P | \{C\} | A ⊎ \{C'\} \implies_{DL} T | P | \{C\} | A$ if $C' ∈ Red_F^{∩G}(\{C\})$ or $C' \prec C$

SIMPLIFYBWD $T | P | \{C\} | A ⊎ \{C'\} \implies_{DL} T | P ∪ \{C''\} | \{C\} | A$ if $C' ∈ Red_F^{∩G}(\{C, C''\})$

SCHEDULEINFER $T | P | \{C\} | A \implies_{DL} T ∪ T' | P | ∅ | A ∪ \{C\}$ if $T' = FInf(A, \{C\})$

DELETEORPHANS $T ⊎ T' | P | Y | A \implies_{DL} T | P | Y | A$ if $T' ∩ FInf(A) = \emptyset$

A reasonable strategy for applying the DL rules is presented below. It relies on a well-founded ordering $▷$ on formulas to make sure that the simplification rules actually simplify their target in some sense, preventing infinite looping. It assumes that $Finf(N, \{C\})$ is finite whenever $N$ is finite.
1. Repeat while $T \cup P \neq \emptyset$ and $\perp \notin Y \cup A$:

1.1. Apply COMPUTEINFER or CHOOSEP to retrieve the next conclusion of an inference from T or the next formula from P, where T and P are organized as a single priority queue, to ensure fairness.

1.2. Apply SIMPLIFYFWD as long as the simplified formula $C'$ is ≻-smaller than the original formula C.

1.3. If DELETEFWD is applicable, apply it.

1.4. Otherwise:

1.4.1. Apply DELETEBWD exhaustively.

1.4.2. Apply SIMPLIFYBWD as long as the simplified formula $C''$ is ≻-smaller than the original formula $C'$.

1.4.3. Apply DELETEORPHANS.

1.4.4. Apply SCHEDULEINFER.

The instantiation of LGC relies on three labels $l_3 \sqsupseteq l_2 \sqsupseteq l_1$ = active corresponding to the sets P, Y, A, respectively.

**Example 82** Higher-order unification can give rise to infinitely many incomparable unifiers. As a result, in $\lambda$-superposition [13], performing all inferences between two clauses can lead to infinitely many conclusions, which need to be enumerated fairly. The Zipperposition prover [13], which implements the calculus, performs this enumeration in an extended DISCOUNT loop.

Infinitary inference rules are also useful to reason about the theory of datatypes and codatatypes. Superposition with (co)datatypes [19] includes $n$-ary ACYCL and UNIQ rules, which had to be restricted and complemented with axioms so that they could be implemented in Vampire [27]. In Zipperposition, it would be possible to support the rules in full generality, eliminating the need for the axioms.

Abstractly, a Zipperposition loop prover ZL operates on states $T \mid P \mid Y \mid A$, where T is organized as a finite set of possibly infinite sequences $(\iota_i)_i$ of inferences and the other components are as in DL (Example 81). The CHOOSEP, DELETEFWD, SIMPLIFYFWD, DELETEBWD, and SIMPLIFYBWD rules are essentially as in DL. The other rules follow:

$$ \text{COMPUTEINFER} \quad T \uplus \{(\iota_i)_i \mid P \mid \emptyset \mid A \implies_{\text{ZL}} T \cup \{(\iota_i)_{i \ge 1}\} \mid P \cup \{C\} \mid \emptyset \mid A \} \\ \text{if } \iota_0 \in \text{Red}_1^{\cap} (A \cup \{C\}) $$

$$ \text{SCHEDULEINFER} \quad T \mid P \mid \{C\} \mid A \implies_{\text{ZL}} T \cup T' \mid P \mid \emptyset \mid A \cup \{C\} \\ \text{if } T' \text{ is a finite set of sequences } (\iota_i^j)_i \text{ of inferences such that the set of} \\ \text{all } \iota_i^j \text{ equals } \text{Finf}(A, \{C\}) $$

$$ \text{DELETEORPHAN} \quad T \uplus \{(\iota_i)_i \mid P \mid Y \mid A \implies_{\text{ZL}} T \mid P \mid Y \mid A \} \\ \text{if } \iota_i \notin \text{Finf}(A) \text{ for all } i $$

COMPUTEINFER works on the first element of sequences. SCHEDULEINFER adds new sequences to T. Typically, these sequences store $Finf(A, \{C\})$, which may be countably infinite, in such a way that all inferences in one sequence have identical premises and can be removed together by DELETEORPHAN. The same rule can also be used to remove empty sequences from T, since the side condition is then vacuously true, thereby providing a form of garbage collection.

A subtle difference with DL is that COMPUTEINFER puts the formula C in P instead of Y. This gives more flexibility for scheduling; for example, a prover can pick several
formulas from the same sequence and then choose the most suitable one—not necessarily
the first one—to move to the active set.

To produce fair derivations, a prover needs to choose the sequence in COMPUTEINFER fairly and to choose the formula in CHOOSEP fairly. In combination, this achieves a form of dovetailing. The prover could use a simple algorithm, such as round-robin, for COMPUTE-INFER and employ more sophisticated heuristics for CHOOSEP.

The implementation in Zipperposition uses a slightly more complicated representation for *T*, with sequences of subsingletons of inferences. Thus, each sequence element is either a single inference *ι* or the empty set, which signifies that no new unifier was found up to a certain depth.

**Remark 83** The above approach to orphan formula deletion works because formulas recognized as orphans, belonging to the *T* state component, cannot have been used to make other formulas or inferences redundant—only passive and active formulas are considered by the redundancy criterion. If formulas from the *P* or *A* set could be detected as orphans, we could lose refutational completeness. To see this, consider the abstract scenario in which a formula *C* that is crucial for a refutation is subsumed by *D*, which is in turn deleted for being an orphan formula. Then *C* is lost forever even if is not an orphan formula.

Nevertheless, the idea of detecting orphan formulas outside the scheduled inferences in *T* can be salvaged as follows: Annotate each formula *D* with its parentage, and whenever *D* is used to simplify other clauses or to make other inferences redundant, remember this fact. Only consider *D* an orphan formula if it has lost a parent and if it has never been used to delete other formulas or to make other inferences redundant.

**4.3 Integrating Saturation Calculi**

The prover architectures described above can be instantiated with saturation calculi that use a redundancy criterion obtained as an intersection of lifted redundancy criteria. Some saturation calculi are defined in such a way that this requirement is trivially satisfied. For others, some reformulation of the redundancy criterion may be necessary.

**Example 84** As explained in Examples 54 and 55, redundancy criteria for calculi with selection functions [5,6] or constraints [29,30] can be defined as intersections $Red^G$ of lifted redundancy criteria.

**Example 85** In Bachmair and Ganzinger's associative-commutative (AC) superposition calculus [4], the redundancy of general clauses and inferences is defined using a ground-ing function *G* that maps every clause *C* to the set of its ground instances *C*θ and every inference *ι* to the set of its ground instances *ι*θ. ("Instance" means "syntactic instance" here, that is, not "instance modulo AC.") In principle, one could now apply (*G*, ⊢)-lifting, where we choose ⊢ as the instantiation ordering modulo AC. This would be pointless, though, since in the definition of $Red_F^{G, ⊢}$ the ordering ⊢ is used only if *D* is a common syntactic instance of *C* and *C'*. Note that, for example, $C = f(c + (c+z)) \approx b$ is an AC-instance of $C' = f((x+x)+y) \approx b$, but since *C* and *C'* have no common syntactic ground instances, this fact is never exploited in $Red_F^{G, ⊢}$. We can repair this by redefining *G* so that it maps every *ι* to the set of its syntactic ground instances *ι*θ, as before, but *C* to the set of all *D* that are AC-equal to some ground instance $Cθ$. This qualifies as a grounding function as well, and since Bachmair and Ganzinger's definition of redundancy for ground clauses is invariant under AC, the new definition of redundancy for general clauses is equivalent to the old one.
**Example 86** Waldmann [44] considers a superposition calculus modulo Ψ-torsion-free cancellative abelian monoids. Redundant clauses and inferences are defined in the standard way by lifting, except for the ABSTRACTION inference rule: According to Waldmann’s definition, a ground instance of an ABSTRACTION inference $\iota = (C_2, C_1, C_0)$ is an ABSTRACTION inference $(C_2\theta, C_1\theta, C_0\theta)$ where $C_2\theta$ and $C_1\theta$ are ground. But the conclusion of an ABSTRACTION inference is never ground, and this applies also to $C_0\theta$. When defining redundancy for such inferences, it is therefore necessary to further instantiate the abstraction variable $\gamma$ in $C_0\theta$ using a substitution $\rho$ that maps $\gamma$ to a sufficiently small ground term. To obtain a grounding function $\mathcal{G}$ as defined in Section 3.1, we need to redefine $\mathcal{G}(\iota)$ as the set of all inferences $(C_2\theta, C_1\theta, C_0\theta\rho)$, rather than the set of all $(C_2\theta, C_1\theta, C_0\theta)$.

**Example 87** The definition of redundancy for Bachmair, Ganzinger, and Waldmann’s hierarchic superposition calculus [8] is mostly standard, using a grounding function that maps every clause $C$ to a subset $\mathcal{G}(C)$ of the set of its ground instances and every hierarchic superposition inference $\iota$ to a set $\mathcal{G}(\iota)$ of ground standard superposition inferences. There is one exception, namely, CLOSE inferences, which derive $\perp$ from a list of premises that is inconsistent w.r.t. some base (background) theory. For these inferences, $\mathcal{G}(\iota) = \text{undef}$.

Baumgartner and Waldmann’s variant of hierarchic superposition [10] uses a slightly different definition of redundancy: A clause $C$ is redundant if $\mathcal{G}(C) \subseteq \text{Red}_F(\mathcal{G}(N) \cup \text{Th}) \cup \text{Th}$; a non-CLOSE inference $\iota$ is redundant if $\mathcal{G}(\iota) \subseteq \text{Red}_1(\mathcal{G}(N) \cup \text{Th})$, where $\text{Th}$ is a fixed set of ground base clauses and $\text{Red}$ is the usual redundancy criterion for ground standard superposition. To convert this into the format required in Section 3.1, we can define $\text{Red}_F^{\text{Th}}(M) := \text{Red}_F(M \cup \text{Th}) \cup \text{Th}$, and $\text{Red}_1^{\text{Th}}(M) := \text{Red}_1(M \cup \text{Th})$. It is easy to check that $\text{Red}^{\text{Th}} := (\text{Red}_1^{\text{Th}}, \text{Red}_F^{\text{Th}})$ is also a redundancy criterion and that the properties above are equivalent to $\mathcal{G}(C) \subseteq \text{Red}_F^{\text{Th}}(\mathcal{G}(N))$ and $\mathcal{G}(\iota) \subseteq \text{Red}_1^{\text{Th}}(\mathcal{G}(N))$. For CLOSE inferences, we have again $\mathcal{G}(\iota) = \text{undef}$.

**Example 88** For saturation calculi whose refutational completeness proof is based on some kind of lifting of ground instances, the requirement to use a redundancy criterion obtained as an intersection of lifted redundancy criteria is rather natural. The outlier is unfailing completion [2].

Unfailing completion predates the introduction of Bachmair–Ganzinger-style redundancy, but it can be incorporated into that framework. The formulas are the rewrite rules and equations. The only inferences are orientation and critical pair computation; the other inferences of the unfailing completion calculus (e.g., simplifications of equations or rules) must be considered as simplifications in our framework, rather than as inferences. With these definitions, formulas and inferences are redundant if for every rewrite proof using that rewrite rule, equation, or critical peak, there exists a smaller rewrite proof.<fnref n="5" />

The requirement that the redundancy criterion must be obtained by lifting (which is necessary to introduce the labeling) can then be trivially fulfilled by “self-lifting”—i.e., by defining $\mathbf{G} := \mathbf{F}$ and $\succ := \emptyset$ and by taking $\mathcal{G}$ as the function that maps every formula or inference to the set of its $\alpha$-renamings.

Note that this definition of redundancy differs from the usual definition of redundancy for superposition. For example, with a term ordering satisfying $f(c) \succ f(b) \succ f(a) \succ c \succ b \succ a$, the equations $c \approx b$ and $c \approx a$ make $f(b) \approx f(a)$ redundant in the superposition calculus (since they are smaller in the induced clause ordering), but they do not make $f(b) \approx f(a)$ redundant in unfailing completion (since the rewrite proof $f(b) \leftrightarrow f(c) \leftrightarrow f(a)$ using $c \approx b$ and $c \approx a$ is larger than the rewrite proof $f(b) \leftrightarrow f(a)$ using $f(b) \approx f(a)$).

<footnote n="5">⁵ Proofs are compared using a proof ordering—that is, the multiset extension of an ordering that compares individual proof steps $s \to_R t$, $s \leftarrow_R t$, or $s \leftrightarrow_E t$.</footnote>
# 5 Isabelle Development

The framework described in the previous sections has been formalized in Isabelle/HOL [31, 32], including all the theorems and lemmas, the prover architectures GC and LGC, and the example prover RP. The Isabelle theory files are available in the *Archive of Formal Proofs* [16, 40]. The development is also part of the IsaFoL (Isabelle Formalization of Logic) [17] effort, which aims at developing a reusable computer-checked library of results about automated reasoning.

The main theory files of the development are listed below:

- Calculus.thy collects basic definitions and lemmas about consequence relations, inference systems, and redundancy criteria, including the equivalence of static and dynamic refutational completeness.

- Calculus_Variations.thy contains alternative notions of inferences, redundancy, saturation, and completeness found in the literature.

- Intersection_Calculus.thy introduces calculi equipped with a family of redundancy criteria, whose intersection is taken.

- Lifting_to_Non_Ground_Calculi.thy gathers the results on nonground liftings of calculi without and with well-founded orderings $\sqsubseteq_D$.

- Labeled_Lifting_to_Non_Ground_Calculi.thy contains the labeled extensions of the previous liftings.

- Given-Clause_Architectures.thy and Given-Clause_Architectures-Revisited.thy include results about the given clause prover GC and its extension LGC with delayed inferences. The invariant-based proofs presented in this paper are found in the latter theory file.

- FO_Ordered_Resolution_Prover-Revisited.thy re-proves the ordered resolution prover RP refutationally complete using our framework, providing a modular alternative to the Isabelle formalization by Schlichtkrull et al. [36, 38].

The development relies heavily on Isabelle's locales [9]. These are contexts that fix variables and make assumptions about these. Definitions and lemmas occurring inside the locale may then refer to them. With locales, the definitions and lemmas look similar to or even simpler than how they are stated on paper, but the proofs often become more complicated: Layers of locales may hide definitions, and often these need to be manually unfolded in several steps before the desired lemma can be proved. A pathological example is Lemma 64, which obviously holds by construction from a human perspective but whose Isabelle proof required more than a hundred lines of code.

We chose to represent basic nonempty sets such as $F$ and $L$ by types. This lightened the development in two ways. First, it relieved us from having to thread through nonemptiness conditions. Second, objects are automatically typed appropriately based on the context, meaning that lemmas could be stated without explicit hypotheses that given objects are formulas, labels, or indices. On the other hand, for sets such as $F_\perp$ and $F_\infty$ that are subsets of other sets, it was natural to use simply typed sets. Derivations, which describe the dynamic behavior of a calculus, are represented by the same lazy list codatatype [18] and auxiliary definitions that were used by Schlichtkrull et al.

The framework's design and its mechanization were carried out largely in parallel. This resulted in more work on the mechanization side because changes had to be propagated,
but it also helped detect missing conditions and shape the theory itself. For example, an
earlier version of the framework considered only single lifted redundancy criteria instead of
intersections of lifted redundancy criteria (Section 3.3); our first attempt at verifying RP in
Isabelle using the framework made it clear that the theory was not quite general enough yet
to support selection functions (Example 54).

6 Conclusion

We presented a formal framework for saturation theorem proving inspired by Bachmair
and Ganzinger's *Handbook* chapter [6]. Users can conveniently derive a dynamic refuta-
tional completeness result for a concrete prover based on a statically refutationally com-
plete calculus. The key was to strengthen the standard redundancy criterion so that all
prover operations, including subsumption deletion, can be justified by inference or redun-
dancy. The framework is mechanized in Isabelle/HOL and can be used to verify actual
provers.

To employ the framework, users must provide a statically complete saturation calculus expressible as the lifting ($Finf, Red^G$) or ($Finf, Red^{\neg G}$) of a ground calculus ($GInf, Red$), where Red qualifies as a redundancy criterion and $G$ qualifies as a grounding function or grounding function family. The framework can be used to derive two main results:

1. After defining a well-founded ordering $\leq$ or a family of well-founded orderings that capture instantiation, invoke Theorem 53 to show ($Finf, Red^{\neg G, \leq}$) dynamically complete.

2. Based on the previous step, invoke Theorem 70 or 80 to derive the dynamic completeness of a prover architecture building on the given clause procedure, such as the Otter, iProver, DISCOUNT, or Zipperposition loop (Example 71, 74, 81, or 82).

The framework can also help establish the static completeness of the nonground calculus.
For many calculi (with the notable exceptions of constraint and hierarchic superposition),
Theorem 32 or 50 can be used to lift the static completeness of ($GInf, Red$) to ($Finf, Red^G$)
or ($Finf, Red^{\neg G}$).

The main missing piece of the framework is a generic treatment of clause splitting.
Until recently, the only formal treatment of splitting, by Fietzke and Weidenbach [22], hard-
codes both the underlying calculus and the splitting strategy. Voronkov's AVATAR architec-
ture [42] is more flexible and yields truly impressive empirical results, but he and his collab-
orators left the question of AVATAR's refutational completeness open. Ebner, Blanchette,
and Tourret [21] recently provided an answer by introducing and instantiating a generic
splitting framework based on our saturation framework.

**Acknowledgment** We thank Alexander Bentkamp for discussions about prover architectures for higher-order logic and for feedback from instantiating the framework, especially concerning Theorem 50. We thank Mathias Fleury and Christian Sternagel for their help with the Isabelle development. Finally, we thank Gabriel Ebner, Robert Lewis, Visa Nummelin, Dmitriy Traytel, and the anonymous reviewers for their comments and suggestions.

Blanchette's 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). He also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme and he has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).
References

1. Avenhaus, J., Denzinger, J., Fuchs, M.: DISCOUNT: A system for distributed equational deduction. In: J. Hsiang (ed.) RTA-95, LNCS, vol. 914, pp. 397–402. Springer (1995)

2. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: H. Aït-Kaci, M. Nivat (eds.) Rewriting Techniques—Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic Press (1989)

3. Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: M.E. Stickel (ed.) CADE-10, LNCS, vol. 449, pp. 427–441. Springer (1990). DOI 10.1007/3-540-52885-7_105

4. Bachmair, L., Ganzinger, H.: Associative-commutative superposition. In: N. Dershowitz, N. Lindenstrauss (eds.) CTRS-94, LNCS, vol. 968, pp. 1–14. Springer (1994)

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

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

7. Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a desion procedure for the monadic class with equality. In: G. Gottlob, A. Leitsch, D. Mundici (eds.) KGC ’93, LNCS, vol. 713, pp. 83–96. Springer (1993). DOI 10.1007/BFb0022557

8. Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)

9. Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014)

10. Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter (eds.) Description Logic, Theory Combination, and All That—Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, LNCS, vol. 11560, pp. 15–56. Springer (2019)

11. Benanav, D.: Simultaneous paramodulation. In: M.E. Stickel (ed.) CADE-10, LNCS, vol. 449, pp. 442–455. Springer (1990)

12. Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P.: Superposition for full higher-order logic. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS, vol. 12699, pp. 396–412. Springer (2021)

13. Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. 65(7), 893–940 (2021)

14. Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Log. Meth. Comput. Sci. 17(2), 1:1–1:38 (2021)

15. Bhayat, A.: Automated theorem proving in higher-order logic. Ph.D. thesis, University of Manchester (2021)

16. Blanchette, J., Tourret, S.: Extensions to the comprehensive framework for saturation theorem proving. Archive of Formal Proofs 2021 (2021). URL https://www.isa-afp.org/entries/Saturation_Framework_Extensions.html

17. Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In: A. Mahboubi, M.O. Myreen (eds.) CPP 2019, pp. 1–13. ACM (2019)

18. Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: G. Klein, R. Gamboa (eds.) ITP 2014, LNCS, vol. 8558, pp. 93–110. Springer (2014)

19. Blanchette, J.C., Peltier, N., Robillard, S.: Superposition with datatypes and codatatypes. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) IJCAR 2018, LNCS, vol. 10900, pp. 370–387. Springer (2018)

20. Duarte, A., Korovin, K.: Implementing superposition in iProver (system description). In: IJCAR (2), LNCS, vol. 12167, pp. 388–397. Springer (2020)

21. 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)

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

23. Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Information and Computation 199(1–2), 3–23 (2005)

24. Hillenbrand, T., Löchner, B.: The next WALDMEISTER loop. In: A. Voronkov (ed.) CADE-18, LNCS, vol. 2392, pp. 486–500. Springer (2002)

25. Huet, G.P.: A mechanization of type theory. In: N.J. Nilsson (ed.) IJCAI-73, pp. 139–146. William Kaufmann (1973)

26. Järvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: J. Esparza, R. Majumdar (eds.) TACAS 2010, LNCS, vol. 6015, pp. 129–144. Springer (2010)
27. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: N. Sharygina, H. Veith (eds.) CAV 2013, LNCS, vol. 8044, pp. 1–35. Springer (2013)

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

29. Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. J. Symb. Comput. **19**(4), 321–351 (1995)

30. Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. I, pp. 371–443. Elsevier and MIT Press (2001)

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

32. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)

33. Nummelin, V., Bentkamp, A., Tourret, S., Vukmirović, P.: Superposition with first-class Booleans and inprocessing clausification. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS, vol. 12699, pp. 378–395. Springer (2021)

34. Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs **2016** (2016). URL https://www.isa-afp.org/entries/SuperCalc.shtml

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

36. Schlichtkrull, A., Blanchette, J., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger’s ordered resolution prover. J. Autom. Reasoning **64**(7), 1169–1195 (2020)

37. 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)

38. Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of Bachmair and Ganzinger’s ordered resolution prover. Archive of Formal Proofs **2018** (2018). URL https://www.isa-afp.org/entries/Ordered_Resolution_Prover.html

39. Schulz, S.: E—a brainiac theorem prover. AI Commun. **15**(2–3), 111–126 (2002)

40. Tourret, S.: A comprehensive framework for saturation theorem proving. Archive of Formal Proofs **2020** (2020). URL https://www.isa-afp.org/entries/Saturation_Framework.shtml

41. Tourret, S., Blanchette, J.: A modular Isabelle framework for verifying saturation provers. In: C. Hriču, A. Popescu (eds.) CPP 2021, pp. 224–237. ACM (2021)

42. 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)

43. Vukmirović, P., Blanchette, J., Heule, M.J.: SAT-inspired eliminations for superposition. In: FMCAD 2021, pp. 231–240. IEEE (2021)

44. Waldmann, U.: Cancellative abelian monoids and related structures in refutational theorem proving (part I). J. Symb. Comput. **33**(6), 777–829 (2002)

45. 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)

46. 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)

Index

|=, 3

|=G, 14

|=q, 12

|=Gq, 20

|=q, 23

|=GLYPH<31>, 12

|=∩, 20

|=G, 20

≈, 4

⊥, 3

∴, 24

>, 19

≥, 19

→, 24

▷Red, 6

□ = (□D)D∈G, 16, 24

□, 24

(a$_{i}$)$_{i}$, 5

active, 25

C, D, 3

(C1)–(C4), 3

concl(t), 4

conclusion, 4

consequence relation, 3

▷-derivation, 6
DISCOUNT loop prover, 32

DL, 32

dynamically refutationally complete, 6

F, 3

F⊥, 3

fair, 6

FL, 23

FL⊥, 23

formulas, 3

G, 14

G, 14

G↓, 23

Gq, 20

Gq, 23

(G1)–(G3), 14

GC, 25

gen, 20

GInf, 14

GInfq, 20

given clause prover, 25

grounding function, 14

IL, 29

Inf, 4

Inf(N), 4

Inf(N, M), 4

inference, 4

inference system, 4

instantiation (quasi-)ordering, 19

intersections of liftings, 20

intersections of redundancy criteria, 12

Inv<sub>Σ</sub>, 26

Inv<sub>T,Σ</sub>, 31

iProver loop prover, 29

ι, 4

∠ι], 23

L, 23

(L1)–(L2), 23

label, 22

labeled version, 23

lazy given clause prover, 30

LGC, 30

liftable, 15

lifting, 13

G-lifting of ⊨=, 14

G-lifting of Red, 15

(G, ⊑)-lifting of Red, 17

limit, 6

N, M, 3

N∞, 6

N<sub>↓l</sub>, M<sub>↓l</sub>, 23

N<sub>↓l</sub>, M<sub>↓l</sub>, 25

N<sub>∞</sub>, 6

∠N], 23

O~S, 29

OL, 27

orphan formula, 30

Otter loop prover, 27

premise, 4

Q, 12

q, 12

(R1)–(R4), 4

Red = (Red<sub>I</sub>, Red<sub>F</sub>), 4

Red' = (Red'<sub>I</sub>, Red<sub>F</sub>), 9

Red<sup>G</sup> = (Red<sup>G</sup><sub>I</sub>, Red<sup>G</sup><sub>F</sub>), 15

Red<sup>G, ⊑</sup> = (Red<sup>G</sup><sub>I</sub>, Red<sup>G, ⊑</sup><sub>F</sub>), 17

Redq = (Red<sup>q</sup><sub>I</sub>, Red<sup>q</sup><sub>F</sub>), 12, 20

Red<sup>q, Gq, ∅</sup> = (Red<sup>q, Gq</sup><sub>I</sub>, Red<sup>q, Gq, ∅</sup><sub>F</sub>), 20

Red<sup>q, Gq, ⊑</sup> = (Red<sup>q, Gq</sup><sub>I</sub>, Red<sup>q, Gq, ⊑</sup><sub>F</sub>), 20

Red∩ = (Red<sub>I</sub>∩, Red<sub>F</sub>∩), 12

Red∩G, 20

Red∩G, ⊑, 20

Red∩G<sub>L</sub>, 24

reduced redundancy criterion, 8

reducedly refutationally complete, 8

redundancy criterion, 4

redundant, 4

RP, 29

saturated, 5

A-sequence, 5

standard redundancy criterion, 5

statically refutationally complete, 5

T, 30

T<sub>∞</sub>, 6

[T], 31

tiebreaker ordering, 16

trivial redundancy criterion, 5

undef, 14

Zipperposition loop prover, 33

ZL, 33