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 ⇔ (Q ⇒ R), are replaced by rewrite rules, for instance P ⟶ (Q ⇒ 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 ⟶ (Q ⇒ 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 ⇒ 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 ∀x (P (x) ⇔ P (f(x))) generates an infinite search space. But attempting to prove a contradiction with Resolution modulo the rule P (x) ⟶ 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 as 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 formulation 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, instead 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 \underline{¬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 resolution [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 Ordered Resolution. Indeed, Polarized resolution modulo fails in finite time when attempting to prove a contradiction in Simple type theory. Thus, its completeness 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 R = ⟨E, R_{−}, R_{+}⟩ where E is a set of equations between terms, R_{−} and R_{+} are sets of rewrite rules whose left hand sides are atomic propositions and right hand sides are arbitrary propositions. The rules of R_{−} are called negative rules and those of R_{+} are called positive rules.

Definition 2 (Polarized rewriting). Let R = ⟨E, R_{−}, R_{+}⟩ be a polarized rewrite system. We define the equivalence relation =_{E} as the congruence on terms generated by the equations of E. We then define the one step negative and positive rewriting relations ⟶_{−} and ⟶_{+} as follows.

– If t_{i} =_{E} u then both P (t_{1}, …, t_{i}, …, t_{n}) ⟶_{−} P (t_{1}, …, u, …, t_{n}) and P (t_{1}, …, t_{i}, …, t_{n}) ⟶_{+} P (t_{1}, …, u, …, t_{n}).

– If P ⟶ A is a rule of R_{s} and σ is a substitution then σP ⟶_{s} σA, where s is either − or +.

– If A ⟶\overline{s} A′ then ¬A ⟶_{s} ¬A′, where \overline{.} swaps − and +.

– If (A ⟶_{s} A′ and B = B′) or (A = A′ and B ⟶_{s} B′), then A ∧ B ⟶_{s} A′ ∧ B′ and A ∨ B ⟶_{s} A′ ∨ B′.

– If (A ⟶\overline{s} A′ and B = B′) or (A = A′ and B ⟶_{s} B′), then A ⇒ B ⟶_{s} A′ ⇒ B′.

– If A ⟶_{s} A′ then ∀x A ⟶_{s} ∀x A′ and ∃x A ⟶_{s} ∃x A′.

We define the sequent one step term rewriting relation ⟶ as follows.

– If A ⟶_{−} A′ then (Γ, A ⊢ Δ) ⟶ (Γ, A′ ⊢ Δ).

– If A ⟶_{+} A′ then (Γ ⊢ A, Δ) ⟶ (Γ ⊢ A′, Δ).

As usual, if R is any binary relation, we write 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 ⟶_{−}^{∗} and ⟶_{+}^{∗} are. The usual, non polarized, Deduction modulo can be recovered by taking R_{−} = R_{+} and predicate logic by taking E = R_{−} = R_{+} = ∅.

The following propositions are proved by induction over proof structure.

Proposition 1. If (Γ ⊢ Δ) ⟶^{∗} (Γ′ ⊢ Δ′) and Γ′ ⊢ Δ′ has a cut free proof modulo R then Γ ⊢ Δ has a cut free proof modulo R of the same size.

axiom if A ⟶_{−}^{∗} P, B ⟶_{+}^{∗} P and P atomic A ⊢ B

Γ, B ⊢ Δ Γ ⊢ C, Δ cut if A ⟶_{−}^{∗} B, A ⟶_{+}^{∗} C Γ ⊢ Δ

Γ, B, C ⊢ Δ contr-left if A ⟶_{−}^{∗} B, A ⟶_{−}^{∗} C Γ, A ⊢ Δ

Γ ⊢ B, C, Δ contr-right if A ⟶_{+}^{∗} B, A ⟶_{+}^{∗} C Γ ⊢ A, Δ

Γ ⊢ Δ ; weak-left ; Γ, A ⊢ Δ

Γ ⊢ Δ ; weak-right ; Γ ⊢ A, Δ

⊤-right if A ⟶_{+}^{∗} ⊤ Γ ⊢ A, Δ

⊥-left if A ⟶_{−}^{∗} ⊥ Γ, A ⊢ Δ

Γ ⊢ B, Δ ¬-left if A ⟶_{−}^{∗} ¬B Γ, A ⊢ Δ

Γ, B ⊢ Δ ¬-right if A ⟶_{+}^{∗} ¬B Γ ⊢ A, Δ

Γ, B, C ⊢ Δ ∧-left if A ⟶_{−}^{∗} (B ∧ C) Γ, A ⊢ Δ

Γ ⊢ B, Δ Γ ⊢ C, Δ ∧-right if A ⟶_{+}^{∗} (B ∧ C) Γ ⊢ A, Δ

Γ, B ⊢ Δ Γ, C ⊢ Δ ∨-left if A ⟶_{−}^{∗} (B ∨ C) Γ, A ⊢ Δ

Γ ⊢ B, C, Δ ∨-right if A ⟶_{+}^{∗} (B ∨ C) Γ ⊢ A, Δ

Γ ⊢ B, Δ Γ, C ⊢ Δ ⇒-left if A ⟶_{−}^{∗} (B ⇒ C) Γ, A ⊢ Δ

Γ, B ⊢ C, Δ ⇒-right if A ⟶_{+}^{∗} (B ⇒ C) Γ ⊢ A, Δ

Γ, C ⊢ Δ ⟨x, B, t⟩ ∀-left if A ⟶_{−}^{∗} ∀x B, (t/x)B ⟶_{−}^{∗} C Γ, A ⊢ Δ

Γ ⊢ B, Δ ⟨x, B⟩ ∀-right if A ⟶_{+}^{∗} ∀x B, x ∉ F V (Γ Δ) Γ ⊢ A, Δ

Γ, B ⊢ Δ ⟨x, B⟩ ∃-left if A ⟶_{−}^{∗} ∃x B, x ∉ F V (Γ Δ) Γ, A ⊢ Δ

Γ ⊢ C, Δ ⟨x, B, t⟩ ∃-right if A ⟶_{+}^{∗} ∃x B, (t/x)B ⟶_{+}^{∗} C Γ ⊢ A, Δ

Fig. 1. Polarized sequent calculus modulo

Proposition 2. Assume that the language contains a closed term and that Γ ⊢ Δ is a closed sequent. Then, if Γ ⊢ Δ 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 R, there is a set of axioms T such that Γ ⊢ Δ is provable modulo R if and only if there exists a finite subset T′ of T such that Γ, T′ ⊢ Δ 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 R into a pair formed with a weaker rewrite system R′ and a set of axioms T .

Definition 3 (Compatibility). Let R and R′ be polarized rewrite systems and T be a set of axioms. The system R is compatible with the pair ⟨R′, T ⟩ when

1. if A ⟶_{−}^{∗} B in R′ then A ⟶_{−}^{∗} B in R and if A ⟶_{+}^{∗} B in R′ then A ⟶_{+}^{∗} B in R,

2. if A ∈ T , then ⊢ A is provable modulo R,

3. if A ⟶_{−}^{∗} B in R, then there exists a finite subset T′ of T such that T′ ⊢ A ⇒ B is provable modulo R′,

4. if A ⟶_{+}^{∗} B in R, then there exists a finite subset T′ of T such that T′ ⊢ B ⇒ A is provable modulo R′.

Proposition 3 (Equivalence). Let R be a polarized rewrite system and ⟨R′, T ⟩ be a pair compatible with R, then the sequent Γ ⊢ Δ is provable modulo R, if and only if there exists a finite subset T′ of T such that the sequent Γ, T′ ⊢ Δ is provable modulo R′.

Proof. If Γ, T′ ⊢ Δ is provable modulo R′, it is provable modulo R and each A of T′ is provable modulo R. We conclude with the cut rule. The converse is a simple induction over proof structure.

Two particular cases are useful: R′ = ∅ i.e. all the rewrite rules are transformed into axioms, and R′ = E, i.e. only proposition rewrite rules are transformed into axioms.

Proposition 4. For all polarized rewrite systems R, there exists a set of axioms T such that R and ⟨∅, T ⟩ are compatible.

Proof. Take the universal closures of all the propositions A ⇒ B such that A ⟶_{−}^{∗} B or B ⟶_{+}^{∗} A.

Proposition 5. For all polarized rewrite systems R = ⟨E, R_{−}, R_{+}⟩, there exists a set of axioms T such that R and ⟨E, T ⟩ are compatible.

Proof. Take for each rule P ⟶_{−} A of R_{−} the universal closure of P ⇒ A and for each rule P ⟶_{+} A of R_{+} the universal closure of A ⇒ 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 ⊥ or of the form ∀x_{1} … ∀x_{p} (L_{1} ∨ … ∨ L_{n}) where L_{1}, …, L_{n} are literals and x_{1}, …, 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 R formed with the negative rule P ⟶ (¬Q ∨ R) and the positive rules P ⟶ ¬Q and P ⟶ ¬¬R is clausal. This rewrite system is compatible with the axiom P ⇔ (Q ⇒ R), in the same way the rule P ⟶ (Q ⇒ 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 ι and o. The language contains

– for each pair of sorts, a constant K_{T,U} of sort T → U → T,

– for each triple of sorts, a constant S_{T,U,V} of sort (T → U → V) → (T → U) → T → V,

– a constant ˙∨ of sort o → o → o,

– a constant ˙¬ of sort o → o,

– for each sort, a constant ˙∀_{T} of sort (T → o) → o,

– for each pair of sorts, a function symbol α_{T,U} of rank ⟨T → U, T, U⟩,

– for each sort T, a Skolem symbol H_{T} of sort (T → o) → T,

– a predicate symbol ε of rank ⟨o⟩.

As usual, we write (t u) for α_{T,U}(t, u) and (t u_{1} … u_{n}) for (… (t u_{1}) … u_{n}). The rewrite rules are

(K_{T,U} x y) =_{E} x
(S_{T,U,V} x y z) =_{E} (x z (y z))
ε(x ˙∨ y) ⟶_{−} (ε(x) ∨ ε(y)) ε(x ˙∨ y) ⟶_{+} ¬¬ε(x)
ε(x ˙∨ y) ⟶_{+} ¬¬ε(y)
ε( ˙¬ x) ⟶_{−} ¬ε(x)  ε( ˙¬ x) ⟶_{+} ¬ε(x)
ε( ˙∀_{T} x) ⟶_{−} ∀y ε(x y)  ε( ˙∀_{T} x) ⟶_{+} ¬¬ε(x H_{T} (x))

This theory does not have the cut elimination property as the sequent ε(x H_{T} (x)) ⊢ ∀y ε(x y) has a proof with a cut (on ε( ˙∀_{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 ι can be expressed by the rules

(Pred (Succ x)) =_{E} x

ε(Null 0) ⟶_{+} ¬⊥
ε(Null (Succ x)) ⟶_{−} ⊥

The first expresses that the function Succ of type ι → ι 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 θ such that θt =_{E} θ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 □. If U is a clause and L is a literal, we write U, L for the clause U ∪ {L}. If A = ∀x_{1} … ∀x_{p} (L_{1} ∨ … ∨ L_{n}) is a clausal proposition, we write |A| for the clause {L_{1}, …, L_{n}}. By convention, |⊥| = □. If ψ is a constrained clause and Φ a set of constrained clauses, a Φ-renaming of ψ is a renaming of ψ with variables that do not occur in Φ.

Definition 7 (One-way clause, Selected literal). To each polarized rewrite system, we associate a set of clauses called the one-way clauses of R. These clauses have a privileged literal called the selected literal. For each negative rule P ⟶ ∀x_{1} … ∀x_{p} (L_{1}∨…∨L_{n}), we take the clause \underline{¬P} , L_{1}, …, L_{n} and, for each positive rule P ⟶ ¬∀x_{1} … ∀x_{p} (L_{1} ∨…∨L_{n}), we take the clause \underline{P} , L_{1}, …, L_{n} where the selected literal is the underlined one.

Definition 8 (Polarized resolution modulo). Let Φ be a set of constrained clauses, we write Φ ↦_{R} ψ if the constrained clause ψ can be derived from the constrained clauses of Φ 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 ψ under the assumptions Φ, i.e. a sequence ψ_{1}, …, ψ_{n} such that either n = 0 and ψ is an element of Φ or n ≥ 1, ψ_{n} = ψ and each ψ_{i} is derived with a rule of Figure 2 from renamings of clauses of the set Φ ∪ {ψ_{1}, …, ψ_{i−1}}.

When R_{−} = R_{+} = ∅, 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 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, \underline{¬Q}, we derive the clause (U ∪ V)[C ∪ \{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

(U, P_{1}, …, P_{n})[C_{1}] (V, ¬Q_{1}, …, ¬Q_{p})[C_{2}] Resolution (U ∪ V)[C_{1} ∪ C_{2} ∪ {P_{1} = … = P_{n} = Q_{1} = … = Q_{p}}]

(U, P)[C]

if V, \underline{¬Q} one-way clause of R Extended Narrowing

(U ∪ V)[C ∪ {P = Q}]

(U, ¬P)[C]

if V, \underline{Q} one-way clause of R Extended Narrowing

(U ∪ V)[C ∪ {P = Q}]

Fig. 2. Polarized resolution modulo

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

\underline{¬ε(x ˙∨ y)}, ε(x), ε(y)  \underline{ε(x ˙∨ y)}, ¬ε(x)
\underline{ε(x ˙∨ y)}, ¬ε(y)
\underline{¬ε( ˙¬ x)}, ¬ε(x)  \underline{ε( ˙¬ x)}, ε(x)
\underline{¬ε( ˙∀_{T} x)}, ε(x y) \underline{ε( ˙∀_{T} x)}, ¬ε(x H_{T} (x))

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 R_{−} and 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 E. We obtain this way the same set of clauses, except that they are not one-way clauses:

¬ε(x ˙∨ y), ε(x), ε(y)  ε(x ˙∨ y), ¬ε(x)
ε(x ˙∨ y), ¬ε(y)
¬ε( ˙¬ x), ¬ε(x)  ε( ˙¬ x), ε(x)
¬ε( ˙∀_{T} x), ε(x y) ε( ˙∀_{T} x), ¬ε(x H_{T} (x))

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}, …, A_{n} are closed clausal propositions, then |A_{1}|[∅], …, |A_{n}|[∅] ↦_{R} □[C] for C unifiable if and only if the sequent A_{1}, …, A_{n} ⊢ has a cut free proof modulo 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.

U

Instantiation (t/x)U U

if U =_{E} U′ Conversion U′

U, P if P ⟶_{−} A, V = |A| Reduction U ∪ V

U, ¬P if P ⟶_{+} ¬A, V = |A| Reduction U ∪ V

U, P U′, ¬P

Identical Resolution

U ∪ U′

Fig. 3. Polarized extended identical resolution (PEIR)

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 R be a polarized rewrite system and K a set of clauses, we write K ↪_{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}, …, U_{n} such that either n = 0 and U is an element of K or n ≥ 1, U_{n} = U and each U_{i} is derived with a rule of Figure 3 from clauses of the set K ∪ {U_{1}, …, U_{i−1}}.

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

We write \overline{∀}A for the universal closure of A.

Proposition 6. Let A_{1}, …, A_{n}, B_{1}, …, B_{n} be clausal propositions such that |A_{1}| = |B_{1}|, …, |A_{n}| = |B_{n}|. If Γ, A_{1}, …, A_{n} ⊢ Δ has a cut free proof, then so does Γ, B_{1}, …, B_{n} ⊢ Δ.

Proof. We first prove that Γ, C ∨ D ⊢ Δ has a cut free proof if and only if Γ, C ⊢ Δ and Γ, D ⊢ Δ 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 ⟶_{−}^{∗} of a proposition of the form ∀x_{1} … ∀x_{n} (σA) for some variables x_{1}, …, x_{n} and substitution σ. The instance is strict if n > 0.

Proposition 7. Let A and B be two propositions and C_{1}, …, C_{n} be partial instances of A ∨ B. If the sequent Γ, C_{1}, …, C_{n} ⊢ Δ has a cut free proof modulo R, then so does Γ, \overline{∀}(A ∨ P), \overline{∀}(B ∨ ¬P) ⊢ Δ.

Proof. By induction on the structure of the proof of the sequent Γ, C_{1}, …, C_{n} ⊢ Δ. If the last rule is a rule on a proposition of Γ or Δ, 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′ ∨ B′, then we have cut free proofs of Γ, A′, C_{2}, …, C_{n} ⊢ Δ and Γ, B′, C_{2}, …, C_{n} ⊢ Δ, with σA ⟶_{−}^{∗} A′ and σB ⟶_{−}^{∗} B′. By induction hypothesis, we get cut free proofs of the sequents Γ, A′, \overline{∀}(A ∨ P), \overline{∀}(B ∨ ¬P) ⊢ Δ and Γ, B′, \overline{∀}(A ∨ P), \overline{∀}(B ∨ ¬P) ⊢ Δ and we build a cut free proof of Γ, \overline{∀}(A ∨ P), \overline{∀}(B ∨ ¬P) ⊢ Δ.

Proposition 8. Let A and B be two propositions and C_{1}, …, C_{n} be partial instances of A ∨ B. Let P be a proposition such that P ⟶_{−}^{∗} ∀x_{1} … ∀x_{p} B or P ⟶_{−}^{∗} ¬¬∀x_{1} … ∀x_{p} B where x_{1}, …, x_{p} are variables not occurring free in A. If the sequent Γ, C_{1}, …, C_{n} ⊢ Δ has a cut free proof modulo R, then so does Γ, \overline{∀}(A ∨ P) ⊢ Δ.

Proof. By induction on the structure of the proof of the sequent Γ, C_{1}, …, C_{n} ⊢ Δ. If the last rule is a rule on a proposition of Γ or Δ, 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′ ∨ B′, then we have cut free proofs of Γ, A′, C_{2}, …, C_{n} ⊢ Δ and Γ, B′, C_{2}, …, C_{n} ⊢ Δ, with σA ⟶_{−}^{∗} A′ and σB ⟶_{−}^{∗} B′. By induction hypothesis, we get cut free proofs of Γ, A′, \overline{∀}(A ∨ P) ⊢ Δ and Γ, B′, \overline{∀}(A ∨ P) ⊢ Δ, and we build a cut free proof of Γ, \overline{∀}(A ∨ P) ⊢ Δ.

Proposition 9. Let A be a proposition and C_{1}, …, C_{n} be strict partial instances of (t/x)A. If the sequent Γ, C_{1}, …, C_{n} ⊢ Δ has a cut free proof modulo R, then so does Γ, \overline{∀}A ⊢ Δ.

Proof. By induction on the structure of the proof of Γ, C_{1}, …, C_{n} ⊢ Δ. If the last rule is a rule on a proposition of Γ or Δ, 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 σ(t/x)A, then we have a cut free proof of Γ, A′, C_{2}, …, C_{n} ⊢ Δ and by induction hypothesis we get a cut free proof of Γ, A′, \overline{∀}A ⊢ Δ and we build a cut free proof of Γ, \overline{∀}A ⊢ Δ.

Proposition 10 (PEIR Soundness). Let A_{1}, …, A_{n} be closed clausal propositions. If |A_{1}|, …, |A_{n}| ↪_{R} □, then A_{1}, …, A_{n} ⊢ has a cut free proof modulo R.

Proof. By induction on the structure the derivation |A_{1}|, …, |A_{n}| ↪_{R} □. If the derivation is empty, then one of the clauses |A_{i}| is □. Thus, the proposition A_{i} is ⊥ and A_{1}, …, A_{n} ⊢ has a cut free proof modulo R. Otherwise, the derivation of |A_{1}|, …, |A_{n}| ↪_{R} □ starts by producing a clause U and there is a shorter derivation of |A_{1}|, …, |A_{n}|, U ↪_{R} □. Let A′ be a closed clausal proposition such that U = |A′|, by induction hypothesis, we have a cut free proof of A_{1}, …, A_{n}, A′ ⊢. 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 ¬P.

Using Proposition 6, we can consider that A_{1} = \overline{∀}(A′_{1} ∨P), A_{2} = \overline{∀}(A′_{2} ∨¬P) and A′ = \overline{∀}(A′_{1}∨A′_{2}). The proposition A′ is a partial instance of A′_{1}∨A′_{2}, thus, by Proposition 7, we get a cut free proof of the sequent A_{1}, …, A_{n}, A_{1}, A_{2} ⊢ and, with a contraction, one of A_{1}, …, A_{n} ⊢.

– If this rule is the Reduction rule, then there is a proposition, say A_{1}, such that A_{1} = \overline{∀}(A′_{1} ∨ P) with P ⟶_{−}^{∗} ∀x_{1} … ∀x_{p} B or P ⟶_{−}^{∗} ¬¬∀x_{1} … ∀x_{p} B where B is a disjunction of literals, and A′ = \overline{∀}(A′_{1} ∨ B). The proposition A′ is a partial instance of A′_{1} ∨B, thus, by Proposition 8, we get a cut free proof of the sequent A_{1}, …, A_{n}, A_{1} ⊢ and, with a contraction, one of A_{1}, …, A_{n} ⊢.

– If this rule is the Conversion rule, then there is a proposition, say A_{1} that is E-equivalent to A′. We have A_{1} ⟶_{−}^{∗} A′. By Proposition 1, we get a cut free proof of the sequent A_{1}, …, A_{n}, A_{1} ⊢ and, with a contraction, one of A_{1}, …, A_{n} ⊢.

– If this rule is the Instantiation rule, then there is a proposition, say A_{1}, such that A_{1} = \overline{∀}B and A′ = \overline{∀}(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}, …, A_{n}, A_{1} ⊢ and, with a contraction, one of A_{1}, …, A_{n} ⊢. Otherwise, A′ = (t/x)B, and we build a cut free proof of A_{1}, …, A_{n} ⊢.

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 ⟶_{−}^{∗} A, then there exists an atomic proposition P′ and a non atomic clausal proposition A′ such that P ⟶_{−}^{∗} P′ ⟶_{−} A′ ⟶_{−}^{∗} A. If P ⟶_{+}^{∗} A, then there exists an atomic proposition P′ and a clausal proposition A_{1} such that P ⟶_{+}^{∗} P′ ⟶_{+} ¬A_{1} ⟶_{+}^{∗} A.

Proof. Consider a reduction sequence, P = B_{0}, …, 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 ⟶_{−}^{∗} P′ ⟶_{−} A′ ⟶_{−}^{∗} 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 ↪_{R} □ and K, V ↪_{R} □ then K, (U ∪ V) ↪_{R} □.

Proof. By induction on the structure of the derivation of K, U ↪_{R} □, there exists a derivation of K, (U ∪ V) ↪_{R} □ or a derivation of K, (U ∪ V) ↪_{R} V. In the first case we are done, in the second, we use K, V ↪_{R} □ to conclude.

Proposition 13 (PEIR Completeness). Let A_{1}, …, A_{n} be closed clausal propositions and P_{1}, …, P_{m} be closed atomic propositions. If A_{1}, …, A_{n} ⊢ P_{1}, …, P_{m} has a cut free proof then |A_{1}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

Proof. By Proposition 2, the sequent A_{1}, …, A_{n} ⊢ P_{1}, …, P_{m} has a closed cut free proof. By induction on the size of this proof.

– If the last rule is an axiom, then n = m = 1, A_{1} ⟶_{−}^{∗} Q and P_{1} ⟶_{+}^{∗} Q for an atomic proposition Q. Thus, A_{1} is atomic, |A_{1}| = A_{1} and, using the Reduction, Conversion and Identical Resolution rules, we get |A_{1}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

– If the last rule is the left contraction rule, then one of the propositions, say A_{1}, reduces to propositions B and C and B, C, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} has a smaller cut free proof. By Proposition 1, A_{1}, A_{1}, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} has a cut free proof of the same size. Thus, by induction hypothesis, |A_{1}|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

– If the last rule is the right contraction rule, the argument is the same.

– If the last rule is the left weakening rule, then one of the propositions, say A_{1}, is erased and the sequent A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} has a smaller cut free proof. By induction hypothesis, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □ and thus |A_{1}|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

– If the last rule is the right weakening rule, the argument is the same.

– If the last rule is the left rule of the disjunction, then one of the propositions, say A_{1}, reduces to a disjunction B ∨ C and B, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} and C, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} have smaller cut free proofs. Thus, A_{1} is either a disjunction B′ ∨ C′ or an atomic proposition, in which case |A_{1}| = A_{1}, and, by Proposition 11, there exists an atomic proposition A′ and a clausal proposition B′ ∨C′ such that A_{1} ⟶_{−}^{∗} A′ ⟶_{−} B′ ∨C′ ⟶_{−}^{∗} B ∨C. In both cases, we have B′ ⟶_{−}^{∗} B and C′ ⟶_{−}^{∗} C, by Proposition 1, B′, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} and C′, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} have cut free proofs of the same size, by induction hypothesis, |B′|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □ and |C′|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □ and by Proposition 12, |B′∨C′|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □. In the first case, we have A_{1} = B′ ∨ C′ and we are done. In the second, we have A_{1} ⟶_{−}^{∗} A′ ⟶_{−} B′ ∨ C′, thus, with the Conversion and Reduction rules, |A_{1}|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

– If the last rule is the left rule of the negation, then one of the propositions, say A_{1}, reduces to a negation ¬B and A_{2}, …, A_{n} ⊢ B, P_{1}, …, P_{m} has a smaller cut free proof. Thus, A_{1} is either a negation ¬B′ or an atomic proposition, in which case |A_{1}| = A_{1}, and, by Proposition 11, there exists an atomic proposition A′ and a clausal proposition ¬B′ such that A_{1} ⟶_{−}^{∗} A′ ⟶_{−} ¬B′ ⟶_{−}^{∗} ¬B. In both cases, we have B′ ⟶_{+}^{∗} B, by Proposition 1, A_{2}, …, A_{n} ⊢ B′, P_{1}, …, P_{m} has a cut free proof of the same size, and, by induction hypothesis, |A_{2}|, …, |A_{n}|, ¬B′, ¬P_{1}, …, ¬P_{m} ↪_{R} □. In the first case, we have A_{1} = ¬B′ and we are done. In the second, we have A_{1} ⟶_{−}^{∗} A′ ⟶_{−} ¬B′, thus, with the Conversion and Reduction rules, |A_{1}|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

– If the last rule is the left rule of the universal quantifier, then one of the propositions, say A_{1}, reduces to a universal proposition ∀x B and (t/x)B, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} has a smaller cut free proof. Thus, A_{1} is either a universal proposition ∀x B′ or an atomic proposition, in which case |A_{1}| = A_{1}, and, by Proposition 11, there exists an atomic proposition A′ and a clausal proposition ∀x B′ such that A_{1} ⟶_{−}^{∗} A′ ⟶_{−} ∀x B′ ⟶_{−}^{∗} ∀x B. In both cases, we have (t/x)B′ ⟶_{−}^{∗} (t/x)B, by Proposition 1, (t/x)B′, A_{2}, …, A_{n} ⊢ P_{1}, …, P_{m} has a cut free proof of the same size, by induction hypothesis, |(t/x)B′|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □ and with the Instantiation rule, |∀x B′|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □. In the first case, we have A_{1} = ∀x B′ and we are done. In the second, we have A_{1} ⟶_{−}^{∗} A′ ⟶_{−} ∀x B′, thus, with the Conversion and Reduction rules, |A_{1}|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

– If the last rule is the right rule of the negation, then one of the propositions, say P_{1}, reduces to a negation ¬B and B, A_{1}, …, A_{n} ⊢ P_{2}, …, 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} ⟶_{+}^{∗} P′ ⟶_{+} ¬B′ ⟶_{+}^{∗} ¬B. Thus B′ ⟶_{−}^{∗} B, by Proposition 1, B′, A_{1}, …, A_{n} ⊢ P_{2}, …, P_{m} has a cut free proof of the same size, and, by induction hypothesis, |B′|, |A_{1}|, …, |A_{n}|, ¬P_{2}, …, ¬P_{m} ↪_{R} □. We have P_{1} ⟶_{+}^{∗} P′ ⟶_{+} ¬B′, thus, with the Conversion and Reduction rules, |A_{1}|, |A_{2}|, …, |A_{n}|, ¬P_{1}, …, ¬P_{m} ↪_{R} □.

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 θU where θ is a unifier of C.

