Guillaume Burel
email: guillaume.burel@ens-lyon.org

Claude Kirchner
email: claude.kirchner@inria.fr

A, B ∧ ¬A A ⊢ ¬a ⊢ ¬-L B

Regaining Cut Admissibility in Deduction Modulo using

Keywords: Automated deduction, rewriting, Knuth-Bendix completion, critical proofs, cut admissibility, deduction modulo, proof ordering, abstract canonical system, computational proof

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.

Introduction

Proof assistants like Coq, PVS or Isabelle-HOL are now well mastered systems both from the conceptual and implementation points of view. They allow for the development of large and even very large proofs like the one of the four-color theorem [START_REF] Gonthier | A computer-checked proof of the Four Colour Theorem[END_REF]. They allow also for a broad use of these techniques, making computer-aided proof development an approach now in use at the industrial level, for instance for making the formal proof of security issues of java card [START_REF] Chetali | A world-first smart card CC certificate with formal assurances[END_REF][START_REF] Chetali | Industrial Use of Formal Methods for a High-Level Security Evaluation[END_REF].

This important activity in the use of current proof assistants enlightens the crucial lack of computing power easily combinable with the deductive capabilities of such systems. If the complementarity and interaction between computation and deduction is identified since at least Henri Poincaré, its formalization as deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] is an appropriate way to present first-order logic as well as any logic in general.

