Polarized Resolution Modulo

Gilles Dowek

► To cite this version:

Gilles Dowek. Polarized Resolution Modulo. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. pp.182-196, 10.1007/978-3-642-15240-5_14. hal-01054460

HAL Id: hal-01054460

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

Submitted on 6 Aug 2014

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Polarized Resolution Modulo

Gilles Dowek

École polytechnique and INRIA
LIX, École polytechnique, 91128 Palaiseau Cedex, France.
gilles.dowek@polytechnique.edu, http://www.lix.polytechnique.fr/~dowek

**Abstract.** We present a restriction of Resolution modulo where the rewrite rules are such that clauses rewrite to clauses, so that the reduct of a clause needs not be further transformed into clause form. Restricting Resolution modulo in this way requires to extend it in another and distinguish the rules that apply to negative and positive atomic propositions. This method can be seen as a restriction of Equational resolution that mixes clause selection and literal selection restrictions. Unlike many restrictions of Resolution, it is not an instance of Ordered resolution.

## 1 Introduction

Deduction modulo is an extension of first-order predicate logic where axioms, for instance $P \Leftrightarrow (Q \Rightarrow R)$, are replaced by rewrite rules, for instance $P \rightarrow (Q \Rightarrow R)$. These rules define an equivalence relation and, in a proof, a proposition can be replaced by an equivalent one at any time.

A motivation for introducing Deduction modulo was its applications to automated theorem proving. Together with Thérèse Hardin and Claude Kirchner, we have defined a proof search method called *Extended Narrowing and Resolution*, or *Resolution modulo*, that extends first-order Resolution to handle such rewrite rules [8]. The term rewrite rules define an equivalence relation on terms that is used by the unification algorithm, but the proposition rewrite rules, such as $P \rightarrow (Q \Rightarrow R)$, are used, in a different way, to directly rewrite, or more generally narrow, the clauses. For instance, with the rewrite rule above, the clause $P,S$ narrows to $Q \Rightarrow R,S$.

The proof-search method obtained this way is complete provided the theory defined by the rewrite rules has the cut elimination property. Moreover this completeness theorem has a converse: if Resolution modulo is complete, then the theory has the cut elimination property [9]. More generally, whether the theory has the cut elimination property or not, the method proves exactly the propositions that have a cut free proof.

Resolution modulo is more efficient than Resolution used with axioms. For instance, a naive search for a Resolution proof of a contradiction with the axiom $\forall x (P(x) \Leftrightarrow P(f(x)))$ generates an infinite search space. But attempting to prove a contradiction with Resolution modulo the rule $P(x) \rightarrow P(f(x))$ generates an empty search space. Besides this trivial example, Simple type theory can be expressed in Deduction modulo and applying Resolution modulo to this theory
yields a step by step simulation of Higher-order resolution [1, 10], that generates
an empty search space when attempting to prove a contradiction in this theory.

Yet, a problem with Resolution modulo is that narrowing the clause *P*,*S*
yields the set of propositions *Q* ⇒ *R*,*S* that is not a clause, and this set needs
to be further transformed into clause form: ¬*Q*,*R*,*S*. In the general case, this
transformation includes skolemization. For instance, with the rule *P(x)* −→
∀*y* *Q(x,y)*, the clause *P(X), S* narrows to *Q(X, Y), S* but the clause ¬*P(X), S*
narrows to ¬*Q(X, f(X))*, *S* where *f* is a new Skolem symbol. This dynamic
skolemization is an unpleasant feature of Resolution modulo that is cumbersome
to implement and that complicates the completeness proof.

To address this problem, we restrict, in this paper, Resolution modulo to
clausal rewrite systems, defined in such a way that a clause always narrows
to a clause. However, restricting Resolution modulo this way requires to extend
it in another. Indeed, the rule P —> (Q => R) must be replaced by the rule
P —> (¬Q ∨ R) when applied to the literal P, but it must be replaced by
the rules P —> ¬Q and P —> ¬¬R when applied to the literal ¬P. Thus,
negative and positive occurrences of atomic propositions must be rewritten in a
different way, like in the so-called Polarized deduction modulo [5], hence the name
Polarized resolution modulo for the method. Like Resolution modulo, Polarized
resolution modulo proves a proposition if and only if this proposition has a cut
free proof. Thus, it is complete if and only if the theory defined by the rewrite
rules has the cut elimination property.

Another advantage of Polarized resolution modulo over the original formu-
lation is that the **Extended Narrowing** rule can be seen as a particular case
of the **Resolution** rule with extra clauses added to the problem. Indeed, in-
stead of using the rewrite rule *P* → (¬*Q* ∨ *R*) to transform the clause *P*,*S* into
¬*Q*,*R*,*S*, we may as well add an extra clause ¬*P*,¬*Q*,*R* and derive ¬*Q*,*R*,*S*
with the **Resolution** rule from *P*,*S* and this new clause. However, the use of
this new clause is restricted in such a way that the resolved literal in this clause
must always be ¬*P*. We shall call such a literal *selected* and a clause with an
selected literal a *one-way* clause. A further restriction is that the **Resolution**
rule cannot be applied to two one-way clauses.

Thus, Polarized resolution modulo appears to be a restriction of Equational
resolution, that combines two types of restrictions used in resolution based proof
methods: clause selection restrictions like in the *Set of support* method [14] and
in *Semantic resolution* [13] and literal selection restrictions like in *Ordered res-
olution* [2], preserving completeness, provided the theory defined by the rewrite
rules has the cut elimination property. Yet, it is more restricted than each of
these methods. In particular, together with Guillaume Burel [4], we have proved
that, unlike many other restrictions of Resolution, it is not an instance of Or-
dered Resolution. Indeed, Polarized resolution modulo fails in finite time when
attempting to prove a contradiction in Simple type theory. Thus, its complete-
ness implies the consistency of Simple type theory, and, from Gödel’s second
incompleteness theorem, the completeness of this method cannot be proved in
Simple type theory, while the completeness of all instances of Ordered resolution can.

This also simplifies the implementation of the method and unlike Resolution modulo, that has never been fully implemented, there is an implementation of Polarized resolution modulo, that gives very promising first results [3], in particular for Simple type theory.

# 2 Polarized deduction modulo

## 2.1 Polarized deduction modulo

**Definition 1 (Polarized rewrite system).** A polarized rewrite system is a triple $\mathcal{R} = \langle \mathcal{E}, \mathcal{R}_-, \mathcal{R}_+ \rangle$ where $\mathcal{E}$ is a set of equations between terms, $\mathcal{R}_-$ and $\mathcal{R}_+$ are sets of rewrite rules whose left hand sides are atomic propositions and right hand sides are arbitrary propositions. The rules of $\mathcal{R}_-$ are called negative rules and those of $\mathcal{R}_+$ are called positive rules.