Proposition 14. If the constrained clause ψ is derived with the Resolution rule from the renamings of two constrained clauses ϕ_{1} and ϕ_{2}, then any instance of ψ is derived in the PEIR system from instances of ϕ_{1} and ϕ_{2}.

Proof. Let (V_{1}, P_{1}, …, P_{n})[C_{1}] and (V_{2}, ¬Q_{1}, …, ¬Q_{p})[C_{2}] be the renamings of ϕ_{1} and ϕ_{2} used to derive ψ. Then, ψ = (V_{1} ∪ V_{2})[C_{1} ∪ C_{2} ∪ {P_{1} = … = P_{n} = Q_{1} = … = Q_{p}}]. Any instance of ψ has the form θ(V_{1} ∪ V_{2}) for some unifier θ of C_{1} ∪ C_{2} ∪ {P_{1} = … = P_{n} = Q_{1} = … = Q_{m}}. The substitution θ is a unifier of C_{1}, thus θ(V_{1}, P_{1}, …, P_{n}) is an instance of (V_{1}, P_{1}, …, P_{n})[C_{1}], hence it is also an instance of ϕ_{1}. In the same way and θ(V_{2}, ¬Q_{1}, …, ¬Q_{p}) is an instance of ϕ_{2}. And θ(V_{1} ∪ V_{2}) is derived from these two clauses with the Conversion and Identical Resolution rules.