Deduction modulo should therefore be at the heart of proof assistants and proof search methods, either implicitly or explicitly [see for instance [START_REF] Dowek | Theorem Proving Modulo[END_REF][START_REF] Peterson | Complete Sets of Reductions for Some Equational Theories[END_REF][START_REF] Barendregt | Autarkic Computations in Formal Proofs[END_REF][START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF] and getting a deep understanding of its logical behavior is of prime interest either for theoretical or practical purposes.

In deduction modulo, computations are modeled by a congruence relation between terms and between propositions. The logical deductions are done modulo this congruence that is represented by a rewrite relation over first-order terms and propositions. This permits to construct proofs that are often more readable, because the really deductive steps appear clearly, and also shorter, as was shown by Burel [START_REF] Burel | Unbounded Proof-Length Speed-up in Deduction Modulo[END_REF]. A first interesting question is to know which theories can be represented by such a congruence. It turns out, as we show in this paper, that any finitely presented first-order theory can be transformed into such a rewrite relation, as far as one is only concerned with classical logic. Nevertheless, the additional expressiveness capabilities added by the congruence entails that the Hauptsatz, i.e. the fact that cuts are not needed to build proofs, is no longer true. This can be seen in particular from an example derived from Crabbé's proof of the non-normalization of Zermelo's theory [START_REF] Crabbé | Non-normalisation de la théorie de Zermelo[END_REF] (see for instance [START_REF] Dowek | Theorem Proving Modulo[END_REF] and Footnote 3 below). And indeed the gap is important as we are proving in this paper that the admissibility of the cut rule is undecidable when one works modulo.

But cut elimination is fundamental for several related reasons: first, it implies the consistency of the logic, and in the case of deduction modulo the consistency of the theory associated with the rewrite relation. Second, it entails the subformula property2 , so that the search space is, in a sense, limited. The tableau method is based on this fact, and for instance TaMed [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF][START_REF] Bonichon | A Semantic Completeness Proof for TaMed[END_REF], a tableau method based on deduction modulo, is shown to be complete only for cut-free systems. Third, it has been shown by Hermant [11] that the proof search method for deduction modulo ENAR [START_REF] Dowek | Theorem Proving Modulo[END_REF]-which generalizes resolution and narrowingis equivalent to the cut-free fragment of deduction modulo, i.e. a sequent has a cut-free proof in deduction modulo if and only if ENAR can find a proof. ENAR is therefore complete if and only if the cut rule is admissible. This is also the case in the more recently introduced Polarized Resolution Modulo [START_REF] Dowek | Polarized resolution modulo[END_REF].

So on the one hand, we like to have a powerful congruence but this may be at the price of losing cut admissibility. How can we get both? It has been shown by Dowek [13] that cut admissibility is equivalent to the confluence of the rewrite system, provided only first-order terms are rewritten. In case the term rewrite system we are considering is not confluent, we can apply standard (a.k.a. Knuth-Bendix [START_REF] Knuth | Simple word problems in universal algebras[END_REF]) completion to get an equivalent term rewrite system which is confluent, and that way, we regain the cut admissibility. It is however no longer true when propositions are also rewritten, and the cut admissibility is in that case a stronger notion than confluence. Dowek wanted therefore to build a generalized completion procedure whose input is a rewrite system over first-order terms and atomic propositions and computing a rewrite system such that the associated sequent calculus modulo admits cut. He proposed such a completion procedure for the quantifier free case [START_REF] Dowek | What Is a Theory?[END_REF], based on the construction of a model for the theory associated with the rewrite system.

To solve this question, including unlimited use of quantifiers, we use here a quite different approach based on the notion of abstract canonical system and inference introduced by Dershowitz and Kirchner [START_REF] Dershowitz | Abstract Canonical Presentations[END_REF], Bonacina and Dershowitz [START_REF] Bonacina | Abstract canonical inference[END_REF]. This abstract framework is based on a proof ordering whose goal is to apprehend the notion of proof quality from which the notions of canonicity, completeness and redundancy follow up. It is shown to be well adapted to existing completion procedures such as ground completion [START_REF] Dershowitz | Canonicity[END_REF] and standard (a.k.a. Knuth-Bendix [START_REF] Knuth | Simple word problems in universal algebras[END_REF]) completion [START_REF] Burel | Completion Is an Instance of Abstract Canonical System Inference[END_REF].

To present the general idea of our approach, let us consider the simple example of Crabbé's axiom [START_REF] Crabbé | Non-normalisation de la théorie de Zermelo[END_REF] A ⇔ B ∧ ¬A 3 . Can we find, for the sequent calculus modulo the associated rewrite system A → B ∧ ¬A, a provable sequent without any cut-free proof? Indeed, let us try to build a minimal example. We will show in Proposition 39 that such a proof, in its simplest form, is necessarily of the shape:

. . . .

A, B ∧ ¬A ⊢ A ⊢ ↑-l . . . . ⊢ B ∧ ¬A, A ⊢ A ↑-r ⊢ Cut(A)
where the rules labeled "↑-r" and "↑-l" allow to unfold the oriented axioms respectively on the right or on the left. In order to validate this proof pattern, we have to check if it is possible to close both sides of the proof tree, possibly adding informations in the initial sequent.

admits the cut rule and has the same expressive power as the initial one.

The study of this question indeed reveals general properties of the sequent calculus modulo and our contributions are the following:

• We define several variants of the sequent calculus modulo more adapted to prove the results of the paper (Section 2.2): the unfolding sequent calculus allows only atomic propositions to be rewritten, step by step; in addition, the polarized unfolding sequent calculus separates which rules can be applied to a proposition on the left and on the right of a sequent; both variants behave the same way, especially w.r.t. cut-free proofs, as the asymmetric sequent calculus modulo of Dowek [START_REF] Dowek | Confluence as a Cut Elimination Property[END_REF], which in turn is equivalent to the original version of the sequent calculus modulo by Dowek et al. [START_REF] Dowek | Theorem Proving Modulo[END_REF] when the rewrite system is confluent;

• We prove, using a semantical argument, that it is undecidable to know if the unfolding sequent calculus associated with a given proposition rewrite system admits cuts (Theorem 15);

• We show how to transform a finite set of axioms into a finite rewrite system, such that the theory induced by the set of axioms is the same as the one proved by the classical sequent calculus modulo the rewrite system (Section 4);

• We provide an appropriate Noetherian ordering on the proofs of the unfolding sequent calculus; This ordering allows us to set on the proof space of unfolding sequent calculus a structure of abstract canonical system (Theorem 37); We characterize the critical proofs in deduction modulo as simple cuts (Proposition 39); We establish a precise correspondence between the limit of a completion process and a cut-free sequent calculus (Theorem 41), therefore bypassing the undecidability of the cut admissibility in the same way as standard completion circumvents the undecidability of the confluence of a rewrite system;

• We show the applicability of the general results, in particular on sequent calculus modulo rewrite systems involving quantifiers, therefore generalizing all previously known results such as the ones of Dowek [START_REF] Dowek | What Is a Theory?[END_REF];

As an important by-product of these results, we demonstrate the expressive power of abstract canonical systems (ACS for short).

The next section presents basic notions on rewriting and introduces the variants of sequent calculi modulo that are used in the paper, proving their equivalence, in particular concerning cut admissibility. In Section 3, we show the undecidability of the cut admissibility in deduction modulo. The rest of the paper is therefore dedicated to ways to circumvent this. Section 4 describes an algorithm which transforms finitely presented first-order theories into rewrite systems such that the sequent calculus modulo proves the theory. It exhibits three important properties of the algorithm (Properties 16, 17 and 19) that are enough to define the completion procedure detailed in Section 5. This procedure is based on the framework of the ACS, which is recalled in Section 5.1. The unfolding sequent calculus is shown to be an instance of this framework (Section 5.2). This allows us in Section 5.3 to characterize the critical proofs of deduction modulo and to set-up the completion process as the appropriate (and indeed non-trivial) instance of the abstract completion process. We conclude after presenting in more details Crabbé's example as well as several examples involving quantifiers.

This paper is a profoundly revised and extended version of the paper presented at LFCS'07 [START_REF] Burel | Cut Elimination in Deduction Modulo by Abstract Completion[END_REF] and it includes detailed proofs, examples and motivations.

Deduction modulo

Rewritings

We define here how propositions are rewritten in deduction modulo. Bases on rewriting can be found in [START_REF] Baader | Term Rewriting and all That[END_REF]. We present here briefly what we need for this paper to be self-contained, mainly by introducing notations. We denote by T (Σ, V ) the set of first-order terms built from a signature Σ and a set of variables V . An atomic proposition is given by a predicate symbol A of arity n and by n terms t 1 , . . . , t n ∈ T (Σ, V ). It is denoted A(t 1 , . . . , t n ). Propositions can be built using the following grammar4 :

P ! = A | ¬P | P ∧ P | P ∨ P | P ⇒ P | ∀x. P | ∃x. P
where A ranges over atomic propositions and x over variables. P ⇔ Q will be used as a syntactic sugar for (P ⇒ Q) ∧ (Q ⇒ P ), as well as Γ for P 1 ∧ . . . ∧ P n ; Γ for P 1 ∨ . . . ∨ P n and ¬Γ for ¬P 1 , . . . , ¬P n when Γ = P 1 , . . . , P n . Free variables of a proposition and substitutions are defined as usual. The replacement of a variable x by a term t in a proposition P is denoted by {t/x}P . A position in a term or a proposition t is a path in the tree representing t. The subterm or subproposition t |p of t at position p is the term or proposition represented by the subtree of t whose root is the last node of p. The replacement in t of the subterm t |p by s is denoted by t[s] p .

A term rewrite rule is the pair of terms l, r such that all free variables of r appear in l. It is denoted l → r. A term rewrite system is a set of term rewrite rules.

A term s can be rewritten to a term t by a term rewrite rule l → r if there exists some substitution σ such that σl = s and σr = t. This is extended to all terms, and then to all propositions by congruence.

A proposition rewrite rule is the pair of an atomic proposition A and a proposition P , such that all free variables of P appear in A. It is denoted A → P . A proposition rewrite system is a set of proposition rewrite rules.

An atomic proposition A can be rewritten to a proposition P by a proposition rewrite rule B → Q if there exists some substitution σ such that σB = A and σQ = P . This is extended to all propositions by congruence. It should be noted that the proposition rewrite relation should be seen, at least at first approximation, as an equivalence between propositions, and not as an implication: We will see that proving using A → P is the same as proving with the extra assumption A ⇔ P .

A rewrite system will be the combination of a term rewrite system and a proposition rewrite system. In the following, the term rewrite system used in addition to all the proposition rewrite systems we will consider is fixed. It is supposed to be terminating and confluent and is denoted R T (Σ,V ) .

We denote by P -→ R Q the fact that P can be rewritten to Q in the rewrite system R in one step. R may be omitted if it is clear from the context.

+ -→ R (resp. * -→ R
) is the transitive (resp. reflexive transitive) closure of this rewrite relation.

The subformula relation ≻ is the least transitive relation such that:

• P ≻ P i (i = 1, 2) if P = P 1 ∧ P 2 , P = P 1 ∨ P 2 or P = ¬P 1 ; • P ≻ {t/x}Q if P = ∀x. Q or P = ∃x. Q; • P ≻ Q if P -→ R T (Σ,V )
Q for all terms t, variables x and propositions P, Q, P 1 , P 2 . It is well-founded: the lexicographic combination of the comparison of the number of connectors and quantifiers in the propositions and the relation -→

R T (Σ,V ) contains ≻: if P ≻ Q,
then either P contains more connectors and quantifier than Q (R T (Σ,V ) rewrites only terms, so it cannot add connectors or quantifiers), or as much and in that case

P + -→ R T (Σ,V )
Q. As we know that R T (Σ,V ) terminates, the lexicographic combination is well founded. Note that this is not the subformula relation that we are talking about in Footnote 2: for the subformula property to hold we need to also include proposition rewriting, in which case the wellfoundedness may be lost even for terminating rewrite systems (for instance for A(c) → ∃x. A(x)).

Sequent Calculi Modulo

Sequent calculi modulo can be seen as extensions of the sequent calculus of Gentzen [START_REF] Gentzen | Untersuchungen über das logische Schliessen[END_REF]. We will use the denominations of Gallier [START_REF] Gallier | Logic for Computer Science: Foundations of Automatic Theorem Proving[END_REF]. There exist several variations of sequent calculi modulo, depending on whether rewrite steps are explicit or not, or whether they are applied to atomic propositions only or not. We propose here two variants, the unfolding sequent calculus and the polarized unfolding sequent calculus. We link them with other variants defined by Dowek [START_REF] Dowek | Confluence as a Cut Elimination Property[END_REF][START_REF] Dowek | What Is a Theory?[END_REF].

A sequent is a pair of multisets of propositions Γ, ∆. It is denoted by Γ ⊢ ∆. The sets of all sequents is denoted S. For a sequent Γ ⊢ ∆, if x 1 , . . . , x n are the free variables of Γ, ∆, we denote P(Γ ⊢ ∆) the proposition ∀x 1 , . . . , x n . ( Γ ⇒ ∆).

In Fig. 1 we present the inference rules of the unfolding sequent calculus, which is an extension of the system G4 of Kleene [START_REF] Kleene | Mathematical Logic[END_REF] with unfolding rules that apply a rewrite rule to an atomic proposition. Proofs are trees labeled by sequents built using these rules, and where all leaves are Axioms. The root sequent is called the conclusion. In the following, a double horizontal bar will mean several applications of an inference rule. A proof is said to be built in the proposition rewrite system R if all ↑-l and ↑-r steps use only rules that appear in R ∪ R T (Σ,V ) .

Identity Group:

Γ, P ⊢ P, ∆ Axiom(P ) Γ, P ⊢ ∆ Γ ⊢ P, ∆ Γ ⊢ ∆ Cut(P )
Logical Rules:

Γ ⊢ P, ∆ Γ, ¬P ⊢ ∆ ¬-l Γ, P ⊢ ∆ Γ, ∃x. P ⊢ ∆ ∃-l Γ ⊢ ∃x. P, {t/x}P, ∆ Γ ⊢ ∃x. P, ∆ ∃-r
In ∀-l and ∃-r, t ∈ T (Σ, V ); in ∃-l and ∀-r, y is not free in Γ, ∆.

Unfolding Rules: Cut(P ) permits essentially to extend the proof search space with the proposition P . Logical Rules decompose some proposition which is called principal. Unfolding Rules, that do not appear in Gentzen's sequent calculus, introduce proposition rewriting into the proof system. They are parametrized by a rewrite rule. Note that only atomic propositions are rewritten, in one step. It can also be remarked that the Unfolding Rules contain an implicit contraction. This is needed to prove that contractions are admissible in the Cut-free Unfolding Sequent Calculus (see Lemma 5 below), even when the rewrite system is confluent, as shown by proving A modulo the rule A → A ⇒ B.

A -→ {r} P , A atomic: Γ, A, P ⊢ ∆ Γ, A ⊢ ∆ ↑-l(r) Γ ⊢ A, P, ∆ Γ ⊢ A, ∆ ↑-r(r)
Definition 1 (Cut admissibility). A proposition rewrite system R is said to admit Cut if for all sequents s ∈ S, s has a proof in R if and only if s has a proof in R without using Cut.

It is well-known (Gentzen's Hauptsatz [START_REF] Gentzen | Untersuchungen über das logische Schliessen[END_REF], or more accurately [START_REF] Dowek | Confluence as a Cut Elimination Property[END_REF]Proposition 8] because of R T (Σ,V ) ) that ∅ admits Cut.

The unfolding sequent calculus is slightly different from the asymmetric sequent calculus modulo of Dowek [START_REF] Dowek | Confluence as a Cut Elimination Property[END_REF], which consists in applying identity and logical rules modulo the rewrite system. For instance, it contains the following inference rules

Γ, P ⊢ Q, ∆ Axiom P * -→ R * ←-Q Γ, Q ⊢ ∆ Γ ⊢ P, ∆ Γ, R ⊢ ∆ ⇒ -l R * -→ P ⇒Q .
The asymmetric sequent calculus modulo also contains explicit contraction and weakening inference rules. Unfolding sequent calculus is to the asymmetric sequent calculus modulo what natural deduction with folding/unfolding rules is to natural deduction modulo (see [START_REF] Dowek | About folding-unfolding cuts and cuts modulo[END_REF]). We will show that they are equivalent, in particular w.r.t. Cut.

From a logical point of view, deduction modulo is not problematic, because proving in a rewrite system R is the same as proving using some set of first-order axioms, which is then called compatible [see 4, Proposition 1.8]. In particular, a compatible axiom for the rewrite rule A → P is the proposition ∀x 1 , . . . , x n . A ⇔ P where x 1 , . . . , x n are the free variables of A. To be able to do the same with implications instead of equivalences, Dowek [START_REF] Dowek | Polarized resolution modulo[END_REF][START_REF] Dowek | What Is a Theory?[END_REF] introduced the polarized sequent calculus modulo. In this, rewrite rules are distinguished by a (positive or negative) polarity written on the arrow of the rule. A polarity is also defined for the positions of propositions: the root is positive, and we switch polarity under ¬ and at the left of ⇒. A proposition is positively rewritten if it is rewritten by a positive rule at a positive position, or by a negative rule at a negative position. A proposition is negatively rewritten if it is rewritten by a negative rule at a positive position, or by a positive rule at a negative position. The polarized sequent calculus is similar to the asymmetric calculus modulo, but propositions on the right of a sequent can only be positively rewritten, and propositions on the left only negatively. Term rewrite rules can be indifferently applied to the left or the right. We will denote by PRR the set of all polarized rewrite rules.

If we try to do the same with the unfolding sequent calculus, we simply have to restrain ↑-l to negative rules, and ↑-r to positive rules. We obtain that way what we call the polarized unfolding sequent calculus. The set of proof of the polarized unfolding sequent calculus is denoted by PUSC. We show now that it is equivalent to the polarized sequent calculus modulo.

First, we show that weakening and contraction are admissible in the polarized unfolding sequent calculus.

Lemma 2 (Weakening Lemma). For all proposition rewrite system R, if there exist a proof of Γ ⊢ ∆ in R, then for all propositions P there exists proofs of Γ, P ⊢ ∆ and Γ ⊢ P, ∆ in R of the same size.

Proof. By induction on the proof, P can be propagated in the first proof until Axioms, which accept side propositions.

Lemma 3 (Kleene Lemma [11,Lemme 3.3]). If a sequent, containing the non-atomic proposition P , has a proof (resp. Cut-free proof ) in R, then it has a proof (resp. Cut-free proof ) in R whose first rule is a logical rule with principal proposition P .

Proof. This is slightly more general than Hermant [START_REF] Hermant | Méthodes Sémantiques en Déduction Modulo[END_REF]Lemme 3.3], because we also consider ∀-l and ∃-r. But, for instance, if there is a proof Γ, ∀x. P ⊢ ∆, by weakening there is a proof of the same size of Γ, ∀x. P, {t/x}P ⊢ ∆. The lemma can be proved by simple induction on the size of the proof.

Corollary 4. For all sequents Γ ⊢ ∆, the sequent ⊢ P(Γ ⊢ ∆) has a Cut-free proof in R iff the sequent Γ ⊢ ∆ has one.

Note. It should be remarked that all inference rules r but ∀-l and ∃-r (even ↑-l and ↑-r) can be permuted from above, in the sense that if there is an application of r above some other inference rule r' that do not decompose a principal proposition into the principal proposition of r, then we can build a valid proof by permuting the inference rules, applying therefore r' above r. This can also be proved by induction on the proof.

Lemma 5 (Contraction Lemma). For all proposition rewrite system R, the two following statements hold:

• There exist a proof of Γ, P ⊢ ∆ in R if and only if there exists a proof of Γ, P, P ⊢ ∆ in R.

• There exist a proof of Γ ⊢ P, ∆ in R if and only if there exists a proof of Γ ⊢ P, P, ∆ in R.

Proof. One direction is a direct corollary of the Weakening Lemma.

The other one is a consequence of Kleene's Lemma, and can be proved by lexicographic induction on the structure of the proposition P and the size of the proof of Γ, P, P ⊢ ∆.

In the case of an atomic proposition A: suppose there exists a proof of Γ, A, A ⊢ ∆. If the principal proposition of the last inference rule is not one of the A, then by we can just apply the induction hypothesis to the subproof. If the last inference rule is Axiom, we can prune one of the A in it. The resulting proof has the same size. If the last inference rule is ↑-l for some rewrite rule A → -P , then we have a strictly smaller proof of Γ, A, A, P ⊢ ∆ to which we can apply the induction hypothesis to get a proof of Γ, A, P ⊢ ∆. Apply ↑-l to this proof gives a proof of Γ, A ⊢ ∆.

In the case of ∨: suppose there exists a proof of Γ, P ∨ Q, P ∨ Q ⊢ ∆. By Kleene's Lemma there exist proofs of Γ, P, P ∨ Q ⊢ ∆ and Γ, Q, P ∨ Q ⊢ ∆. We can apply Kleene Lemma twice again to get proofs of Γ, P, P ⊢ ∆; Γ, Q, P ⊢ ∆; Γ, P, Q ⊢ ∆ and Γ, Q, Q ⊢ ∆. By induction hypothesis, we have proofs of Γ, P ⊢ ∆ and Γ, Q ⊢ ∆, and therefore a proof of Γ, P ∨ Q ⊢ ∆.

In the case of ∃: suppose there exists a proof of Γ, ∃x. Q, ∃x. Q ⊢ ∆. By applying Kleene's Lemma twice there exists a proof of Γ, {y/x}Q, {y ′ /x}Q ⊢ ∆ where y and y ′ are not free in Γ, ∆. Then, we can replace y ′ by y in this proof to get a valid proof of Γ, {y/x}Q, {y/x}Q ⊢ ∆. By induction hypothesis, there exists a proof of Γ, {y/x}Q ⊢ ∆ where y is not free in Γ and ∆. Therefore we have a proof of Γ, ∃x. Q ⊢ ∆.

In the case of ∀: we proceed by induction on the proof of Γ, ∀x. Q, ∀x. Q ⊢ ∆. If no ∀x. Q is the principal proposition of the last rule, this is a simple induction. If it is principal, the direct subproof proves Γ, {t/x}Q, ∀x. Q, ∀x. Q ⊢ ∆ for some t ∈ T (Σ, V ). By induction hypothesis, we have a proof of Γ, {t/x}Q, ∀x. Q ⊢ ∆, and therefore a proof of Γ, ∀x. Q ⊢ ∆.

Note. The premises Γ and conclusions ∆ of sequent Γ ⊢ ∆ can therefore be considered as sets.

Lemma 6 (Rewrite Lemma). For all proposition rewrite systems R 1 and R 2 , the two following statements hold:

• If P * -→ R1∪R T (Σ,V ) Q negatively and there exists a proof of Γ, Q ⊢ ∆ in R 2 ,
then there exists a proof of

Γ, P ⊢ ∆ in R 1 ∪ R 2 . • If P * -→ R1∪R T (Σ,V )
Q positively and there exists a proof of

Γ ⊢ Q, ∆ in R 2 ,
then there exists a proof of

Γ ⊢ P, ∆ in R 1 ∪ R 2 .
Proof. We proceed by induction on the length of the rewrite derivation P * -→

R1∪R T (Σ,V ) Q.
We therefore only have to show it for a single step of rewriting.

If P -→

R1∪R T (Σ,V )
Q negatively, then there exists some context C[], an atomic proposition A and a proposition

Q ′ such that P = C[A] and Q = C[Q ′ ] and A -→ R1∪R T (Σ,V )
Q ′ negatively if the position of the hole in the context is positive or positively in the other case. We proceed by induction on the context. Suppose there exists a proof of Γ, C[Q ′ ] ⊢ ∆. We can transform it into a proof of Γ, C[A] ⊢ ∆ by applying the same inference rules, except when these rules are directly applied to Q ′ , because it is replaced by A. In this case, if the hole in C[] is at a positive position, then A is on the left of the sequent, and we can apply ↑-l (the rewrite rule that rewrites A into Q ′ is indeed negative in that case). In the other case, it is on the right and we can apply ↑-r (the rewrite rule is indeed positive). We can then carry on the proof. The resulting proof uses then rewrite rules in

R 1 ∪ R 2 ∪ R T (Σ,V ) , and is thus in R 1 ∪ R 2 .
The second sentence is dual.

Note that in all the previous lemmata, we do not introduce extra Cuts in the resulting proofs. This allows to prove the equivalence with the polarized sequent calculus modulo, also w.r.t. Cut-free proofs. [START_REF] Dowek | What Is a Theory?[END_REF], that is, a sequent is provable (resp. provable without Cut) in the polarized unfolding sequent calculus in a proposition rewrite system R iff it is provable (resp. provable without Cut) in the polarized sequent calculus modulo the rewrite system R ∪ R T (Σ,V ) .

Proposition 7 (Equivalence). The polarized unfolding sequent calculus is equivalent to the polarized sequent calculus modulo of Dowek

Proof. It is quite clear that the inference rules of the polarized unfolding sequent calculus can be derived in Dowek's one, by integrating each unfolding step into the inference rules above through the modulo.

Conversely, using Lemma 6, we can extract the rewriting from the logical rules. For instance, if we have a proof whose root is

Γ, Q ⊢ ∆ Γ ⊢ P, ∆ Γ, O ⊢ ∆ ⇒ -l O * -→ P ⇒Q negatively ,
we use the premises to get a proof Γ, P ⇒ Q ⊢ ∆ without implicit rewriting, and we use Lemma 6 to get the proof of Γ, O ⊢ ∆. Then, Lemmata 2 and 5 proves that weakening and contraction are admissible.

Of course, as we have seen, both system are also equivalent regarding Cutfree proofs, since we did not need to add any Cut in the proofs of the previous lemmata.

Corollary 8. The unfolding sequent calculus is equivalent (in the same sense) to the asymmetric sequent calculus modulo.

Proof. A non-polarized rewrite system R can easily be seen as a polarized rewrite system R ± with for each rule A → P in R a positive rule A → + P and a negative rule A → -P . The unfolding sequent calculus for R (resp. the asymmetric sequent calculus modulo for R) is then the polarized unfolding sequent calculus for R ± (resp. the polarized sequent calculus modulo for R ± ).

This translation also permits to know that every lemma above holds also for the unfolding sequent calculus.

Given a polarized rewrite system R, we can transform it into a non-polarized rewrite system R ∓ :

• a positive rule A → + P is translated into A → A ∨ P ; • a negative rule A → -P is translated into A → A ∧ P .
The polarized unfolding sequent calculus for R is then equivalent to the unfolding sequent calculus for R ∓ : Proposition 9. A sequent is provable (resp. provable without Cut) in the polarized unfolding sequent calculus in a polarized proposition rewrite system R iff it is provable (resp. provable without Cut) in the unfolding sequent calculus in the rewrite system R ∓ .

Proof. By induction on the structure of the proofs. Only the cases with unfolding rules are interesting.

If we have a proof ending with

Γ, σA, σP ⊢ ∆ Γ, σA ⊢ ∆ ↑-l(A → -P )
then by induction hypothesis we have a proof of Γ, σA, σP ⊢ ∆ in the unfolding sequent calculus. Using Lemma 2, and applying ∧-l we obtain a proof of Γ, σA, σA ∧ σP ⊢ ∆. We therefore can build the derivation

Γ, σA, σA, σP ⊢ ∆ Γ, σA, σ(A ∧ P ) ⊢ ∆ ∧-l Γ, σA ⊢ ∆ ↑-l(A → A ∧ P )
in the unfolding sequent calculus. This is dual for the polarized ↑-r.

Conversely, there are two cases: either the rewrite rule is applied on the side corresponding to the polarity of the polarized rule that produced it, or on the other side. In the first case, suppose for instance that we have the proof

π . . . . Γ ⊢ σ(A ∨ P ), σA, ∆ Γ ⊢ σA, ∆ ↑-r(A → A ∨ P ) .
By induction hypothesis on π we have a proof of Γ ⊢ σ(A ∨ P ), σA, ∆ in the polarized unfolding sequent calculus. By Lemmata 3 and 5, we have a proof of Γ ⊢ σP, σA, ∆. Because σA -→

A→ + P
σP positively, we can apply ↑-r to get a proof of Γ ⊢ σA, ∆. In the second case, suppose for instance that we have the proof

π . . . . Γ, σA, σ(A ∨ P ) ⊢ ∆ Γ, σA ⊢ ∆ ↑-l(A → A ∨ P ) .
By induction hypothesis on π we have a proof of Γ, σA, σ(A ∨ P ) ⊢ ∆ in the polarized unfolding sequent calculus. By Lemmata 3 and 5, we have a proof of Γ, σA ⊢ ∆.

Corollary 10. The polarized sequent calculus modulo and the asymmetric sequent calculus modulo are equivalent.

This somehow answers a question of Dowek [15, end of Section 4] who asked which polarized rewrite system can be represented as a non-polarized rewrite system. We can also prove the equivalence for intuitionistic logic, with the same translation. To be able to do this, one needs a multi-conclusion sequent calculus for intuitionistic logic, see [START_REF] Burel | Automating Theories in Intuitionistic Logic[END_REF] (the translation is in the appendix of the full version of that paper, available at http://hal.inria.fr/inria-00395934).

However, the non-polarized system is not necessarily confluent, and therefore, we may not have the equivalence with the original sequent calculus modulo of Dowek et al. [START_REF] Dowek | Theorem Proving Modulo[END_REF], at least concerning Cut admissibility. Nevertheless, this should not be a problem. Indeed, the proving procedures based on deduction modulo, TaMed and ENAR, are actually complete for the cut-free part of the asymmetric sequent calculus modulo, regardless of the confluence of the rewrite system.

Undecidability of the cut admissibility

We present here some properties of the unfolding sequent calculus, which are slight generalizations of Hermant [START_REF] Hermant | Méthodes Sémantiques en Déduction Modulo[END_REF][START_REF] Hermant | A Model-based Cut Elimination Proof[END_REF]. In particular, we introduce the notion of semantically sound rewrite systems, which implies Cut admissibility, and we prove that the Cut admissibility is not decidable.

We need the following definitions, whose motivations can be found in Hermant [START_REF] Hermant | A Model-based Cut Elimination Proof[END_REF]:

Definition 11 (Properties of a theory). Given a rewrite system R, a theory Γ:

• is complete iff for all propositions P , either Γ, P ⊢ or Γ ⊢ P has a Cut-free proof in R;

• is consistent iff there is no Cut-free proof of Γ ⊢ in R;

• admits Henkin witnesses iff for all propositions Q with one free variable x, there is a constant c of the language such that

-if Γ, ∃x. Q ⊢ has no Cut-free proof in R, then {c/x}Q is in Γ; -if Γ ⊢ ∀x. Q has no Cut-free proof in R, then ¬{c/x}Q is in Γ.
Models in deduction modulo are standard first-order models, except that they are compatible with the rewrite system: Definition 12 (Model for a rewrite system). A Boolean model M is a model for the rewrite system R if for all rewrite rules A → P in R, A and P are interpreted the same way in M.

We introduce the new notion of semantically sound rewrite system: Definition 13 (Semantical soundness). A rewrite system R is said semantically sound if every complete, consistent theory Γ which admits Henkin witnesses has a model M for R.

Proposition 14 (Semantical soundness implies Cut admissibility). If R is semantically sound, then R admits Cut.

Proof. As proved by Hermant [START_REF] Hermant | A Model-based Cut Elimination Proof[END_REF]Lemma 3], if Γ ⊢ ∆ has a proof in R, then any model M for R interprets P(Γ ⊢ ∆) as true.

It remains to be proved that if any model M for R interprets P(Γ ⊢ ∆) as true then Γ ⊢ ∆ has a Cut-free proof in R.

If ¬P(Γ ⊢ ∆) is consistent, then using Hermant [27, Section 6.1], we can complete it into a consistent, complete theory Θ which admits Henkin witnesses. By hypothesis (semantical soundness), Θ has a model M for R. Furthermore, by construction of Θ this model is also a model for ¬P(Γ ⊢ ∆). Consequently, this model for R does not interpret P(Γ ⊢ ∆) as true, which contradicts our hypothesis.

Hence ¬P(Γ ⊢ ∆) is not consistent, by definition there is a Cut-free proof of ¬P(Γ ⊢ ∆) ⊢ in R, and using Lemma 3 there is a Cut-free proof of Γ ⊢ ∆. This proposition permits to prove the main theorem of this first section:

Theorem 15 (Undecidability of the Cut Admissibility). The problem

Input: A propositional rewrite system R Decide if R admits Cut. is undecidable.
Proof. We reduce to the validity problem in first-order logic (given a proposition, decide whether it is valid in all first-order models). We recall the reader that this problem is undecidable in the empty theory when the language contains at least a binary predicate.

Let P be a first-order proposition.

Let A be a nullary predicate not appearing in P . Consider the propositional rewrite system

R = { A → A ⇒ P } .
It is always possible to build a proof of ⊢ P in R:

A, P ⊢ P Axiom A ⊢ A, P Axiom A, A ⇒ P ⊢ P ⇒ -l A ⊢ P ↑-l A ⊢ P, A, P Axiom ⊢ A ⇒ P, A, P ⇒ -r ⊢ A, P ↑-r ⊢ P Cut(A)
Then we show that P is valid if and only if R admits Cut: If P is valid, then R is semantically sound: given a complete, consistent theory Γ which admits Henkin witnesses, let M be the model defined as follows: Its domain is the set of closed terms. An atomic predicate B is interpreted as true by M iff Γ ⊢ B has a Cut-free proof in R. Because the theory is complete and because it admits Henkin witnesses, this permits to define the model for all propositions [see 27, Lemma 8]. This process is well-defined by consistency. Then ⊢ A has a Cut-free proof (the right part of the proof above where P is pruned). By weakening Γ ⊢ A has a Cut-free proof in R, and A is therefore interpreted as true by M. As P is valid, it is interpreted as true in particular in M. Consequently, the interpretation of A ⇒ P is also true. Thus, the left-hand side and the right-hand side of the rules in R have the same interpretation in M, which is therefore a model for R. Consequently, R is semantically sound and by Proposition 14 it admits Cut.

Conversely, if R admits Cut, because of the existence of the proof above, there exists a Cut-free proof of ⊢ P in R. Because P does not contain A, no unfolding rules can be applied in this proof (simple proof by induction). Therefore, there exists a proof of ⊢ P in Gentzen's sequent calculus, and as it is complete for first-order logic, P is valid.

Note. This proof is deeply inspired by the proof of Hermant [START_REF] Hermant | Méthodes Sémantiques en Déduction Modulo[END_REF]Chapter 8] that there exists terminating and confluent rewrite systems that admits Cut, but in which some proof is not normalizing. Cut admissibility remains undecidable even when considering only terminating and confluent rewrite system, by using the system r ∈ r → ∀y. (∀x. y ∈ x ⇒ r ∈ x) ⇒ y ∈ r ⇒ P in the proof above.