**Definition 2 (Polarized rewriting).** Let $\mathcal{R} = \langle \mathcal{E}, \mathcal{R}_-, \mathcal{R}_+ \rangle$ be a polarized rewrite system. We define the equivalence relation $\cong_\mathcal{E}$ as the congruence on terms generated by the equations of $\mathcal{E}$. We then define the one step negative and positive rewriting relations $\to_-$ and $\to_+$ as follows.

- If $t_i \stackrel{\mathcal{E}}{=} u$ then both $P(t_1, \dots, t_i, \dots, t_n) \to_- P(t_1, \dots, u, \dots, t_n)$ and $P(t_1, \dots, t_i, \dots, t_n) \to_+ P(t_1, \dots, u, \dots, t_n)$.

- If $P \to A$ is a rule of $\mathcal{R}_s$ and $\sigma$ is a substitution then $\sigma P \to_s \sigma A$, where $s$ is either $-$ or $+$.

- If $A \stackrel{s}{\to} A'$ then $\neg A \stackrel{s}{\to} \neg A'$, where $\stackrel{s}{\to}$ swaps $-$ and $+$.

- If $(A \to_s A'$ and $B = B'$) or $(A = A'$ and $B \to_s B'$), then $A \wedge B \to_s A' \wedge B'$ and $A \vee B \to_s A' \vee B'$.

- If $(A \to_s A'$ and $B = B'$) or $(A = A'$ and $B \to_s B'$), then $A \Rightarrow B \to_s A' \Rightarrow B'$.

- If $A \to_s A'$ then $\forall x A \to_s \forall x A'$ and $\exists x A \to_s \exists x A'$.

We define the sequent one step term rewriting relation $\to$ as follows.

- If $A \to_- A'$ then $(\Gamma, A \vdash \Delta) \to (\Gamma, A' \vdash \Delta)$.

- If $A \to_+ A'$ then $(\Gamma \vdash A, \Delta) \to (\Gamma \vdash A', \Delta)$.

As usual, if $\mathcal{R}$ is any binary relation, we write $\mathcal{R}^*$ for its reflexive-transitive closure. The rules of *Polarized sequent calculus modulo* are those of Figure 1. Proof checking is decidable when the relations $\to_-^*$ and $\to_+^*$ are. The usual, non polarized, Deduction modulo can be recovered by taking $\mathcal{R}_- = \mathcal{R}_+$ and predicate logic by taking $\mathcal{E} = \mathcal{R}_- = \mathcal{R}_+ = \emptyset$.

The following propositions are proved by induction over proof structure.

**Proposition 1.** If $(\Gamma \vdash \Delta) \stackrel{*}{\to} (\Gamma' \vdash \Delta')$ and $\Gamma' \vdash \Delta'$ has a cut free proof modulo $\mathcal{R}$ then $\Gamma \vdash \Delta$ has a cut free proof modulo $\mathcal{R}$ of the same size.
<figure><img src="image_2.png" /><figcaption>Fig. 1. Polarized sequent calculus modulo</figcaption></figure>
**Proposition 2.** Assume that the language contains a closed term and that $Γ \vdash \Delta$ is a closed sequent. Then, if $Γ \vdash \Delta$ has a cut free proof using neither the left rule of the existential quantifier, nor the right rule of the universal quantifier, it has a cut free proof where all the sequents are closed.

## 2.2 Compatibility

We want to show that rewrite rules build in axioms, i.e. that for each rewrite system $\mathcal{R}$, there is a set of axioms $\mathcal{T}$ such that $Γ \vdash \Delta$ is provable modulo $\mathcal{R}$ if and only if there exists a finite subset $\mathcal{T}'$ of $\mathcal{T}$ such that $Γ, \mathcal{T}' \vdash \Delta$ is provable in predicate logic. As we sometimes want to transform some, but not all, rewrite rules into axioms, we shall transform the rewrite system $\mathcal{R}$ into a pair formed with a weaker rewrite system $\mathcal{R}'$ and a set of axioms $\mathcal{T}$.

**Definition 3 (Compatibility).** Let $\mathcal{R}$ and $\mathcal{R}'$ be polarized rewrite systems and $\mathcal{T}$ be a set of axioms. The system $\mathcal{R}$ is compatible with the pair $\langle \mathcal{R}', \mathcal{T} \rangle$ when

1. if $A \dashv\dashv_B^* B$ in $\mathcal{R}'$ then $A \dashv\dashv_B^* B$ in $\mathcal{R}$ and if $A \dashv\dashv_B^* B$ in $\mathcal{R}'$ then $A \dashv\dashv_B^* B$ in $\mathcal{R}$,

2. if $A \in \mathcal{T}$, then $\vdash A$ is provable modulo $\mathcal{R}$,

3. if $A \dashv\dashv_B^* B$ in $\mathcal{R}$, then there exists a finite subset $\mathcal{T}'$ of $\mathcal{T}$ such that $\mathcal{T}' \vdash A \Rightarrow B$ is provable modulo $\mathcal{R}'$,

4. if $A \dashv\dashv_B^* B$ in $\mathcal{R}$, then there exists a finite subset $\mathcal{T}'$ of $\mathcal{T}$ such that $\mathcal{T}' \vdash B \Rightarrow A$ is provable modulo $\mathcal{R}'$.

**Proposition 3 (Equivalence).** Let $\mathcal{R}$ be a polarized rewrite system and $\langle \mathcal{R}', \mathcal{T} \rangle$ be a pair compatible with $\mathcal{R}$, then the sequent $Γ \vdash \Delta$ is provable modulo $\mathcal{R}$, if and only if there exists a finite subset $\mathcal{T}'$ of $\mathcal{T}$ such that the sequent $Γ, \mathcal{T}' \vdash \Delta$ is provable modulo $\mathcal{R}'$.

*Proof.* If $Γ, \mathcal{T}' \vdash \Delta$ is provable modulo $\mathcal{R}'$, it is provable modulo $\mathcal{R}$ and each $A$ of $\mathcal{T}'$ is provable modulo $\mathcal{R}$. We conclude with the cut rule. The converse is a simple induction over proof structure.

Two particular cases are useful: $\mathcal{R}' = \emptyset$ i.e. all the rewrite rules are transformed into axioms, and $\mathcal{R}' = \mathcal{E}$, i.e. only proposition rewrite rules are transformed into axioms.