Proposition 15. If the constrained clause ψ is derived with the Extended Narrowing rule from the renaming of a constrained clause ϕ, then any instance of ψ is derived in the PEIR system from an instance of ϕ.

Proof. If the Extended Narrowing rule applied is the negative one, then let (V_{1}, P)[C] be the renaming of ϕ and V_{2}, \underline{¬Q} be the renaming of the one-way clause of R used to derive ψ. We have ψ = (V_{1} ∪ V_{2})[C ∪ {P = Q}]. Any instance of ψ has the form θ(V_{1} ∪ V_{2}) for some unifier θ of C ∪ {P = Q}. The substitution θ is a unifier of C, thus θ(V_{1}, P) is an instance of (V_{1}, P)[C] hence it is also an instance of ϕ. There exists a proposition A such that θQ ⟶ A and |A| = θV_{2}, thus θ(V_{1} ∪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}, … U_{n} be clauses. If U_{1}[∅], …, U_{n}[∅] ↦_{R} □[C] where C is a unifiable set of constraints. Then, U_{1}, …, U_{n} ↪_{R} □.

Proof. Let K = {U_{1}, … U_{n}} and Φ = {U_{1}[∅], …, U_{n}[∅]}. With a simple induction on the structure of derivations and using Propositions 14 and 15, we get that if ψ is a constrained clause such that Φ ↦_{R} ψ and U is an instance of ψ, then there exists a set L of instances of clauses of Φ such that L ↪_{R} U. Then, as C is unifiable, the clause □ is an instance of □[C], thus there exists a set L of instances of clauses of Φ, such that L ↪_{R} □. As each element of L can be obtained from a clause of K with the Instantiation rule, we get K ↪_{R} □.