Note. In fact, this problem seems to be Π 0 2 -complete in the arithmetical hierarchy (see [START_REF]Handbook of Mathematical Logic[END_REF]Chapter C.1] for an introduction on the arithmetical hierarchy), i.e. it is not even semi-decidable. This could be proved by merging the proof above with techniques used in [START_REF] Endrullis | Degrees of Undecidability in Term Rewriting[END_REF] to prove in particular that the confluence of a rewrite system is Π 0 2 -complete.

Construction of a rewrite system compatible with a theory

We now present an algorithm transforming a finitely presented first-order theory into a polarized rewrite system such that, proving in the theory is equivalent to proving modulo the rewrite system. We first define the good properties that such an algorithm should have, and then provide an example of such an algorithm.

Desired properties

We want to build an algorithm that translates a finite presentation of a firstorder theory into a rewrite system. This algorithm may be seen as a function from sequents to polarized rewrite systems: Rew : S → PRR.

First, we require that each polarized rewrite rule can be produced by the algorithm. This is not really useful here, but we need this for the completion procedure in the next section.

Property 16. For all polarized rewrite rule r there exists a sequent s such that Rew(s) = {r}.

Then we want that the theory is compatible with the rewrite system produced from it. Moreover, we would like that at least the axioms in the presentation of the theory are provable without Cut in the produced rewrite system.

Property 17 (Strong Compatibility). For all sequents Γ ⊢ ∆, Rew(Γ ⊢ ∆) and P(Γ ⊢ ∆) are strongly compatible:

(a) for all positive rewrite rule A → + P in Rew(Γ ⊢ ∆), there exists a proof of P(Γ ⊢ ∆) ⊢ P ⇒ A in ∅ (i.e. using only term rewrite rules of R T (Σ,V ) ); (b) for all negative rewrite rule A → -P in Rew(Γ ⊢ ∆), there exists a proof of