**Proposition 4.** For all polarized rewrite systems $\mathcal{R}$, there exists a set of axioms $\mathcal{T}$ such that $\mathcal{R}$ and $\langle \emptyset, \mathcal{T} \rangle$ are compatible.

*Proof.* Take the universal closures of all the propositions $A \Rightarrow B$ such that $A \dashv\dashv_B^* B$ or $B \dashv\dashv_A^* A$.

**Proposition 5.** For all polarized rewrite systems $\mathcal{R} = \langle \mathcal{E}, \mathcal{R}_-, \mathcal{R}_+ \rangle$, there exists a set of axioms $\mathcal{T}$ such that $\mathcal{R}$ and $\langle \mathcal{E}, \mathcal{T} \rangle$ are compatible.

*Proof.* Take for each rule $P \dashv\dashv_A^* A$ of $\mathcal{R}_-$ the universal closure of $P \Rightarrow A$ and for each rule $P \dashv\dashv_A^* A$ of $\mathcal{R}_+$ the universal closure of $A \Rightarrow P$.
## 2.3 Clausal rewrite systems

**Definition 4 (Literal, Clausal proposition).** A proposition is a literal if it is either atomic or the negation of an atomic proposition. A proposition is clausal if it is $\perp$ or of the form $\forall x_1 \dots \forall x_p (L_1 \vee \dots \vee L_n)$ where $L_1, \dots, L_n$ are literals and $x_1, \dots, x_p$ variables.

**Definition 5 (Clausal rewrite system).** A rewrite system is clausal if negative rules rewrite atomic propositions to clausal propositions and positive rules atomic propositions to negations of clausal propositions.

For instance, the rewrite system $\mathcal{R}$ formed with the negative rule $P \longrightarrow (\neg Q \vee R)$ and the positive rules $P \longrightarrow \neg Q$ and $P \longrightarrow \neg\neg R$ is clausal. This rewrite system is compatible with the axiom $P \Leftrightarrow (Q \Rightarrow R)$, in the same way the rule $P \longrightarrow (Q \Rightarrow R)$ is in usual Deduction modulo.

**Example 1.** A presentation of Simple type theory in Deduction modulo has been given in [7]. To adapt it to Polarized deduction modulo, we just need to duplicate each rule, but this polarized rewrite system is not clausal. An equivalent one, that is clausal has been given in [6]. The sorts of this system are simple types built from two base types $\iota$ and $o$. The language contains

- for each pair of sorts, a constant $K_{T,U}$ of sort $T \to U \to T$,

- for each triple of sorts, a constant $S_{T,U,V}$ of sort $(T \to U \to V) \to (T \to U) \to T \to V$,

- a constant $\dot{\vee}$ of sort $o \to o \to o$,

- a constant $\dot{\lhd}$ of sort $o \to o$,

- for each sort, a constant $\dot{\nabla}_T$ of sort $(T \to o) \to o$,

- for each pair of sorts, a function symbol $\alpha_{T,U}$ of rank $\langle T \to U, T, U \rangle$,

- for each sort $T$, a Skolem symbol $H_T$ of sort $(T \to o) \to T$,

- a predicate symbol $\varepsilon$ of rank $\langle o \rangle$.

As usual, we write $(t u)$ for $\alpha_{T,U}(t, u)$ and $(t u_1 \dots u_n)$ for $(\dots (t u_1) \dots u_n)$. The rewrite rules are

$$ (K_{T,U} \ x \ y) = \varepsilon \ x $$

$$ (S_{T,U,V} \ x \ y \ z) = \varepsilon \ (x \ z \ (y \ z)) $$

$$ \varepsilon(x \ \dot{\vee} \ y) \longrightarrow_{-} (\varepsilon(x) \vee \varepsilon(y)) \quad \varepsilon(x \ \dot{\vee} \ y) \longrightarrow_{+} \neg\neg\varepsilon(x) $$

$$ \varepsilon(x \ \dot{\vee} \ y) \longrightarrow_{+} \neg\neg\varepsilon(y) $$

$$ \varepsilon(\dot{\lhd} \ x) \longrightarrow_{-} \neg\varepsilon(x) \quad \varepsilon(\dot{\lhd} \ x) \longrightarrow_{+} \neg\varepsilon(x) $$

$$ \varepsilon(\forall_T \ x) \longrightarrow_{-} \forall y \ \varepsilon(x \ y) \quad \varepsilon(\dot{\nabla}_T \ x) \longrightarrow_{+} \neg\neg\varepsilon(x \ H_T(x)) $$

This theory does not have the cut elimination property as the sequent $\varepsilon(x H_T(x)) \vdash \forall y \ \varepsilon(x \ y)$ has a proof with a cut (on $\varepsilon(\dot{\nabla}_T \ x)$) but no cut free proofs. Yet, as proved in [6], for sequents not containing the symbols $H_T$, cut free provability in this theory characterizes exactly provability in Simple type theory.

The fact that there is an infinite number of objects of type $\iota$ can be expressed by the rules

$$ (Pred \ (Succ \ x)) = \varepsilon \ x $$
$$ 
\begin{aligned}
\varepsilon(\mathit{Null} \ 0) &\longrightarrow_+ \neg \bot \\
\varepsilon(\mathit{Null} \ (\mathit{Succ} \ x)) &\longrightarrow_- \bot
\end{aligned}
$$

The first expresses that the function *Succ* of type $\iota \to \iota$ has a left inverse *Pred*, i.e. that it is injective. The two others that 0 is not in its image, i.e. that it is not surjective.

### 3 Polarized resolution modulo

**Definition 6 (Clause, Constraint, Unifier, Constrained clause).** A clause is a finite set of literals. A constraint is a pair of terms or of atomic propositions, written $t = u$. A unifier of a constraint $t = u$ is a substitution $\theta$ such that $\theta t = \varepsilon \theta u$. A constrained clause is a pair $U[C]$ such that $U$ is a clause and $C$ is a finite set of constraints.

The empty clause is written $\square$. If $U$ is a clause and $L$ is a literal, we write $U, L$ for the clause $U \cup \{L\}$. If $A = \forall x_1 \dots \forall x_p (L_1 \lor \dots \lor L_n)$ is a clausal proposition, we write $|A|$ for the clause $\{L_1, \dots, L_n\}$. By convention, $|\bot| = \square$. If $\psi$ is a constrained clause and $\Phi$ a set of constrained clauses, a $\Phi$-renaming of $\psi$ is a renaming of $\psi$ with variables that do not occur in $\Phi$.