Proposition 17. If the clause V is derived with the Identical Resolution rule from clauses U_{1} and U_{2}, E-equivalent to instances of constrained clauses ϕ_{1} and ϕ_{2}, then V is E-equivalent to an instance of a constrained clause derived in Polarized resolution modulo from renamings of ϕ_{1} and ϕ_{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}, ¬P), and V = U′_{1} ∪ U′_{2}. Consider two renamings W_{1}[C_{1}] and W_{2}[C_{2}] of ϕ_{1} and ϕ_{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 θ_{1} and θ_{2} of C_{1} and C_{2}, such that θ_{1}W_{1} =_{E} (U′_{1}, P) and θ_{2}W_{2} =_{E} (U′_{2}, ¬P). The substitution θ = θ_{1} ∪ θ_{2} is a unifier of C_{1} ∪ C_{2} and we have θW_{1} =_{E} (U′_{1}, P) and θW_{2} =_{E} (U′_{2}, ¬P). Thus, the clause W_{1} has the form W′_{1}, P_{1}, …, P_{n} and the clause W_{2} has the form W′_{2}, ¬Q_{1}, …, ¬Q_{p} with θW′_{1} =_{E} U′_{1}, θW′_{2} =_{E} U′_{2}, θP_{i} =_{E} P and θQ_{j} =_{E} P. The Resolution rule applies to W_{1}[C_{1}] and W_{2}[C_{2}] and derives the constrained clause ψ = (W′_{1} ∪ W′_{2})[C_{1} ∪ C_{2} ∪ {P_{1} = … = P_{n} = Q_{1} = … = Q_{p}}]. The substitution θ is a unifier of the constraints of this clause and V = U′_{1} ∪ U′_{2} =_{E} θ(W′_{1} ∪ W′_{2}). Thus V is E-equivalent to an instance of ψ.

Proposition 18. If the clause V is derived with the Reduction rule from a clause U, E-equivalent to an instance of a constrained clause ϕ, then V is Eequivalent to an instance of a constrained clause derived in Polarized resolution modulo from a renaming of ϕ.

Proof. If the Reduction rule applied is negative, we have U = (U′, P), and there is a negative rule Q ⟶ A in R and a substitution σ such that P = σQ, V = U′∪|σA|. Taking the variables bound in A out of the domain of σ, we have |σA| = σ|A|. Let Z = |A|. The clause (Z, \underline{¬Q}) is a one-way clause of R, P = σQ and V = U′ ∪ σZ. Consider a renaming W [C] of ϕ with fresh variables. There exists a unifier θ_{0} of C such that θ_{0}W =_{E} (U′, P). Thus, the clause W has the form W′, P′_{1}, …, P′_{n} and θ_{0}W′ =_{E} U′ and θ_{0}P′_{i} =_{E} P. Let (Z_{1}, \underline{¬Q_{1}}), ..., (Z_{n}, \underline{¬Q_{n}}) be n renamings of the one-way clause (Z, \underline{¬Q}) and θ_{1}, ..., θ_{n} be domain-disjoint substitutions such that θ_{i}Q_{i} = σQ and θ_{i}Z_{i} = σZ. Let θ = θ_{0} ∪ θ_{1} ∪ ... ∪ θ_{n}, θ is a unifier of C, θW′ =_{E} U′, θP′_{i} =_{E} P, θQ_{i} = σQ = P and θZ_{i} = σZ. Applying the Extended Narrowing rule n times to W [C] yields the constrained clause ψ = (W′ ∪ Z_{1} ∪ ... ∪ Z_{n})[C ∪ {P_{1} = Q_{1}, …, P_{n} = Q_{n}}]. The substitution θ is a unifier of the constraints of ψ and V = U′ ∪ σZ =_{E} θ(W′ ∪ Z_{1} ∪ ... ∪ Z_{n}). We proceed in the same way for the positive Reduction rule.

Proposition 19 (Completeness). Let U_{1}, …, U_{n} be clauses. If U_{1}, …, U_{n} ↪_{R} □ then U_{1}[∅], …, U_{n}[∅] ↦_{R} □[C], where C is a unifiable set of constraints.

Proof. Let K = {U_{1}, …, U_{n}} and Φ = {U_{1}[∅], …, U_{n}[∅]}. With a simple induction on the structure of derivations and with Propositions 17 and 18, we prove that if K ↪_{R} U then there exists a constrained clause ψ such that Φ ↦_{R} ψ and U is E-equivalent to an instance of ψ. Then, if K ↪_{R} □ then there exists a constrained clause ψ such that Φ ↦_{R} ψ and □ is E-equivalent to an instance of ψ. Thus ψ = □[C] where C is a unifiable set of constraints.

Theorem 1. Let A_{1}, …, A_{n} be closed clausal propositions. Then |A_{1}|[∅], …, |A_{n}|[∅] ↦_{R} □[C] for C unifiable if and only if A_{1}, …, A_{n} ⊢ 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 firstorder 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.