P(Γ ⊢ ∆) ⊢ A ⇒ P in ∅ (i.e. using only term rewrite rules of R T (Σ,V ) ); (c) there exists a Cut-free proof of ⊢ P(Γ ⊢ ∆) in Rew(Γ ⊢ ∆).
Property 17 is a stronger notion than the compatibility in the sense of Definition 1.4 of Dowek et al. [START_REF] Dowek | Theorem Proving Modulo[END_REF]: it imposes Cut-free proof in (c) and it does not care about term rewrite rules. Property 17(a) and 17(b) implies the following:

Proposition 18. For all sequents Γ ⊢ ∆, for all rewrite systems R, if there is a proof of a sequent Γ ′ ⊢ ∆ ′ in the rewrite system Rew(Γ ⊢ ∆) ∪ R, there is a proof of P(Γ ⊢ ∆), Γ ′ ⊢ ∆ ′ in R.
Proof. We prove it by induction on the proof of Γ ′ ⊢ ∆ ′ . The only interesting case is when the last inference rule is an unfolding rule. If it is ↑-l with a rule in Rew(Γ ⊢ ∆) \ R, we have . . . .

Γ ′ , A, P ⊢ ∆ ′ Γ ′ , A ⊢ ∆ ′ ↑-l(B → -Q) with B → -Q in Rew(Γ ⊢ ∆
) and A = σB, P = σQ for some substitution σ. By induction hypothesis, there exists a proof

π of P(Γ ⊢ ∆), Γ ′ , A, P ⊢ ∆ ′ in ∅. By Property 17(b), there is a proof ̟ of P(Γ ⊢ ∆) ⊢ B ⇒ Q in ∅. We can apply σ to ̟ to get a valid proof ̟ ′ of P(Γ ⊢ ∆) ⊢ A ⇒ P .
We can therefore build the proof π . . . .

P(Γ ⊢ ∆), Γ ′ , A, P ⊢ ∆ ′ P(Γ ⊢ ∆), Γ ′ , A ⊢ A, ∆ ′ Axiom P(Γ ⊢ ∆), Γ ′ , A, A ⇒ P ⊢ ∆ ′ ⇒ -l ̟ ′ P(Γ ⊢ ∆), Γ ′ , A ⊢ ∆ ′ Cut(A ⇒ P ) which is indeed in R.
The case of ↑-r is very similar.

The next property will also be useful for the completion procedure. It essentially says that Rew should be modular, i.e. for all sequents s, s 1 , s 2 , if Rew(s) = Rew(s 1 ) ∪ Rew(s 2 ) then having a cut-free proof of s 1 and s 2 implies having a cut-free proof of s, whatever the rewrite system used in the modulo.

Property 19. For all proposition rewrite system R, for all sequents s, if for all rewrite rules r ∈ Rew(s) there exists a sequent s r which is provable without Cut in R and such that r ∈ Rew(s r ), then s has a Cut-free proof in R.

An Algorithm . . .

We now present one possible algorithm having the required properties. It is quite simple to describe: it consists in applying rules of the sequent calculus to the sequent until an atomic proposition appears in the sequent. This atomic proposition will be the left-hand side of the polarized rewrite rule, the polarity of the rule will depend on the side of the sequent in which A appears, and the right-hand side will contain all other propositions.

More precisely, the algorithm can be described by the non-deterministic steps below. To decompose universally quantified propositions on the left and existentially quantified propositions on the right only once, we mark that they have already been decomposed by underlining them. Step 2. Decompose the last proposition iteratively:

P 1 , . . . , P n ⊢ Q 1 , . . . , Q m becomes P 1 , . . . , P n , ¬Q 1 , . . . , ¬Q m-1 ⊢ Q m P 1 , . . . , P n ⊢ Q 1 ∧ Q 2 " P 1 , . . . , P n ⊢ Q 1 ; P 1 , . . . , P n ⊢ Q 2 P 1 , . . . , P n ⊢ Q 1 ∨ Q 2 " P 1 , . . . , P n , ¬Q 1 ⊢ Q 2 P 1 , . . . , P n ⊢ Q 1 ⇒ Q 2 " P 1 , . . . , P n , Q 1 ⊢ Q 2 P 1 ,
⇒ P 2 ⊢ Q 1 , . . . , Q m becomes P 2 ⊢ Q 1 , . . . , Q m ; ¬P 1 ⊢ Q 1 , . . . , Q m ∀x. P ⊢ Q 1 , . . . , Q m " {t/x}P ⊢ ¬∀x. P , Q 1 , . . . , Q m where t can be any term A ⊢ Q 1 , . . . , Q m " A → -∀x 1 , . . . , x p . (Q 1 ∨ • • • ∨ Q m ) (A atomic, and the x i are the free variables appearing in Q 1 , . . . , Q m but not in A) for ¬P ⊢ Q 1 , . . . , Q m , return to Step 1.
In practice, we can for instance choose x for t, so that no substitution is needed in those cases. All other choices are also correct. Of course, at the end, the underlines are removed.

This algorithm clearly terminates, because each times a step 2 or 3 begins, either a rewrite rule is generated, or a proposition is decomposed into subformulae, so that the number of connectors in the non-underlined propositions in a sequent different from ¬ strictly diminishes. Of course, we do not pretend that this algorithm is the most optimized for our purpose.

We denote Rew(Γ ⊢ ∆) the function returning the rewrite system obtained by applying the algorithm to Γ ⊢ ∆ .

To get an intuition on this algorithm, it may be seen as the attempt to build a Cut-free proof of a sequent, adding rewrite rules to close the branches where an atomic proposition appears.

. . . with the Good Properties

We first prove Property 17 using three lemmata.

Lemma 20. If the sequent Γ ⊢ ∆ is transformed to the set of sequents {Γ ′ ⊢ ∆ ′ }∪ S ′ by the algorithm described in Section 4.2, then the sequent

P(Γ ⊢ ∆) ⊢ P(Γ ′ ⊢ ∆ ′ )
can be proved (without proposition rewrite rules).

Proof. By case analysis on the transformation. For instance, in Step 2, P 1 , . . . , P n ⊢ Q 1 ∧Q 2 is transformed into P 1 , . . . , P n ⊢ Q 1 ; P 1 , . . . , P n ⊢ Q 2 . Suppose x 1 , . . . , x n (resp. y 1 , . . . , y m ) are the free variables of P 1 , . . . , P n , Q 1 ∧Q 2 (resp.P 1 , . . . , P n , Q 1 ). {y 1 , . . . , y m } ⊆ {x 1 , . . . , x n } so that we can suppose y i = x i for i ∈ {1, . . . , m}. We have the following proof (only relevant propositions are written, and the substitutions are forgotten in the above part of the proof):

Q 1 , Q 2 ⊢ Q 1 Axiom Q 1 ∧ Q 2 ⊢ Q 1 ∧-l i P i ⊢ i P i Axiom i P i ⇒ (Q 1 ∧ Q 2 ), i P i ⊢ Q 1 ⇒ -l i P i ⇒ (Q 1 ∧ Q 2 ) ⊢ i P i ⇒ Q 1 ⇒ -r ∀x 1 , . . . , x n . ( i P i ⇒ (Q 1 ∧ Q 2 )) ⊢ ( i P i ⇒ Q 1 ) ∀-l ∀x 1 , . . . , x n . ( i P i ⇒ (Q 1 ∧ Q 2 )) ⊢ ∀y 1 , . . . , y m . ( i P i ⇒ Q 1 ) ∀-r
It can be checked that the side conditions of the rules ∃-l and ∀-r are verified.

Lemma 21. For all propositions A, P 1 , . . . , P n , if x 1 , . . . , x p are the free variables of P 1 , . . . , P n not appearing freely in A, then the sequents

P(P 1 , . . . , P n ⊢ A) ⊢ (∃x 1 , . . . , x p . i P i ) ⇒ A P(A ⊢ P 1 , . . . , P n ) ⊢ A ⇒ ∀x 1 , . . . , x p . i P i
can be proved (without proposition rewrite rules).

Proof. Suppose y 1 , . . . , y m are the free variables of A, P 1 , . . . , P n . Note that {x 1 , . . . , x p } ⊆ {y 1 , . . . , y m } so that we can suppose y i = x i for i ∈ {1, . . . , p}.

We can construct the following proof (only relevant propositions are written):

A ⊢ A Axiom i P i ⊢ i P i Axiom ( i P i ⇒ A), i P i ⊢ A ⇒ -l ∀y 1 , . . . , y m . ( i P i ⇒ A), i P i ⊢ A ∀-l ∀y 1 , . . . , y m . ( i P i ⇒ A), ∃x 1 , . . . , x p . i P i ⊢ A ∃-l ∀y 1 , . . . , y m . ( i P i ⇒ A) ⊢ (∃x 1 , . . . , x p . i P i ) ⇒ A ⇒ -r
The proof of the other sequent is dual.

Note that although the proofs given by Lemmata 20 and 21 are Cut-free, we will need Cuts to link them and prove Properties 17(a) and 17(b).

Lemma 22. For all atomic propositions A and propositions P 1 , . . . , P n , if x 1 , . . . , x p are the free variables of P 1 , . . . , P n not appearing freely in A, then we can prove without Cut the sequent ⊢ P(P 1 , . . . , P n ⊢ A) in the rewrite system consisting of the rule A → + ∃x 1 , . . . , x p .

(P 1 ∧ • • • ∧ P n ),
and the sequent ⊢ P(A ⊢ P 1 , . . . , P n ) in the rewrite system consisting of the rule A → -∀x 1 , . . . , x p .

(P 1 ∨ • • • ∨ P n ).
Proof. Suppose y 1 , . . . , y m are the free variables of A, P 1 , . . . , P n . Note that {x 1 , . . . , x p } ⊆ {y 1 , . . . , y m } so that we can suppose y i = x i for i ∈ {1, . . . , p}.

Because x 1 , . . . , x p do not appear in A, {t i /y i }A = {t i /y i : i > p}A. Only relevant propositions are written:

P 1 ⊢ P 1 Axiom • • • P n ⊢ P n Axiom P 1 , . . . , P n ⊢ A, P 1 ∧ • • • ∧ P n ∧-r i P i ⊢ A, P 1 ∧ • • • ∧ P n ∧-l i P i ⊢ A, ∃x 1 , . . . , x p . (P 1 ∧ • • • ∧ P n ) ∃-r i P i ⊢ A ↑-r ⊢ i P i ⇒ A ⇒ -r ⊢ ∀y 1 , . . . , y m . ( i P i ⇒ A) ∀-r
We can prove Property 19 using the following lemma:

Lemma 23. For all proposition rewrite system R, if the set of sequents S is transformed into the set of sequents S ′ by the algorithm of Section 4.2 without the production of a rewrite rule, then all sequents of S have a (resp. Cut-free) proof in R iff all sequents of S ′ have a (resp. Cut-free) proof in R.

Proof. By case analysis on the transformation. The "if" part is the application of logical rules, whereas the "only if" part is a consequence of Lemma 3.

For instance, P 1 , . . . , P n ⊢ ∀x. Q is transformed into P 1 , . . . , P n ⊢ {y/x}Q where y does not appear in P 1 , . . . , P n . If P 1 , . . . , P n ⊢ {y/x}Q has a proof in R, then because y does not appear in P 1 , . . . , P n , P 1 , . . . , P n ⊢ ∀x. Q has a proof in R by application of ∀-r. Conversely, if P 1 , . . . , P n ⊢ ∀x. Q has a proof in R, then by Lemma 3 there exists a proof of P 1 , . . . , P n ⊢ {y/x}Q in R for y not free in P 1 , . . . , P n . Therefore P 1 , . . . , P n ⊢ {y/x}Q has a proof in R.

In the preceding paragraph, if proofs are supposed Cut-free, then the resulting proofs have the same property.

We can now prove the main result of this subsection: Proof. We proceed by induction on the execution of the algorithm of Section 4.2.

Property 16 directly follows from the fact that Rew(A ⊢ P ) = {A → -P } and Rew(P ⊢ A) = {A → + P }.

For Properties 17(a) and 17(b), Lemma 21 permits to prove the properties at the end of the algorithm, when sequents are transformed into rules. Lemma 20 permits to prove the inductive case: suppose Γ ⊢ ∆ is transformed into {Γ ′ ⊢ ∆ ′ }∪• • • . Suppose P(Γ ′ ⊢ ∆ ′ ) ⊢ A ⇒ P has a proof π without proposition rewrite rules. By Lemma 20, there is a proof π ′ of P(Γ ⊢ ∆) ⊢ P(Γ ′ ⊢ ∆ ′ ) in ∅. Therefore, we can construct the proof π . . . .