**Definition 7 (One-way clause, Selected literal).** To each polarized rewrite system, we associate a set of clauses called the one-way clauses of $\mathcal{R}$. These clauses have a privileged literal called the selected literal. For each negative rule $P \longrightarrow \forall x_1 \dots \forall x_p (L_1 \lor \dots \lor L_n)$, we take the clause $\neg P, L_1, \dots, L_n$ and, for each positive rule $P \longrightarrow \neg \forall x_1 \dots \forall x_p (L_1 \lor \dots \lor L_n)$, we take the clause $\underline{P}, L_1, \dots, L_n$ where the selected literal is the underlined one.

**Definition 8 (Polarized resolution modulo).** Let $\Phi$ be a set of constrained clauses, we write $\Phi \mapsto_R \psi$ if the constrained clause $\psi$ can be derived from the constrained clauses of $\Phi$ using finitely many applications of the Resolution and Extended Narrowing rules described in Figure 2. This means that there exists a derivation of the clause $\psi$ under the assumptions $\Phi$, i.e. a sequence $\psi_1, \dots, \psi_n$ such that either $n = 0$ and $\psi$ is an element of $\Phi$ or $n \ge 1$, $\psi_n = \psi$ and each $\psi_i$ is derived with a rule of Figure 2 from renamings of clauses of the set $\Phi \cup \{\psi_1, \dots, \psi_{i-1}\}$.

When $\mathcal{R}_- = \mathcal{R}_+ = \emptyset$, Polarized resolution modulo boils down to Plotkin's Equational resolution [12, 11]: the Extended Narrowing rule never applies, and the only difference with first-order Resolution is that unification is replaced by equational unification modulo $\mathcal{E}$.

As discussed in the introduction, the Extended Narrowing rule can be seen as an instance of the Resolution rule where, from an ordinary clause $(U, P)[C]$ and a one-way clause $V, \neg Q$, we derive the clause $(U \cup V)[C \cup \{P = Q\}]$. Thus instead of having the Extended Narrowing rule, we could add the one-way clauses to the set of clauses to be refuted and restrict Equational resolution in
$$ \frac{(U, P_1, \dots, P_n)[C_1] \quad (V, \neg Q_1, \dots, \neg Q_p)[C_2]}{(U \cup V)[C_1 \cup C_2 \cup \{P_1 = \dots = P_n = Q_1 = \dots = Q_p\}]} \quad \text{Resolution} $$

$$ \frac{(U, P)[C]}{(U \cup V)[C \cup \{P = Q\}]} \quad \text{if } V, \neg Q \text{ one-way clause of } \mathcal{R} \text{ Extended Narrowing} $$

$$ \frac{(U, \neg P)[C]}{(U \cup V)[C \cup \{P = Q\}]} \quad \text{if } V, Q \text{ one-way clause of } \mathcal{R} \text{ Extended Narrowing} $$

<caption>Fig. 2. Polarized resolution modulo</caption>

such a way that the **Resolution** rule cannot be applied to two one-way clauses and can be applied to a one-way clause and another clause only if the resolved literal in the one-way clause is the selected one. Yet, we prefer to distinguish this **Extended Narrowing** rule for better clarity.

*Example 2.* Using the rewrite system presented in Example 1, we get the one way clauses

$$ \begin{array}{l@{\qquad}l} \underline{\neg\varepsilon(x \ \dot{\lor} \ y)}, \varepsilon(x), \varepsilon(y) & \frac{\varepsilon(x \ \dot{\lor} \ y), \neg\varepsilon(x)}{\varepsilon(x \ \dot{\lor} \ y), \neg\varepsilon(y)} \\ \underline{\neg\varepsilon(\dot{\wedge} \ x)}, \neg\varepsilon(x) & \frac{\varepsilon(\dot{\wedge} \ x), \varepsilon(x)}{\varepsilon(\dot{\wedge} \ x), \neg\varepsilon(x)} \\ \underline{\neg\varepsilon(\dot{\forall}_T \ x)}, \varepsilon(x \ y) & \varepsilon(\dot{\forall}_T \ x), \neg\varepsilon(x \ H_T(x)) \end{array} $$

As we shall prove, Polarized resolution modulo with these one-way clauses is a complete method for Simple type theory, and attempting to prove a contradiction in this theory with this method yields an empty search space.

An alternative to this method is to transform the rules of $\mathcal{R}_-$ and $\mathcal{R}_+$ into axioms, with Proposition 3 and 5, add the clause form of these axioms to the set of clauses to be refuted, and use Equational resolution modulo $\mathcal{E}$. We obtain this way the same set of clauses, except that they are not one-way clauses:

$$ \begin{array}{l@{\qquad}l} \underline{\neg\varepsilon(x \ \dot{\lor} \ y)}, \varepsilon(x), \varepsilon(y) & \frac{\varepsilon(x \ \dot{\lor} \ y), \neg\varepsilon(x)}{\varepsilon(x \ \dot{\lor} \ y), \neg\varepsilon(y)} \\ \underline{\neg\varepsilon(\dot{\wedge} \ x)}, \neg\varepsilon(x) & \frac{\varepsilon(\dot{\wedge} \ x), \varepsilon(x)}{\varepsilon(\dot{\wedge} \ x), \neg\varepsilon(x)} \\ \underline{\neg\varepsilon(\dot{\forall}_T \ x)}, \varepsilon(x \ y) & \varepsilon(\dot{\forall}_T \ x), \neg\varepsilon(x \ H_T(x)) \end{array} $$

equational resolution, modulo SK, with these clauses is a complete proof search method for Simple type theory, but attempting to prove a contradiction in this theory with this method yields an infinite search space.

# 4 Soundness and Completeness

We now want to prove that Polarized resolution modulo is sound and complete, i.e. that if $A_1, \dots, A_n$ are closed clausal propositions, then $|A_1|[\emptyset], \dots, |A_n|[\emptyset] \mapsto_{\mathcal{R}} \square[C]$ for $\mathcal{C}$ unifiable if and only if the sequent $A_1, \dots, A_n \vdash$ has a cut free proof modulo $\mathcal{R}$. As a corollary, Polarized resolution modulo is complete if and only if the theory defined by the rewrite rules has the cut elimination property.
$\frac{U}{(t/x)U}$ **Instantiation**