P(Γ ⊢ ∆), P(Γ ′ ⊢ ∆ ′ ) ⊢ A ⇒ P π ′ . . . . P(Γ ⊢ ∆) ⊢ P(Γ ′ ⊢ ∆ ′ ), A ⇒ P P(Γ ⊢ ∆) ⊢ A ⇒ P Cut(P(Γ ′ ⊢ ∆ ′ ))
without proposition rewrite rules. For Property 17(c), the base case is a consequence of Lemma 22, whereas the inductive case is a consequence of Lemma 3. For instance, suppose P 1 , . . . , P n ⊢ Q 1 ∧ Q 2 is transformed into P 1 , . . . , P n ⊢ Q 1 ; P 1 , . . . , P n ⊢ Q 2 . For i ∈ {1, 2}, suppose ⊢ P(P 1 , . . . , P n ⊢ Q i ) has a Cut-free proof in some rewrite system R i . By Lemma 3, there is a Cut-free proof π i of P 1 , . . . , P n ⊢ Q i in R i . Consequently we can construct the Cut-free proof π 1 . . . .

P 1 , . . . , P n ⊢ Q 1 π 2 . . . . P 1 , . . . , P n ⊢ Q 2 ⊢ P(P 1 , . . . , P n ⊢ Q 1 ∧ Q 2 ) ∀-r, ⇒-r, ∧-l, ∧-r in R 1 ∪ R 2 .
For Property 19, using Lemma 23 by induction on the execution of the algorithm, we obtain that a sequent s is provable without Cut in a rewrite system R iff the sequents eventually producing all rules of Rew(s) are provable without Cut in R. Suppose that for all r ∈ Rew(s) there exists a sequent s r provable without Cut in R such that r ∈ Rew(s ′ ). Then the sequent producing each r can be proved without Cut in R. Therefore s can be proved without Cut in R.

Note. P(Γ ⊢ ∆) is compatible with Rew(Γ ⊢ ∆) in classical logic, but it is not true for intuitionistic logic. For instance, Rew(⊢ ∃x. B(x)) = {B(x) → + ¬∃x. B(x)}. Then, ⊢ ∃x. B(x) has the following proof in Rew(⊢ ∃x, B(x))

∃x. B(x) ⊢ ∃x. B(x), B(x) Axiom ⊢ ∃x. B(x), B(x), ¬∃x. B(x) ¬-r ⊢ ∃x. B(x), B(x) ↑-r ⊢ ∃x. B(x) ∃-r
in the classical polarized unfolding sequent calculus but it has no proof in, for instance, the polarized natural deduction of Dowek [START_REF] Dowek | What Is a Theory?[END_REF], which is an intuitionistic system. As pointed out by a referee, it is not possible to transform an axiom ∃x. B(x) into a rewrite system admitting Cut and compatible in intuitionistic logic, because the theory formed with the axiom do not enjoy the witness property, but it would using the rewrite system. Notice also that, as shown by Hermant [START_REF] Hermant | Méthodes Sémantiques en Déduction Modulo[END_REF], Cut admissibility in classical and intuitionistic logic are not equivalent in deduction modulo.

Note. It is possible that the produced rewrite system does not admit Cut.

For instance, on ⊢ A ⇔ B ∧ ¬A the algorithm returns Crabbé's system of the introduction.

As a nice consequence of the properties of Rew, we obtain a way to internalize in the congruence any first-order theory:

Corollary 25. For all finite set of formulae Γ and rewrite systems R, there exists a rewrite system R ′ such that for all finite set of formulae ∆:

Γ ⊢ ∆ is derivable in R iff ⊢ ∆ is derivable in R ′ .
Proof. Simply take R ′ = R ∪ P ∈Γ Rew(⊢ P ).

Abstract Completion for Cut Admissibility

We present in this section the completion procedure which permits to transform a rewrite system into one admitting Cut. It is based on an abstract completion procedure introduced in the framework of the Abstract Canonical Systems and Inference, that we are first presenting.

Abstract Canonical Systems and Inference

The results in this section are extracted from Dershowitz and Kirchner [START_REF] Dershowitz | Abstract Canonical Presentations[END_REF][START_REF] Dershowitz | Abstract Saturation-Based Inference[END_REF] and Bonacina and Dershowitz [START_REF] Bonacina | Abstract canonical inference[END_REF], which should be consulted for motivations, details and proofs. We define a framework with abstract notions of formulae, proofs, etc. These should not be confused with the first-order propositions and sequent-calculus proofs used before, although the framework could be instantiated with those. In Section 5.2 we will see which exact instance we will be using. In this section, to give intuitions, we will use standard completion as an example of instance, but without going into details (that can be found in Burel and Kirchner [START_REF] Burel | Completion Is an Instance of Abstract Canonical System Inference[END_REF]).

Let A be the set of all (abstract) formulae over some fixed vocabulary. Let P be the set of all (abstract) proofs. These sets are linked by two functions: [•] Pm : P → 2 A gives the premises in a proof, and [•] Cl : P → A gives its conclusion. Both are extended to sets of proofs in the usual fashion. The set of proofs built using assumptions in R ⊆ A is denoted by

Pf (R) ! = p ∈ P : [p] Pm ⊆ R .
The framework described here is predicated on two well-founded partial orderings over P: a proof ordering > and a subproof relation . They are related by a monotonicity requirement (postulate E). The proof ordering expresses the quality of proofs, whereas the subproof relation translates their structures. We assume for convenience that the proof ordering only compares proofs with the same conclusion (p > q ⇒ [p] Cl = [q] Cl ), rather than mention this condition each time we have cause to compare proofs. We will use the term presentation to mean a set of formulae, and justification to mean a set of proofs. We reserve the term theory for deductively closed presentations:

Th R ! = [Pf (R)] Cl = {[p] Cl : p ∈ P, [p] Pm ⊆ R} .
In addition to this, we assume the two following postulates:

Postulate A (Reflexivity). For all presentations R: R ⊆ Th R Postulate B (Closure). For all presentations R:

Th Th R ⊆ Th R
We call a proof trivial when it proves only its unique assumption and has no subproofs other than itself, that is, if [p] Pm = {[p] Cl } and p q ⇒ p = q, where is the reflexive closure of the subproof ordering . We denote by a such a trivial proof of a ∈ A and by R the set of trivial proofs of each a ∈ R.

Example 27. For standard completion, the trivial proof of s → t is just s -→ s→t t.

We assume that proofs use their assumptions (postulate C), that subproofs don't use non-existent assumptions (postulate D), and that proof orderings are monotonic with respect to subproofs (postulate E):

Postulate C (Trivia). For all proofs p and formulae a:

a ∈ [p] Pm ⇒ p a
Postulate D (Subproofs Premises Monotonicity). For all proofs p and q:

p q ⇒ [p] Pm ⊇ [q] Pm
Postulate E (Replacement). For all proofs p, q and r:

p q > r ⇒ ∃v ∈ Pf ([p] Pm ∪ [r] Pm ). p > v r
We make no other assumptions regarding proofs or their structure and the proof ordering > is lifted to a quasi-ordering over presentations:

R 1 R 2 if Th R 1 = Th R 2 and ∀p ∈ Pf (R 1 ). ∃q ∈ Pf (R 2 ). p ≥ q .
A normal-form proof for R will be a proof that is minimal whatever the presentation of the theory build on R, i.e. it is one of the minimal proofs of Pf (Th R):

Nf (R) ! = µPf (Th R) ! = {p ∈ Pf (Th R) : ¬∃q ∈ Pf (Th R). p > q}
Normal form proofs are the best, the one we wish we can build from our current presentation.

Example 28. For standard completion, normal proofs are valley proofs, that is, proofs of the form a * -→ * ←c.

The canonical presentation contains those formulae that appear as assumptions of normal-form proofs:

R ♯ ! = [Nf (R)] Pm .
So, we will say that R is canonical if R = R ♯ . Intuitively, the canonical presentation of R contains the formulae that are necessary to build all the best proofs of the theory of R, and only these formulae.

A presentation R is complete if every theorem has a normal-form proof:

Th R = [Pf (R) ∩ Nf (R)] Cl
Canonicity implies completeness, but the converse is not true. Intuitively, R is complete iff it contains enough to build all the theory using only its own best proofs.

Example 29. For standard completion, completeness means that every equality provable with a rewrite system can be proved with this rewrite system using a valley proof. In other words, a complete rewrite system is confluent.

We now consider inference and deduction mechanisms. A deduction mechanism is a function from presentations to presentations and we call the relation

R 1 R 2 a deduction step. A sequence of presentations R 0 R 1 • • • is called a derivation.
The result of the derivation is, as usual, its persisting formulae:

R ∞ ! = lim inf j→∞ R j = j>0 i>j R i . A deduction mechanism is completing if for each step R 1 R 2 , R 1 R 2 and the limit R ∞ is complete.
A completing mechanism can be used to build normal-form proofs of theorems of the initial presentation:

Theorem 30 (Bonacina and Dershowitz [17,Lemma 5.13

]). A deduction mechanism is completing if and only if for all derivations R

0 R 1 • • • , Th R 0 ⊆ [Pf (R ∞ ) ∩ Nf (R 0 )] Cl .
A critical proof is a minimal proof which is not in normal form, but whose strict subproofs are:

Crit (R) ! = p ∈ µPf (R) \ Nf (R) : ∀q ∈ Pf (R). p q ⇒ q ∈ Nf (R)
Intuitively, a critical proof of R is a minimal (in terms of quality and structure) counter-example that shows that R is not complete.

Example 31. For standard completion, critical proofs correspond to non-confluent critical pairs, that is, proofs a ←-

s[b]→a s[b] -→ b→c s[c] with no valley proof a * -→ * ←-s[c].
Standard completion adds the equation a = s[c] to the presentation, so that it is possible to build the smaller proof a ←→

a=s[c] s[c].
The idea to obtain a complete presentation is therefore to enhance the current presentation with formulae that permits to build proofs smaller than the critical ones. Completing formulae are then premises of proofs smaller than critical proofs:

Comp(R) ! = p ∈ Crit(R) p ′ is any proof such that p > p ′ [p ′ ] Pm
To get a completing procedure, we therefore need to add at least these proofs, and we can only add formulae that are in the theory. In this paper, given some function C from presentations to presentations such that Comp(R) ⊆ C(R) ⊆ Th R for all presentations R, the deduction mechanism is therefore:

R R ∪ C(R) .
Proposition 32 (Dershowitz and Kirchner [30,Lemma 10]). This deduction mechanism is completing.

Example 33. For standard completion, the deduction mechanism is more evolved, because there are also simplification steps. Burel and Kirchner [START_REF] Burel | Completion Is an Instance of Abstract Canonical System Inference[END_REF] give remaining details.

Deduction Modulo is an Instance of ACS

We want to show that the polarized unfolding sequent calculus can be seen as an instance of ACS. For this purpose, we have to define what the (abstract) formulae, proofs, premises and conclusions are, and to give the appropriate orderings. After this, we need to check that the postulates are verified by the defined instance.

Proofs and Formulae

We aim to obtain Cut-free proofs, so that the natural candidate for abstract proofs are polarized-unfolding-sequent-calculus proofs.

The completion procedure we want to establish deals with polarized rewrite rules over atomic propositions. Nevertheless, the conclusions of the proofs, from which we want to generate the rewrite rules added by the completion mechanism, are sequents. In other words, sequents must be related to rewrite rules. We therefore assume that we have a function Rew satisfying Properties 16, 17 and 19. Only these properties are important, so that we do not need to use the particular algorithm given in Section 4.2.

Then, ACS formulae will be polarized rewrite rules (similarly as for standard completion), and proofs will be polarized-unfolding-sequent-calculus proofs. The premises of a proof are the rewrite rules used in that proof. For the conclusion, as a sequent may be associated by Rew to several rewrite rules, we would need proofs with several conclusions. However, we can bypass this by considering several instances of a proof of Γ ⊢ ∆, one for each rules in Rew(Γ ⊢ ∆). The conclusion of a proof will therefore be this particular rule.

Orderings on Proofs

To define an ordering on proofs, we need the concept of proof skeleton:

Definition 34. The skeleton of a proof p is the tree labeled by the inference rules used p, with the active proposition in the case of Cut and Axiom.

We define the following precedence > on inference rules: for all propositions P, Q, O, if P is greater than Q for the subformula relation, then Cut(P ) > Cut(Q) and Axiom(P ) > Axiom(Q), and for all other inference rules r of Fig. 1, Cut(P ) > Axiom(O) > r. This precedence is infinite, but it is well founded because the subformula relation is.

We order the proof skeletons with the RPO [START_REF] Dershowitz | Orderings for Term-Rewriting Systems[END_REF] based on this precedence. Since the precedence is well-founded, so is the RPO [START_REF] Dershowitz | Orderings for Term-Rewriting Systems[END_REF]. We define the ordering over proofs by saying that a proof is strictly greater than another if this holds for their skeletons. This defines therefore a well-founded ordering on proofs.

We restrict this ordering to proofs which have the same conclusion. Notice that with this ordering, a Cut-free proof is always strictly smaller than a proof with at least one Cut at root. Note. To get a completion procedure producing rewrite systems admitting Cut, it should have been possible to use a coarser ordering, the essential property being that proofs with Cut are bigger than proofs without. Nevertheless, the finer the ordering is, the fewer the critical proofs are. To be able to better characterize the critical proofs, the ordering we are using seems convenient. Moreover, we use an RPO because it is a simplification ordering and Postulate E is therefore easier to prove. Subproofs of a proof p are for a part defined as the subproofs of p for the sequent calculus. We also want to say that if a proof do not use a proposition (i.e. it is the weakened version of another proof), then the strengthened proof should be smaller for the subproof relation. We therefore consider the transitive closure of the subproof ordering in the unfolding sequent calculus and this "weakening" ordering.

Definition 35. We say that π sp π ′ iff π ′ is a strict subproof of π in the sequent calculus.

We say that π w π ′ if there is a proposition in π that can be pruned from all sequents in π to produce the valid proof π ′ . PU SC will be the transitive closure of sp ∪ w .

Lemma 36. If π 1 PU SC π 2 then there exists π 3 such that π 1 * sp π 3 * w π 2 .
Proof. We only need to show that if π 1 w π 2 sp π 3 then there exist some π ′ 2 such that π 1 sp π ′ 2 w π 3 . If π 1 w π 2 there exists some proposition P that can be pruned in the sequents in π 1 to get π 2 . Let π ′ 2 be π 3 in which P is added in each sequents by weakening in the same side as in

π 1 . Then π ′ 2 is a subproof of π 1 .
Unfortunately, this definition is not sufficient to define trivial proofs, because if we use a premise through a ↑-l or ↑-r rule, there will always be a strict subproof, so that there are no proofs using premises without strict subproofs. For instance,

P ⊢ P Axiom

A ⊢ P ↑-l seems a good candidate for the trivial proof A → -P , but is contains the subproof P ⊢ P Axiom .

To solve this problem, we can manually add the trivial proofs. We therefore consider proofs a for each formula a ∈ A.

We have to extend the ordering > to trivial proofs: it can be simply done by saying that they cannot be compared with other proofs.

For Postulate C to be verified, we have to extend the subproof relation:

p q if -q is a subproof of p for PU SC -or q = a with a ∈ [p] Pm .
This relation is well-founded because of the wellfoundedness of the subproof relation in the sequent calculus, and because trivial proofs cannot have strict subproofs.

To summarize, with respect to the definitions of ACSs (see Section 5.1) deduction modulo can be seen as an ACS, in the following way: • P: proofs are either couples formed with a sequent calculus proof and a polarized rule in the rewrite system associated with its conclusion, or trivial proofs:

P ! =    . . . Γ ⊢ ∆ , A → ± P ∈ PUSC × A : (A → ± P ) ∈ Rew(Γ ⊢ ∆)    ∪ { a : a ∈ A} • [•]
Pm : premises of a non-trivial proof are the rewrite rules used in its first component, the unique premise of a trivial proof is the formula it corresponds to.

• [•]

Cl : the conclusion of a non-trivial proof is its second component, the conclusion of a trivial proof is the formula it corresponds to.

• >: the ordering on proofs is defined by p > q if p and q are not trivial, their second component is the same as well as the conclusion of their first component, and the skeleton of the first component of p is greater than the one of q for the RPO based on the precedence defined by: for all propositions P, Q, O, if P is greater than Q for the subformula relation, then Cut(P ) > Cut(Q) and Axiom(P ) > Axiom(Q), and for all other inference rules r of Fig. 1, Cut(P ) > Axiom(O) > r.

• : the subproof ordering is defined by p q if neither p nor q are trivial and the first component of p is greater than the first component of q for PU SC ;

or q = a with a ∈ [p] Pm .

With these definitions we can prove the main theorem of this section:

Theorem 37 (Instance of ACS). The unfolding sequent calculus is an instance of ACS, with the definitions of A, P, [•] Pm , [•] Cl , > and given above.

Proof. First we need to show that > and are strict and well-founded orderings. It is not too difficult to prove that > is irreflexive and transitive. It is well founded because the RPO on skeleton is, because the subformula relation is. Concerning , first remark that a q iff q = a. Then, we only need to show that PU SC is a strict ordering: indeed, it is trivially irreflexive, and transitive by definition. To show that is well founded we also only need to show that PU SC is. This is less trivial, but can be shown using Lemma 36 which says that if p PU SC q, then q can be obtained by pruning some propositions in a subproof of p. Then we only need to show that sp and w are well founded, which holds because the first relation makes the skeleton of proof decrease whereas the second makes the number of propositions in the conclusion decrease.

We then show the postulates:

• Postulate A: suppose a ∈ R, we want to show that a is the conclusion of a proof built with R. a is such a proof.

• Postulate B: let a be in Th Th R. By definition there is a proof

p ∈ Pf (Th R) such that [p] Cl = a. If p is trivial, then {a} = [p] Pm ⊆ Th R therefore a ∈ Th R. If p is not trivial, then its first component π p ∈ PUSC proves Γ ⊢ ∆ in Th R for some Γ ⊢ ∆ such that a ∈ Rew(Γ ⊢ ∆). Rewrite rules used in π p are therefore in Th R. Let b ∈ [p] Pm be such a rule. There exists q ∈ Pf (R) such that [q] Cl = b. If q is trivial, then {b} = [p] Pm ⊆ R therefore b = [p] Cl ∈ R.
Else, its first component π q ∈ PUSC proves s in R for some s such that b ∈ Rew(s). Using Property 17 and Proposition 18, we can transform π p into a proof

̟ p of Γ, Prop(s) ⊢ ∆ in [p] Pm \ Rew(s).
One can apply ∧-l, ∨-r, ⇒-r and ∀-r to π q to get a proof of ⊢ Prop(s) in R. By applying Cut to this proof and ̟ p we obtain a proof of Γ ⊢ ∆ in [p] Pm \ Rew(s) ∪ R. By repeating this process to every premises of p not in R, we eventually obtain a proof

π in R whose conclusion is Γ ⊢ ∆. Then, a = [ π, a ] Cl ∈ [Pf (R)] Cl = Th R.
• Postulate C: it holds by definition of the subproof relation .

• Postulate D: suppose p q. If q = a then by definition of , we have [q] Pm = {a} ⊆ [p] Pm . If q is not trivial, neither is p. In that case, by definition of PU SC the first component of q use a subset of the rules used in the first component of p.

• Postulate E: suppose p q > r. Because q is comparable with r, none of them is trivial, and p neither. We call π p , π q and π r their first components. Because of Lemma 36, π q can be obtained by pruning some first-order propositions in a subproof π ′ of π p . By definition of >, π q and π r have the same conclusion. We can therefore add the propositions pruned in π ′ in π r , and replace π ′ by this proof in π p to get a valid proof π v . If a is the second component of p, then let v ! = π v , a , which is a correct ACS proof because π p and π v have the same conclusion. Then p > v because the RPO is a simplification ordering and because if π 1 w π 2 , then π 1 and π 2 have the same skeleton. Moreover, by definition of π v , v r. Furthermore, the rewrite rules used in π v are included in the ones used in π p and π r , therefore v ∈ Pf ([p] Pm ∪ [r] Pm ).

A Generalized Completion Procedure

We want to define a completion procedure through critical proofs. For this, we first need some characterizations of the normal-form proofs and the critical proofs. The limit of this completion procedure will be an equivalent rewrite system modulo which the sequent calculus admits Cut.

Normal-form Proofs and Critical Proofs in Deduction Modulo

Proposition 38 (Characterization of Normal-Form Proofs). A proof in the unfolding sequent calculus is in normal form iff it is either a trivial proof or its first component is a Cut-free proof with no unneeded logical rules, where Axiom is applied only to atomic propositions.

Proof. If a proof p in Pf (R) is not a trivial proof, and its first component π p possesses a Cut at position p, then using Property 17(c), we know that there exists a Cut-free proof of the sequent ⊢ P(Γ ⊢ ∆) in Rew(Γ ⊢ ∆) where Γ ⊢ ∆ is the conclusion of π p |p . Using Lemma 3 we obtain a Cut-free proof π q of Γ ⊢ ∆. Because π q is Cut-free and π p |p has a Cut at root, the skeleton of π p |p is greater than the one of π q for the RPO. Replacing π p |p by π q in p using Postulate E, we obtain a smaller proof than p which is in Pf (T hR) because π q is by assumption in Rew(Γ ⊢ ∆) = a∈Rew(Γ⊢∆) [ π p |p , a ] Cl , and each π p |p , a is in Pf (R). Therefore p cannot be in normal form.

If a proof p is not a trivial proof, and its first component π p has a unneeded logical rule at position p, then the direct subproofs of π p |p shows the same conclusion as π p |p when weakened, and are smaller because an RPO is a simplification ordering and the weakening of a proof does not change its skeleton. By using Postulate E we can obtain a proof smaller than p, and therefore p cannot be in normal form.

If a proof p is not a trivial proof, and its first component apply Axiom to a non-atomic proposition, then it is always possible to replace this application by some proof where Axiom is applied only to atomic propositions. Given the definition of the precedence, this proof is smaller than the original application of Axiom and p is therefore not minimal.

Due to our definition of the precedence of the RPO, if a non-trivial proof p is not minimal in every presentation of a theory, i.e. there exists a smaller proof q, then either the first component of p contains a Cut, or it applies Axiom on a non-atomic proposition, or the first component of q is a weakened subproof of the one of p, i.e. unneeded rules were applied in p.

A trivial proof in Pf (R) is not comparable with any other proof, in particular in Pf (Th R), so that it is in normal form.

We give now a characterization of the critical proofs in deduction modulo.

Proposition 39 (Critical Proofs in Deduction Modulo). Critical proofs in deduction modulo are non trivial and their first component is of the form π . . . .

Γ, A, P ⊢ ∆ Γ, A ⊢ ∆ ↑-l(B → -P 1 ) π ′ . . . . Γ ⊢ Q, A, ∆ Γ ⊢ A, ∆ ↑-r(C → + P 2 ) Γ ⊢ ∆ Cut(A)
where

• π and π ′ are Cut-free;

• π and π ′ do not use unneeded logical rules;

• π and π ′ apply Axiom only to atomic propositions;

• Γ contains only universally quantified propositions and atomic propositions different from A;

• ∆ contains only existentially quantified propositions and atomic propositions different from A;

• all propositions of Γ ∪ ∆ are principal proposition either in some Axiom (and not ↑-l nor ↑-r), ∀-l or ∃-r in π or π ′ .

• at least one of B → -P 1 or C → + P 2 is not a term rewriting.

Proof. We essentially follow the proof of the Hauptsatz of Girard, Lafont, and Taylor [START_REF] Girard | Proofs and Types[END_REF]Chapter 13].

Because of Proposition 38, subproofs of a critical proof (which are by definition in normal form) that are not trivial must be Cut-free. Furthermore, because a critical proof is not in normal form, then it possesses either a Cut, a unneeded logical rule or apply Axiom to a non atomic proposition. In the second and third cases, we can find a smaller proof in the same presentation, contradicting the minimality of critical proofs. Therefore a critical proof has a Cut at its root. It is a proof of the form

π π 1 • • • π n Γ, P ⊢ ∆ r π ′ 1 • • • π ′ m Γ ⊢ P, ∆ r' π ′ Γ ⊢ ∆ Cut(P )
where π and π ′ are in normal form, so are cut-free, do not use unneeded rules and apply Axiom only to atomic propositions. Moreover, if A ∈ Γ ∪ ∆, then Cut is unneeded. Furthermore, if Γ contains a non-atomic proposition which is not universally quantified, then either it can be pruned, in which case we can obtain a proof smaller for which is not in normal form (It contains a Cut.); or it is the principal proposition of some inference rule (different from ∀-l and ↑-l) in π or π ′ . But it is possible to permute this inference rule with all other inference rules until Cut (see Note 1), in which case we obtain a proof smaller for > in the same presentation. This is also the case if some atomic proposition is rewritten using ↑-l. For ∆ this is dual. All propositions in Γ ∪ ∆ are used somewhere, else they could be pruned and we could obtain a proof smaller for which would not be in normal form.

In the following, ̟, ̟ ′ , ̟ 1 , . . . , ̟ n , ̟ ′ 1 , . . . , ̟ ′ m are proof obtained from π, π ′ , π 1 , . . . , π n , π ′ 1 , . . . , π ′ m by weakening. We can now check the different cases that can be found in Section 13.2 of Girard et al. [START_REF] Girard | Proofs and Types[END_REF] (note that we do not have to consider structural rules in the polarized unfolding sequent calculus):

1. r is Axiom. There are two cases :

• the principal proposition of the Axiom is P , then we have necessarily P ∈ ∆ and π ′ is therefore a proof of Γ ⊢ ∆ which is smaller than the initial proof, contradicting its minimality;

• the principal proposition of the Axiom is another proposition Q, then Q ∈ Γ and Q ∈ ∆, so that we can build the proof Γ ⊢ ∆ Axiom which is smaller than the initial proof, contradicting its minimality.

2. r' is Axiom. This case is handled as case 1.

3. r is a logical rule other than a left one with principal proposition P . In this case, the conclusion of a subproof π i has the form Γ i , P ⊢ ∆ i , because r does not touch P . We can build the proof