$\frac{U}{U'}$ if $U = \varepsilon$ $U'$ **Conversion**

$\frac{U, P}{U \cup V}$ if $P \rightarrow_{-} A, V = |A|$ **Reduction**

$\frac{U, \neg P}{U \cup V}$ if $P \rightarrow_{+} \neg A, V = |A|$ **Reduction**

$\frac{U, P \quad U', \neg P}{U \cup U'}$ **Identical Resolution**

<caption>Fig. 3. Polarized extended identical resolution (PEIR)</caption>

As usual we introduce an intermediate system that we prove sound and complete and then lift the result to Polarized resolution modulo.

**Definition 9 (Polarized extended identical resolution).** Let $\mathcal{R}$ be a polarized rewrite system and $K$ a set of clauses, we write $K \hookrightarrow_{\mathcal{R}} U$ if the clause $U$ can be derived from the clauses of $K$ using finitely many applications of the Polarized extended identical resolution (PEIR) rules described in Figure 3. This means that there exists a derivation of the clause $U$ under the assumptions $K$, i.e. a sequence $U_1, \dots, U_n$ such that either $n = 0$ and $U$ is an element of $K$ or $n \ge 1$, $U_n = U$ and each $U_i$ is derived with a rule of Figure 3 from clauses of the set $K \cup \{U_1, \dots, U_{i-1}\}$.

Like [9], we prove directly the soundness of the PEIR method with respect to the cut free sequent calculus.

We write $\bar{\forall} A$ for the universal closure of $A$.

**Proposition 6.** Let $A_1, \dots, A_n, B_1, \dots, B_n$ be clausal propositions such that $|A_1| = |B_1|, \dots, |A_n| = |B_n|$. If $\Gamma, A_1, \dots, A_n \vdash \Delta$ has a cut free proof, then so does $\Gamma, B_1, \dots, B_n \vdash \Delta$.

*Proof.* We first prove that $\Gamma, C \lor D \vdash \Delta$ has a cut free proof if and only if $\Gamma, C \vdash \Delta$ and $\Gamma, D \vdash \Delta$ do. The result follows by a simple induction on proofs.

**Definition 10 (Partial instance).** A partial instance of a proposition $A$ is a reduct for $\rightarrow_{-}^*$ of a proposition of the form $\forall x_1 \dots \forall x_n (\sigma A)$ for some variables $x_1, \dots, x_n$ and substitution $\sigma$. The instance is strict if $n > 0$.

**Proposition 7.** Let $A$ and $B$ be two propositions and $C_1, \dots, C_n$ be partial instances of $A \lor B$. If the sequent $\Gamma, C_1, \dots, C_n \vdash \Delta$ has a cut free proof modulo $\mathcal{R}$, then so does $\Gamma, \bar{\forall}(A \lor P), \bar{\forall}(B \lor \neg P) \vdash \Delta$.

*Proof.* By induction on the structure of the proof of the sequent $\Gamma, C_1, \dots, C_n \vdash \Delta$. If the last rule is a rule on a proposition of $\Gamma$ or $\Delta$, a contraction rule, a
weakening rule, or the left rule of the universal quantifier, we just apply the
induction hypothesis. If it is the left rule of the disjunction, say to $C_1 = A' \lor B'$,
then we have cut free proofs of $\Gamma, A', C_2, \dots, C_n \vdash \Delta$ and $\Gamma, B', C_2, \dots, C_n \vdash \Delta$,
with $\sigma A \dashv\neg A'$ and $\sigma B \dashv\neg B'$. By induction hypothesis, we get cut free
proofs of the sequents $\Gamma, A', \overline{\forall}(A \lor P), \overline{\forall}(B \lor \neg P) \vdash \Delta$ and $\Gamma, B', \overline{\forall}(A \lor P), \overline{\forall}(B \lor \neg P) \vdash \Delta$.
and we build a cut free proof of $\Gamma, \overline{\forall}(A \lor P) \vdash \Delta$.

**Proposition 8.** Let $A$ and $B$ be two propositions and $C_1, \dots, C_n$ be partial instances of $A \lor B$. Let $P$ be a proposition such that $P \dashv\neg x_1 \dots \forall x_p B$ or $P \dashv\neg \neg x_1 \dots \forall x_p B$ where $x_1, \dots, x_p$ are variables not occurring free in $A$. If the sequent $\Gamma, C_1, \dots, C_n \vdash \Delta$ has a cut free proof modulo $\mathcal{R}$, then so does $\Gamma, \overline{\forall}(A \lor P) \vdash \Delta$.

*Proof.* By induction on the structure of the proof of the sequent $\Gamma, C_1, \dots, C_n \vdash \Delta$. If the last rule is a rule on a proposition of $\Gamma$ or $\Delta$, a contraction rule, a weakening rule, or the left rule of the universal quantifier, we just apply the induction hypothesis. If it is the left rule of the disjunction, say to $C_1 = A' \lor B'$, then we have cut free proofs of $\Gamma, A', C_2, \dots, C_n \vdash \Delta$ and $\Gamma, B', C_2, \dots, C_n \vdash \Delta$, with $\sigma A \dashv\neg A'$ and $\sigma B \dashv\neg B'$. By induction hypothesis, we get cut free proofs of $\Gamma, A', \overline{\forall}(A \lor P) \vdash \Delta$ and $\Gamma, B', \overline{\forall}(A \lor P) \vdash \Delta$, and we build a cut free proof of $\Gamma, \overline{\forall}(A \lor P) \vdash \Delta$.

**Proposition 9.** Let $A$ be a proposition and $C_1, \dots, C_n$ be strict partial instances of $(t/x)A$. If the sequent $\Gamma, C_1, \dots, C_n \vdash \Delta$ has a cut free proof modulo $\mathcal{R}$, then so does $\Gamma, \overline{\forall}A \vdash \Delta$.

*Proof.* By induction on the structure of the proof of $\Gamma, C_1, \dots, C_n \vdash \Delta$. If the last rule is a rule on a proposition of $\Gamma$ or $\Delta$, a contraction rule, a weakening rule, or the left rule of the universal quantifier producing a strict partial instance of $(t/x)A$, we just apply the induction hypothesis. If it is the left rule of the universal quantifier, say to $C_1$, producing a reduct $A'$ of $\sigma(t/x)A$, then we have a cut free proof of $\Gamma, A', C_2, \dots, C_n \vdash \Delta$ and by induction hypothesis we get a cut free proof of $\Gamma, A', \overline{\forall}A \vdash \Delta$ and we build a cut free proof of $\Gamma, \overline{\forall}A \vdash \Delta$.

**Proposition 10 (PEIR Soundness).** Let $A_1, \dots, A_n$ be closed clausal propositions. If $|A_1|, \dots, |A_n| \hookrightarrow_{\mathcal{R}} \emptyset$, then $A_1, \dots, A_n \vdash$ has a cut free proof modulo $\mathcal{R}$.

*Proof.* By induction on the structure the derivation $|A_1|, \dots, |A_n| \hookrightarrow_{\mathcal{R}} \emptyset$. If the derivation is empty, then one of the clauses $|A_i|$ is $\emptyset$. Thus, the proposition $A_i$ is $\perp$ and $A_1, \dots, A_n \vdash$ has a cut free proof modulo $\mathcal{R}$. Otherwise, the derivation of $|A_1|, \dots, |A_n| \hookrightarrow_{\mathcal{R}} \emptyset$ starts by producing a clause $U$ and there is a shorter derivation of $|A_1|, \dots, |A_n|, U \hookrightarrow_{\mathcal{R}} \emptyset$. Let $A'$ be a closed clausal proposition such that $U = |A'|$, by induction hypothesis, we have a cut free proof of $A_1, \dots, A_n, A' \vdash$. We consider four cases, according to the rule used to derive $U$.

- If this rule is the **Identical Resolution** rule, then there are two propositions, say $A_1$ and $A_2$, such that $|A_1|$ contains a literal $P$ and $|A_2|$ a literal $\neg P$.
Using Proposition 6, we can consider that $A_1 = \overline{\forall}(A'_1 \lor P), A_2 = \overline{\forall}(A'_2 \lor \neg P)$ and $A' = \overline{\forall}(A'_1 \lor A'_2)$. The proposition $A'$ is a partial instance of $A'_1 \lor A'_2$, thus, by Proposition 7, we get a cut free proof of the sequent $A_1, \dots, A_n, A_1, A_2 \vdash$ and, with a contraction, one of $A_1, \dots, A_n \vdash$.

- If this rule is the **Reduction** rule, then there is a proposition, say $A_1$, such that $A_1 = \overline{\forall}(A'_1 \lor P)$ with $P \dashv\neg x_1 \dots \forall x_p B$ or $P \dashv\neg\neg x_1 \dots \forall x_p B$ where $B$ is a disjunction of literals, and $A' = \overline{\forall}(A'_1 \lor B)$. The proposition $A'$ is a partial instance of $A'_1 \lor B$, thus, by Proposition 8, we get a cut free proof of the sequent $A_1, \dots, A_n, A_1 \vdash$ and, with a contraction, one of $A_1, \dots, A_n \vdash$.

- If this rule is the **Conversion** rule, then there is a proposition, say $A_1$ that is $\mathcal{E}$-equivalent to $A'$. We have $A_1 \dashv\neg A'$. By Proposition 1, we get a cut free proof of the sequent $A_1, \dots, A_n, A_1 \vdash$ and, with a contraction, one of $A_1, \dots, A_n \vdash$.

- If this rule is the **Instantiation** rule, then there is a proposition, say $A_1$, such that $A_1 = \overline{\forall}B$ and $A' = \overline{\forall}(t/x)B$. If the proposition $A'$ is a strict partial instance of $(t/x)B$, then, by Proposition 9, we get a cut free proof of the sequent $A_1, \dots, A_n, A_1 \vdash$ and, with a contraction, one of $A_1, \dots, A_n \vdash$. Otherwise, $A' = (t/x)B$, and we build a cut free proof of $A_1, \dots, A_n \vdash$.

We now prove the completeness of the PEIR method.

**Proposition 11 (Interpolation).** Let $P$ be an atomic proposition and $A$ be a non atomic one. If $P \dashv\neg A$, then there exists an atomic proposition $P'$ and a non atomic clausal proposition $A'$ such that $P \dashv\neg P'$ $\dashv$ $A'$ $\dashv\neg A$. If $P \dashv\neg\neg A$, then there exists an atomic proposition $P'$ and a clausal proposition $A_1$ such that $P \dashv\neg P'$ $\dashv$ $A_1$ $\dashv\neg A_1$.

*Proof.* Consider a reduction sequence, $P = B_0, \dots, B_n = A$ from $P$ to $A$ and let $P'$ be the last atomic proposition in this sequence. As $A$ is not atomic, $P'$ is not the last proposition of the sequence, let $A'$ be the next proposition in the sequence. We have $P \dashv\neg P'$ $\dashv$ $A'$ $\dashv\neg A$. As $P'$ reduces to $A'$ in one step, $A'$ is clausal proposition in the first case and it is the negation of a clausal proposition in the second.

**Proposition 12.** Let $K$ be a set of clauses and $U$ and $V$ two clauses. If $K, U \hookrightarrow_R \square$ and $K, V \hookrightarrow_R \square$ then $K, (U \cup V) \hookrightarrow_R \square$.

*Proof.* By induction on the structure of the derivation of $K, U \hookrightarrow_R \square$, there exists a derivation of $K, (U \cup V) \hookrightarrow_R \square$ or a derivation of $K, (U \cup V) \hookrightarrow_R V$. In the first case we are done, in the second, we use $K, V \hookrightarrow_R \square$ to conclude.

**Proposition 13 (PEIR Completeness).** Let $A_1, \dots, A_n$ be closed clausal propositions and $P_1, \dots, P_m$ be closed atomic propositions. If $A_1, \dots, A_n \vdash P_1, \dots, P_m$ has a cut free proof then $|A_1|, \dots, |A_n|, \neg P_1, \dots, \neg P_m \hookrightarrow_R \square$.

*Proof.* By Proposition 2, the sequent $A_1, \dots, A_n \vdash P_1, \dots, P_m$ has a closed cut free proof. By induction on the size of this proof.
∀x B. In both cases, we have $(t/x)B' \dashv^* (t/x)B$, by Proposition 1, $(t/x)B', A_2, \dots, A_n \vdash P_1, \dots, P_m$ has a cut free proof of the same size, by induction hypothesis, $|(t/x)B'|, |A_2|, \dots, |A_n|, \neg P_1, \dots, \neg P_m \hookrightarrow_R \Box$ and with the **Instantiation** rule, $|\forall x B'|, |A_2|, \dots, |A_n|, \neg P_1, \dots, \neg P_m \hookrightarrow_R \Box$. In the first case, we have $A_1 = \forall x B'$ and we are done. In the second, we have $A_1 \dashv^* A' \dashv \forall x B'$, thus, with the **Conversion** and **Reduction** rules, $|A_1|, |A_2|, \dots, |A_n|, \neg P_1, \dots, \neg P_m \hookrightarrow_R \Box$.

- If the last rule is the right rule of the negation, then one of the propositions, say $P_1$, reduces to a negation $\neg B$ and $B$, $A_1, \dots, A_n \vdash P_2, \dots, P_m$ has a smaller cut free proof. By Proposition 11, there exists an atomic proposition $P'$ and a clausal proposition $B'$ such that $P_1 \dashv^*_+ P' \dashv_+ \neg B' \dashv^*_+ \neg B$. Thus $B' \dashv^*_+ B$, by Proposition 1, $B', A_1, \dots, A_n \vdash P_2, \dots, P_m$ has a cut free proof of the same size, and, by induction hypothesis, $|B'|, |A_1|, \dots, |A_n|, \neg P_2, \dots, \neg P_m \hookrightarrow_R \Box$. We have $P_1 \dashv^*_+ P' \dashv_+ \neg B'$, thus, with the **Conversion** and **Reduction** rules, $|A_1|, |A_2|, \dots, |A_n|, \neg P_1, \dots, \neg P_m \hookrightarrow_R \Box$.

We now lift the soundness and completeness results from the PEIR method to Polarized resolution modulo.

**Definition 11 (Instance).** An instance of a constrained clause $U[C]$ is a clause $\theta U$ where $\theta$ is a unifier of $C$.

**Proposition 14.** If the constrained clause $\psi$ is derived with the **Resolution** rule from the renamings of two constrained clauses $\phi_1$ and $\phi_2$, then any instance of $\psi$ is derived in the PEIR system from instances of $\phi_1$ and $\phi_2$.

*Proof.* Let $(V_1, P_1, \dots, P_n)[C_1]$ and $(V_2, \neg Q_1, \dots, \neg Q_p)[C_2]$ be the renamings of $\phi_1$ and $\phi_2$ used to derive $\psi$. Then, $\psi = (V_1 \cup V_2)[C_1 \cup C_2 \cup \{P_1 = \dots = P_n = Q_1 = \dots = Q_p\}]$. Any instance of $\psi$ has the form $\theta(V_1 \cup V_2)$ for some unifier $\theta$ of $C_1 \cup C_2 \cup \{P_1 = \dots = P_n = Q_1 = \dots = Q_m\}$. The substitution $\theta$ is a unifier of $C_1$, thus $\theta(V_1, P_1, \dots, P_n)$ is an instance of $(V_1, P_1, \dots, P_n)[C_1]$, hence it is also an instance of $\phi_1$. In the same way and $\theta(V_2, \neg Q_1, \dots, \neg Q_p)$ is an instance of $\phi_2$. And $\theta(V_1 \cup V_2)$ is derived from these two clauses with the **Conversion** and **Identical Resolution** rules.

**Proposition 15.** If the constrained clause $\psi$ is derived with the **Extended Narrowing** rule from the renaming of a constrained clause $\phi$, then any instance of $\psi$ is derived in the PEIR system from an instance of $\phi$.

*Proof.* If the **Extended Narrowing** rule applied is the negative one, then let $(V_1, P)[C]$ be the renaming of $\phi$ and $V_2, \neg Q$ be the renaming of the one-way clause of $R$ used to derive $\psi$. We have $\psi = (V_1 \cup V_2)[C \cup \{P = Q\}]$. Any instance of $\psi$ has the form $\theta(V_1 \cup V_2)$ for some unifier $\theta$ of $C \cup \{P = Q\}$. The substitution $\theta$ is a unifier of $C$, thus $\theta(V_1, P)$ is an instance of $(V_1, P)[C]$ hence it is also an instance of $\phi$. There exists a proposition $A$ such that $\theta Q \dashv A$ and $|A| = \theta V_2$, thus $\theta(V_1 \cup V_2)$ is derived from this clause with the **Conversion** and **Reduction** rules. We proceed in the same way for the positive **Extended Narrowing** rule.
**Proposition 16 (Soundness).** Let $U_1, \dots, U_n$ be clauses. If $U_1[\emptyset], \dots, U_n[\emptyset] \mapsto_R \square[C]$ where $C$ is a unifiable set of constraints. Then, $U_1, \dots, U_n \mapsto_R \square$.

*Proof.* Let $K = \{U_1, \dots, U_n\}$ and $\Phi = \{U_1[\emptyset], \dots, U_n[\emptyset]\}$. With a simple induction on the structure of derivations and using Propositions 14 and 15, we get that if $\psi$ is a constrained clause such that $\Phi \mapsto_R \psi$ and $U$ is an instance of $\psi$, then there exists a set $L$ of instances of clauses of $\Phi$ such that $L \mapsto_R U$. Then, as $C$ is unifiable, the clause $\square$ is an instance of $\square[C]$, thus there exists a set $L$ of instances of clauses of $\Phi$, such that $L \mapsto_R \square$. As each element of $L$ can be obtained from a clause of $K$ with the **Instantiation** rule, we get $K \mapsto_R \square$.

**Proposition 17.** If the clause $V$ is derived with the **Identical Resolution** rule from clauses $U_1$ and $U_2$, $\mathcal{E}$-equivalent to instances of constrained clauses $\phi_1$ and $\phi_2$, then $V$ is $\mathcal{E}$-equivalent to an instance of a constrained clause derived in Polarized resolution modulo from renamings of $\phi_1$ and $\phi_2$.

*Proof.* As the **Identical Resolution** rule applies to $U_1$ and $U_2$ we have $U_1 = (U'_1, P)$ and $U_2 = (U'_2, \neg P)$, and $V = U'_1 \cup U'_2$. Consider two renamings $W_1[C_1]$ and $W_2[C_2]$ of $\phi_1$ and $\phi_2$. The clauses $U_1$ and $U_2$ are instance of $W_1[C_1]$ and $W_2[C_2]$, thus there exist two domain-disjoint unifiers $\theta_1$ and $\theta_2$ of $C_1$ and $C_2$, such that $\theta_1 W_1 =_{\mathcal{E}} (U'_1, P)$ and $\theta_2 W_2 =_{\mathcal{E}} (U'_2, \neg P)$. The substitution $\theta = \theta_1 \cup \theta_2$ is a unifier of $C_1 \cup C_2$ and we have $\theta W_1 =_{\mathcal{E}} (U'_1, P)$ and $\theta W_2 =_{\mathcal{E}} (U'_2, \neg P)$. Thus, the clause $W_1$ has the form $W'_1, P_1, \dots, P_n$ and the clause $W_2$ has the form $W'_2, \neg Q_1, \dots, \neg Q_p$ with $\theta W'_1 =_{\mathcal{E}} U'_1$, $\theta W'_2 =_{\mathcal{E}} U'_2$, $\theta P_i =_{\mathcal{E}} P$ and $\theta Q_j =_{\mathcal{E}} P$. The **Resolution** rule applies to $W_1[C_1]$ and $W_2[C_2]$ and derives the constrained clause $\psi = (W'_1 \cup W'_2)[C_1 \cup C_2 \cup \{P_1 = \dots = P_n = Q_1 = \dots = Q_p\}]$. The substitution $\theta$ is a unifier of the constraints of this clause and $V = U'_1 \cup U'_2 =_{\mathcal{E}} \theta(W'_1 \cup W'_2)$. Thus $V$ is $\mathcal{E}$-equivalent to an instance of $\psi$.

**Proposition 18.** If the clause $V$ is derived with the **Reduction** rule from a clause $U$, $\mathcal{E}$-equivalent to an instance of a constrained clause $\phi$, then $V$ is $\mathcal{E}$-equivalent to an instance of a constrained clause derived in Polarized resolution modulo from a renaming of $\phi$.

*Proof.* If the **Reduction** rule applied is negative, we have $U = (U', P)$, and there is a negative rule $Q \to A$ in $\mathcal{R}$ and a substitution $\sigma$ such that $P = \sigma Q$, $V = U' \cup |\sigma A|$. Taking the variables bound in $A$ out of the domain of $\sigma$, we have $|\sigma A| = \sigma |A|$. Let $Z = |A|$. The clause $(Z, \neg Q)$ is a one-way clause of $\mathcal{R}$, $P = \sigma Q$ and $V = U' \cup \sigma Z$. Consider a renaming $\overline{W}[C]$ of $\phi$ with fresh variables. There exists a unifier $\theta_0$ of $C$ such that $\theta_0 W =_{\mathcal{E}} (U', P)$. Thus, the clause $W$ has the form $W', P'_1, \dots, P'_n$ and $\theta_0 W' =_{\mathcal{E}} U'$ and $\theta_0 P'_i =_{\mathcal{E}} P$. Let $(Z_1, \neg Q_1), \dots, (Z_n, \neg Q_n)$ be $n$ renamings of the one-way clause $(Z, \neg Q)$ and $\theta_1, \dots, \theta_n$ be domain-disjoint substitutions such that $\theta_i Q_i = \sigma Q$ and $\theta_i Z_i = \sigma Z$. Let $\theta = \theta_0 \cup \theta_1 \cup \dots \cup \theta_n$, $\theta$ is a unifier of $C$, $\theta W' =_{\mathcal{E}} U'$, $\theta P'_i =_{\mathcal{E}} P$, $\theta Q_i = \sigma Q = P$ and $\theta Z_i = \sigma Z$. Applying the **Extended Narrowing** rule $n$ times to $W[C]$ yields the constrained clause $\psi = (W' \cup Z_1 \cup \dots \cup Z_n)[C \cup \{P_1 = Q_1, \dots, P_n = Q_n\}]$. The substitution $\theta$ is a unifier of the constraints of $\psi$ and $V = U' \cup \sigma Z =_{\mathcal{E}} \theta(W' \cup Z_1 \cup \dots \cup Z_n)$. We proceed in the same way for the positive **Reduction** rule.
**Proposition 19 (Completeness).** Let $U_1, \dots, U_n$ be clauses. If $U_1, \dots, U_n \hookrightarrow_R \square$ then $U_1[\emptyset], \dots, U_n[\emptyset] \hookrightarrow_R \square[C]$, where $C$ is a unifiable set of constraints.

*Proof.* Let $K = \{U_1, \dots, U_n\}$ and $\Phi = \{U_1[\emptyset], \dots, U_n[\emptyset]\}$. With a simple induction on the structure of derivations and with Propositions 17 and 18, we prove that if $K \hookrightarrow_R U$ then there exists a constrained clause $\psi$ such that $\Phi \hookrightarrow_R \psi$ and $U$ is $\mathcal{E}$-equivalent to an instance of $\psi$. Then, if $K \hookrightarrow_R \square$ then there exists a constrained clause $\psi$ such that $\Phi \hookrightarrow_R \psi$ and $\square$ is $\mathcal{E}$-equivalent to an instance of $\psi$. Thus $\psi = \square[C]$ where $C$ is a unifiable set of constraints.

**Theorem 1.** Let $A_1, \dots, A_n$ be closed clausal propositions. Then $|A_1[\emptyset], \dots, A_n[\emptyset] \hookrightarrow_R \square[C]|$ for $C$ unifiable if and only if $A_1, \dots, A_n \vdash$ has a cut free proof modulo $R$.

*Proof.* From Propositions 10, 13, 16, and 19.

## References

1. P.B. Andrews, Resolution in type theory, *The Journal of Symbolic Logic*, 36, 1971, pp. 414-432.

2. L. Bachmair and H. Ganzinger, Resolution Theorem Proving, in J.A. Robinson and A. Voronkov, *Handbook of Automated Reasoning*, Elsevier, 2001.

3. G. Burel, Embedding Deduction Modulo into a Prover, manuscript available on the web page of the author, 2010.

4. G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another? *Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice*. ACM International Conference Proceeding Series, 2009.

5. G. Dowek, What is a theory?, H. Alt, A. Ferreira (Eds.), *Symposium on Theoretical Aspects of Computer Science*, Lecture Notes in Computer Science, 2285, Springer-Verlag, 2002, pp. 50-64.

6. G. Dowek, Simple Type Theory as a clausal theory, manuscript available on the web page of the author, 2010.

7. G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an intentional first-order expression of higher-order logic, *Mathematical Structures in Computer Science*, 11, 2001, pp. 1-25.

8. G. Dowek, Th. Hardin, and C. Kirchner, Theorem proving modulo, *Journal of Automated Reasoning*, 31(1), 2003, pp. 33-72.

9. O. Hermant, Resolution is cut-free, *Journal of Automated Reasoning*, 44(3), 2010, pp. 245-276.

10. G. Huet, A mechanisation of Type Theory, *Third International Joint Conference on Artificial Intelligence*, 1973, pp. 139-146.

11. G. Peterson and M. E. Stickel, Complete sets of reductions for some equational theories, *Journal of the ACM* 28, 1981, pp. 233-264.

12. G. Plotkin, Building-in equational theories, *Machine Intelligence*, 7, 1972, pp. 73-90.

13. J.R. Slagle. Automatic theorem proving with renamable and semantic resolution. J. ACM, 14, 1967, pp. 687–697.

14. L. Wos, G.A. Robinson, D.F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. J. ACM, 12, 1965, pp. 536–541.