̟ 1 ̟ ′ . . . . . . Γ, Γ 1 , P ⊢ ∆, ∆ 1 Γ, Γ 1 ⊢ P, ∆, ∆ 1 Γ, Γ 1 ⊢ ∆, ∆ 1 Cut(P ) ̟ n ̟ ′ . . . . . . Γ, Γ n , P ⊢ ∆, ∆ n Γ, Γ n ⊢ P, ∆, ∆ n Γ, Γ n ⊢ ∆, ∆ n Cut(P ) • • • • • • • • • • • • • Γ, Γ ⊢ ∆, ∆
r and then use Lemma 5. If we look at the proof of this lemma, we can show by induction that the skeleton of the contracted proofs is smaller than the original one for the RPO. We therefore have a smaller proof than the initial proof, contradicting its minimality. 4. r' is a logical rule other than a right one with principal proposition P .

This case is handled as case 3. 5. Both r and r' are logical rules, r a left one and r' a right one, of principal proposition P . This is one of the key cases as given in Section 13.1 of Girard et al. [START_REF] Girard | Proofs and Types[END_REF] : by replacing the Cut over P by Cuts over subformulae of P we obtain a smaller proof, thus contradicting the minimality of the original proof. For instance, if P = P 1 ∧ P 2 , the initial proof

π 1 . . . . Γ, P 1 , P 2 ⊢ ∆ Γ, P 1 ∧ P 2 ⊢ ∆ ∧-l π ′
is greater than the proof

π 1 . . . . Γ, P 1 , P 2 ⊢ ∆ ̟ ′ 2 . . . . Γ, P 1 ⊢ P 2 , ∆ Γ, P 1 ⊢ ∆ Cut(P 2 ) π ′ 1 . . . . Γ ⊢ P 1 , ∆ Γ ⊢ ∆ Cut(P 1 )
6. r or r' is an unfolding rule applying to another proposition than P . This case can in fact be handled as case 3. 7. r is an unfolding rule and r' is a logical rule, both applying to P . This case cannot occur, because only atomic propositions are unfolded, so that no logical rule can be applied to P . 8. r is a logical rule and r' is an unfolding rule, both applying to P . This case is handled as case 7. 9. r and r' are both unfolding rules applying to P . Therefore P has to be atomic, and is rewritten by B → -P 1 to the left and C → + P 2 to the right. If both of this rewriting are term rewriting, then, because of confluence of R T (Σ,V ) , we know that there is some

P ′ such that P 1 * -→ R T (Σ,V ) P ′ * ←- R T (Σ,V ) P 2 .
The proof

π 1 . . . . Γ, P 1 ⊢ ∆ Γ, P ′ ⊢ P ′ , ∆ Axiom Γ, P 2 ⊢ P 1 , ∆ Unfolding Rules ̟ ′ 1 . . . . Γ ⊢ P 1 , P 2 , ∆ Γ ⊢ P 1 , ∆ Cut(P 2 ) Γ ⊢ ∆ Cut(P 1 )
is smaller than the initial proof (remind that the term rewrite relation is by definition included in the subformula relation), contradicting its minimality. Otherwise, we are exactly in the case stated in the theorem.

Note. If we suppose, as in the order condition of Hermant [START_REF] Hermant | Semantic Cut Elimination in the Intuitionistic Sequent Calculus[END_REF], that the proposition rewrite system is confluent, and that it is included in an well-founded ordering compatible with the subformula relation, then we can take this ordering instead of the subformula relation to compare Cuts in the precedence. Doing this, we can prove that there are no minimal proofs of this form, and consequently no critical proofs. Therefore the admissibility of Cut is verified, as a by-product of the completion procedure.

The main difference with Hermant [START_REF] Hermant | Semantic Cut Elimination in the Intuitionistic Sequent Calculus[END_REF] is that he gives a semantic proof of the admissibility of Cut, whereas we have here a Cut elimination algorithm, i.e. a terminating syntactical process that transforms a proof into a Cut-free one. It is proved by Dowek and Werner [START_REF] Dowek | Proof Normalization Modulo[END_REF] that such an order condition provides normalization.

The fact that the compatibility of the rewrite system with the subformulae relation implies the Cut-admissibility was also independently found by Aiguier, Boin, and Longuet [START_REF] Aiguier | On Generalized Theorems for Normalization of Proofs[END_REF], with the same kind of ordering over proofs.

Theorem 40 (Undecidability of Critical Proof Search). The problem Input: A propositional rewrite system R and a sequent Γ ⊢ ∆.

Decide if Γ ⊢ ∆ is the conclusion of a critical proof in R.

is undecidable.

Proof. We reduce to the problem of validity in first-order logic.

Let P be a first-order proposition.

Let A, B be atomic propositions not appearing in P . Consider the following propositional rewrite system:

A → -B A → + P .
We can check that ⊢ B is the conclusion of a critical proof in it if and only if P is valid. Indeed, a critical proof is necessarily of the form

A, B ⊢ B Axiom A ⊢ B ↑-l
Proof of P with no ↑-l nor ↑-r . . . .

⊢ P, A, B ⊢ A, B ↑-r ⊢ B Cut(A)
Of course, in the quantifier-free case, this problem is decidable. It remains to be investigated for what fragments of first-order logic it is decidable, in particular if these fragments are the same that for the validity problem.

The Completion Procedure

As we wrote in Section 5.1, we want to define a completing deduction mechanism by adding to a presentation A a presentation C(A) such that Comp(A) ⊆ C(A) ⊆ Th A.

Here, using Property 17(c), we know that for all proofs p whose first component is a proof π of a sequent Γ ⊢ ∆ there exists a Cut-free proof of the sequent ⊢ P(Γ ⊢ ∆) in Rew(Γ ⊢ ∆). Using Lemma 3 we obtain a Cut-free proof π of Γ ⊢ ∆ in Rew(Γ ⊢ ∆). If the proof p is critical, π has a Cut at its root and thus it is greater than π ′ , so that we can use this particular π ′ in the definition of Comp. Note that if p is critical, so are the proofs with the same first component π but another conclusion (that is, another rule in Rew(Γ ⊢ ∆)). We therefore have to add the premises of π ′ , but these premises are in fact in Rew(Γ ⊢ ∆), and we obtain all Rew(Γ ⊢ ∆) by considering the conclusion of all the critical proofs whose first component is π:

Comp(A) ! = p∈Crit (A) [p] Cl .
The best procedure is thus to add only the conclusions of critical proofs. Nevertheless, searching for these conclusions is undecidable, so that we must use a superset of them. Here we will add the conclusion of the proofs in the form of Proposition 39. (Note that this proposition is only a necessary condition for being critical.)

We must consider proofs of the form of Proposition 39. As π and π ′ are Cut-free and do not use unneeded logical rules, they could be found using for instance a tableau method modulo, like TaMed [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF][START_REF] Bonichon | A Semantic Completeness Proof for TaMed[END_REF], which is complete with respect to Cut-free proofs, if we knew Γ and ∆. The idea is therefore to apply a tableau method for the deduction modulo on A, P ⊢ and ⊢ A, Q until they are either proved or the method terminates, and to complete the sequents to close all branches. Of course, the tableau method may not terminate, in which case we have to arbitrarily decide to stop it. If we stop it too early, then maybe there remains some open branch that could be closed, and therefore Γ and ∆ in the critical-proof candidate will not be minimal. This is not a problem because the generated rewrite rules for this will be more general than the one for the real critical proof. However, the longer the tableau method runs, the more accurate the additional rules will be.

Then, we have to close all remaining open branches by adding some propositions in Γ and ∆. We know we do not need to add A. The formulae in Γ and ∆ can be non-atomic formulae, in which case they could be further decomposed by the tableau method. However, if we use a tableau method with meta-variables (see [START_REF] Fitting | First-order logic and automated theorem proving[END_REF]), the order in which formulas are decomposed in no longer relevant, only the unification of meta-variables is, so that they could have occurred before the decomposition of A, P ⊢ or ⊢ A, Q. As Axioms are applied only to atomic propositions, we only need to consider such cases to close the branches, and then, we may need to recompose the atomic formulae added to the branches to get the actual Γ and ∆. In particular, if we added some atomic formula in which there is a variable which was introduced in the proof by some ∃-l or ∀-r (an Eigenvariable) 5 , then it cannot appear in Γ ∪ ∆. It therefore has to be introduced using a quantification. For instance, if we wanted to add B(x) in Γ and x is such an Eigenvariable, we have to add ∀x. B(x) instead. We need to do so for all possible choices of atomic propositions different from A to close the branches, and a priori for all choices of recompositions. We would obtain that way all possible conclusions Γ ⊢ ∆ of proofs of the form of Proposition 39, and C(A) would be the union of Rew(Γ ⊢ ∆) for each of them. However, it seems that we only need to recompose the formulae to add the quantifications protecting the Eigenvariables. Indeed, by applying other recompositions, we obtain sequents Γ ⊢ ∆ whose rules in Rew(Γ ⊢ ∆) are redundant w.r.t. the rules obtained without the recomposition -this is due to the fact that Rew is working by decomposing the formulae in the sequent.

We repeatedly complete the rewrite system until a fixpoint is reached. The limit admits Cut.

Theorem 41 (Cut Admissibility of the Limit). For all sequents Γ ⊢ ∆, for all proposition rewrite systems R 0 , Γ ⊢ ∆ has a proof in R 0 if and only if it has a Cut-free proof in R ∞ .

Proof. By Proposition 32, we know that our deduction mechanism is completing, and therefore by Theorem 30

Th R 0 ⊆ [Pf (R ∞ ) ∩ Nf (R 0 )] Cl . (1)
The "if" part comes from the fact that we only add rules that corresponds to sequents provable in R 0 . For the "only if", suppose that Γ ⊢ ∆ has a proof in R 0 , then using (1) there exists a proof p a of conclusion a in Pf (R ∞ ) ∩ Nf (R 0 ) for all rules a ∈ Rew(Γ ⊢ ∆). If p a is trivial, then we can use Property 17(c) to find a Cut-free proof with the same conclusion, otherwise Proposition 38 shows that p a is Cut-free. We can therefore conclude with Property 19.

Examples

In the case of Crabbé's example presented in the introduction, the input is the rewrite system {A → + B∧¬A; A → -B∧¬A} and the completion procedure generates B → -⊥.

With this new rule, we can show that there are no more critical proofs. The proposition rewrite system

A → B ∧ ¬A B → ⊥ admits Cut.
The next example deals with quantifiers and is extracted from Hermant [START_REF] Hermant | Semantic Cut Elimination in the Intuitionistic Sequent Calculus[END_REF]:

r ∈ r → ∀y. y ≃ r ⇒ y ∈ r ⇒ C where y ≃ z ! = ∀x. (y ∈ x ⇒ z ∈ x).
It is terminating and confluent, but does not admits Cut.

The critical proofs have the form . . . .

r ∈ r, ∀y. y ≃ r ⇒ y ∈ r ⇒ C ⊢ r ∈ r ⊢ ↑-l . . . . ⊢ r ∈ r, ∀y. y ≃ r ⇒ y ∈ r ⇒ C ⊢ r ∈ r ↑-l ⊢ Cut(r ∈ r)
The left part can be developed as

r ∈ r, C ⊢ r ∈ r ⊢ t 1 ∈ r r ∈ r, t 1 ∈ r ⇒ C ⊢ ⇒ -l r ∈ r, t 1 ∈ z ⊢ r ∈ z r ∈ r ⊢ t 1 ∈ z ⇒ r ∈ z ⇒ -r r ∈ r ⊢ t 1 ≃ r ∀-r r ∈ r, t 1 ≃ r ⇒ t 1 ∈ r ⇒ C ⊢ ⇒ -l r ∈ r, ∀y. y ≃ r ⇒ y ∈ r ⇒ C ⊢ ∀-l
and the right part as

r ∈ t 0 , z ∈ r ⊢ r ∈ r, C z ∈ r ⊢ z ∈ t 0 , r ∈ r, C z ∈ t 0 ⇒ r ∈ t 0 , z ∈ r ⊢ r ∈ r, C ⇒ -l z ≃ r, z ∈ r ⊢ r ∈ r, C ∀-l z ≃ r ⊢ r ∈ r, z ∈ r ⇒ C ⇒ -r ⊢ r ∈ r, z ≃ r ⇒ z ∈ r ⇒ C ⇒ -r ⊢ r ∈ r, ∀y. y ≃ r ⇒ y ∈ r ⇒ C ∀-r .
To close the proofs, we can for instance have t 0 = r = t 1 , and C in the right part of the sequent (to close r ∈ r, C ⊢). One can see that other choices will not produce critical proofs. The resulting sequent is therefore ⊢ C, and the added rule is C → + ⊤. This rule does not generate new critical proofs, and consequently, the proposition rewrite system

   r ∈ r → + ∀y. y ≃ r ⇒ y ∈ r ⇒ C r ∈ r → -∀y. y ≃ r ⇒ y ∈ r ⇒ C C → + ⊤ admits Cut.
One can also think of another example, where there remains quantifiers in the conclusion: one can replace B by ∃x. ∀y. B ∧ C(x, y) in Crabbé's example to get the rule: A → (∃x. ∀y. B ∧ C(x, y)) ∧ ¬A where A and B are atomic propositions, and C a predicate of arity 2.

We first search for a proof of A, (∃x. A → (∃x. ∀y. B ∧ C(x, y)) ∧ ¬A has already been applied in the right part of the sequent, so it is not useful to do it again, and so we cannot close the derivation. We see that we have to add propositions in the context to close the remaining branches. As we do not add A, and Axiom is only applied to atomic propositions, there remains only the choice to add B in Γ for the left branch and C(x, y) in Γ for the right branch. However, in C(x, y), the variable y is an Eigenvariable, so we need in fact to add ∀y. C(x, y). Finally, the conclusion of the critical proof is B, ∀y. C(x, y) ⊢ which gives for instance the rewrite rule B → -∀x. ¬∀y. C(x, y). With this new rule, there are no longer critical proofs.

In particular we have the following Cut-free proof of ∃x. and may be completed by the rewrite rule C → + E.

We nevertheless conjecture that if the initial proposition rewrite system is confluent, the completion procedure is terminating, possibly in one step.

Conclusion and Perspectives

This paper reveals a deep logical correspondence between the sequent calculus, proof orderings and completion. We have first shown the boundaries of the research for an optimal criterion which ensures the Cut admissibility of a rewrite system by proving its undecidability in general. Then, we have proposed how to circumvent this issue by transforming the rewrite systems we are working with into an equivalent one which admits Cut. This is done by setting the right abstract canonical system structure on the proof space of the unfolding sequent calculus modulo, which is equivalent to the asymmetric sequent calculus modulo, in particular concerning Cut admissibility. This permits to use abstract completion to recover the admissibility of Cut. This abstract completion is precise enough to be operational, and it is actually implemented, based on a prototype of the tableau method modulo TaMed [START_REF] Bonichon | A Semantic Completeness Proof for TaMed[END_REF], and coded in the language TOM+OCaml [http://tom.loria.fr/, http://caml.inria. fr/ocaml/index.en.html]. The implementation is available on the SVN distribution of TOM (see http://gforge.inria.fr/scm/?group id=78) in the directory trunk/jtom/application/completion. Note that because the implemented tableau method is for non-polarized deduction modulo, the completion procedure adds non-polarized rewrite rules thanks to the translation • ∓ given in Section 2.2 before Proposition 9.

All this opens many questions that we are now considering. The limit of the completion procedure admits Cut in the polarized sequent calculus, and therefore we can translate it by Corollary 8 and Proposition 9 into a non-polarized rewrite system that admits Cut in the asymmetric sequent calculus modulo. However, this system may be non-confluent, so we do not know if it admits Cut in the original version of the sequent calculus modulo of Dowek et al. [START_REF] Dowek | Theorem Proving Modulo[END_REF]. However, if we begin with a confluent rewrite system R 0 , then the original sequent calculus modulo R 0 is equivalent to the asymmetric sequent calculus modulo R ∓ ∞ without Cut. This is exactly what we wanted, since the asymmetric sequent calculus modulo without Cut is analytic, in the sense that rewriting is oriented from the bottom to the top of proofs, which induces that the asymmetric sequent calculus modulo is well adapted for proof search. The usual restriction of deduction modulo to confluent rewrite system was mainly imposed to be able to check the congruence using only rewritings, and is no longer needed as far as we know that the final system prove the same that the original one.

The ordering on proofs we are using is adapted to consider Cut admissibility as a normal-form property of an ACS, but produces too many critical proofs, in particular when quantifiers are involved, because some of the rules produced by the completion procedure subsumes other ones. (For instance A → + ∃x. P (x) subsumes A → + P (t) for a particular t ∈ T (Σ, V ).) This ordering has therefore to be refined in order to restrict oneself to the more relevant critical proofs.

Furthermore, our procedure can be used to determine if a system admits Cut. Indeed, if a proposition rewrite system is a fixpoint of this procedure, then we know that it admits Cut. Nevertheless, the converse is not true, essentially because we have to use a superset of the critical proofs. It will be interesting to check what results this procedure will give on system that are proved to admits Cut, like Higher Order Logic [START_REF] Dowek | HOL-λσ an intentional first-order expression of higher-order logic[END_REF] or arithmetic [START_REF] Dowek | Arithmetic as a Theory Modulo[END_REF], or for systems for which the admissibility of Cut is unknown yet, such as Pure Type Systems [START_REF] Burel | A First-Order Representation of Pure Type Systems using Superdeduction[END_REF].

Indeed, we have shown that the Rew algorithm provides a constructive way to transform a first-order theory into a proposition rewrite system. Up to efficiency questions, this closes the problem of transforming proofs in a theory into proofs modulo, i.e. to replace deduction steps by computational ones. What remains still open and challenging is to understand how to systematically build first-order theories out of general ones (e.g. HOL or arithmetic) and how to balance the amount of computations on term versus the one on propositions.

Moreover, our procedure only guarantees the admissibility of Cut, and does not provide a Cut elimination procedure. In other words, we do not have a process that transform proofs with Cuts to Cut-free ones, so that we have to build the Cut-free proofs from scratch. In particular, for the completed system, normalization may not hold. For instance, with Crabbé's rule, once the system is completed, the initial proof of B ⊢ can still be constructed, and it is still not normalizing, i.e. the λ-term that is associated to the proof can be infinitely β-reduced. We can notice that, even if Cut is admissible, the proof of Proposition 39 does not give a cut elimination procedure: we know that there are no critical proofs, but we do not know how to transform a proof in the form of Proposition 39 into a smaller one (without building a Cut-free proof from scratch). We probably have to introduce some simplification rules in order to suppress the possibility to build non-normalizing proofs. For instance, in our example, we could simplify A → B ∧ ¬A into A → ⊥ ∧ ¬A using B → ⊥, and then simplify it to A → ⊥, the system {A → ⊥ ; B → ⊥} being normalizing. Besides, with such simplification rules, we may obtain the canonical presentation of the system.

Lastly, it will be interesting to understand how the results presented here can be transferred to intuitionistic logic. In particular, the impossibility to build a Rew function without breaking the witness property shows that it is not trivial. We tackle this issue in [START_REF] Burel | Automating Theories in Intuitionistic Logic[END_REF].

Figure 1 :

 1 Figure 1: Unfolding Sequent Calculus

Step 1 .

 1 Choose a sequent. Push all negated propositions on the other side of the sequent. For instance, A, ¬B ⊢ ¬C, ¬¬D becomes A, C ⊢ B, D. If the new Γ contains only underlined propositions (or no proposition), go to step 2. If the new ∆ contains only underlined propositions (or no proposition), go to step 3. Else, go to either Step 2 or Step 3.

Proposition 24 .

 24 The Rew function defined in Section 4.2 has the Properties 16, 17 and 19.

Example 26 .d

 26 For standard completion, formulae are rewrite rules or equations, proofs are proofs by rewriting (for instance a ←as a proof of a = d in Pf ({s → t; u → v; e = f })). The proof ordering is chosen so that a ←-s→t b -→ u→v c is greater than a ←→ a=c c, which is greater than a proof of the form a * -→ * ←c.

•

  A: formulae are polarized rewrite rules A ! = PRR (= Rew(S) by Property 16)

⊢

  ∀y. B ∧ C(x, y)) ∧ ¬A ⊢, and we get A, (∃x. ∀y. B ∧ C(x, y)) ⊢ A Axiom(A) A, (∃x. ∀y. B ∧ C(x, y)), ¬A ⊢ ¬-l A, (∃x. ∀y. B ∧ C(x, y)) ∧ ¬A ⊢ ∧-l We try do the same for the right part ⊢ ∃x. ∀y. B ∧ C(x, y), B, A ⊢ ∃x. ∀y. B ∧ C(x, y), C(x, y), A ⊢ ∃x. ∀y. B ∧ C(x, y), B ∧ C(x, y), A ∧-r ⊢ ∃x. ∀y. B ∧ C(x, y), ∀y. B ∧ C(x, y), A ∀-r ⊢ ∃x. ∀y. B ∧ C(x, y)(∃x. ∀y. B ∧ C(x, y)) ∧ ¬A, A ∧-r

A

  ∀y. B ∧ C(x, y) ⊢, corresponding to the conclusion B ⊢ of the critical proof in the original Crabbé system: ∀y. B ∧ C(x, y), C(x, y 0 ), B, ∀x. ¬∀y. C(x, y), C(x, y) ⊢ C(x, y 0 ) Axiom ∀y. B ∧ C(x, y), B ∧ C(x, y 0 ), B, ∀x. ¬∀y. C(x, y), C(x, y) ⊢ C(x, y 0 ) ∧-l ∀y. B ∧ C(x, y), B, ∀x. ¬∀y. C(x, y), C(x, y) ⊢ C(x, y 0 ) ∀-l ∀y. B ∧ C(x, y), B, ∀x. ¬∀y. C(x, y), C(x, y) ⊢ ∀y. C(x, y) ∀-r ∀y. B ∧ C(x, y), B, ∀x. ¬∀y. C(x, y), ¬∀y. C(x, y), C(x, y) ⊢ ¬-l ∀y. B ∧ C(x, y), B, ∀x. ¬∀y. C(x, y), C(x, y) ⊢ ∀-l ∀y. B ∧ C(x, y), B, C(x, y) ⊢ ↑-l ∀y. B ∧ C(x, y), B ∧ C(x, y) ⊢ ∧-l ∀y. B ∧ C(x, y) ⊢ ∀-l ∃x. ∀y. B ∧ C(x, y) ⊢ ∃-l In these three examples, only one step was needed to produce a complete system. But the system → -B A → + C D → -B D → + E may need two steps to produce the completed systemR ∪    B → -C B → + E C → + E .Indeed, the first two rules of R create the critical proofB, A, C ⊢ C Axiom B, A ⊢ C ↑-l B ⊢ A, B, C Axiom B ⊢ A, C ↑-r B ⊢ C Cut(A)that leads for instance to the rewrite rule B → -C. Similarly the two other rules may complete the system by the rewrite rule B → + E. Consequently, after one step the system has a critical proof E, B, C ⊢ C Axiom

  . . . , P n ⊢ ∀x. Q " P 1 , . . . , P n ⊢ {y/x}Q where y does not appear in P 1 , . . . , P n P 1 , . . . , P n ⊢ ∃x. Q " P 1 , . . . , P n , ¬∃x. Q ⊢ {t/x}Q where t can be any term P 1 , . . . , P n ⊢ A " A → + ∃x 1 , . . . , x p . (P 1 ∧ • • • ∧ P n ) (A atomic, and the x i are the free variables appearing in P 1 , . . . , P n but not in A) for P 1 , . . . , P n ⊢ ¬Q, return to Step 1 Step 3. Decompose the first proposition iteratively, dually from step 2. For instance, P 1

In the case of deduction modulo, the intuitive notion of subformula must take the considered rewrite relation into account.

In Crabbé's manuscript, A represents rs ∈ rs and B rs ∈ s where rs is {x ∈ s : x ∈ x}. Then, there is a proof of rs ∈ s in Zermelo's set theory that is not normalizing.

!= is used for definitions.

Γ ⊢ ¬P, ∆ ¬-r Γ, P, Q ⊢ ∆ Γ, P ∧ Q ⊢ ∆ ∧-l Γ ⊢ P, ∆ Γ ⊢ Q, ∆ Γ ⊢ P ∧ Q, ∆ ∧-r Γ, P ⊢ ∆ Γ, Q ⊢ ∆ Γ, P ∨ Q ⊢ ∆ ∨-l Γ ⊢ P, Q, ∆ Γ ⊢ P ∨ Q, ∆ ∨-r Γ, Q ⊢ ∆ Γ, ⊢ P, ∆ Γ, P ⇒ Q ⊢ ∆ ⇒ -l Γ, P ⊢ Q, ∆ Γ ⊢ P ⇒ Q, ∆ ⇒ -r Γ,∀x. P, {t/x}P ⊢ ∆ Γ, ∀x. P ⊢ ∆ ∀-l Γ ⊢ {y/x}P, ∆ Γ ⊢ ∀x. P, ∆ ∀-r Γ, {y/x}P ⊢ ∆

. . . .Γ ⊢ P 1 , ∆ π ′

. . . .Γ ⊢ P 2 , ∆ Γ ⊢ P 1 ∧ P 2 , ∆ ∧-r Γ ⊢ ∆ Cut(P 1 ∧ P 2 )

Working using meta-variables, this would mean that the formula contains a Skolem symbol.

Acknowledgements. We had many fruitful discussions with Nachum Dershowitz and Gilles Dowek on the topics of this paper. Many thanks also to the anony-mous referees for their careful reading and clever suggestions.