David Delahaye
email: david.delahaye@cnam.fr

Damien Doligez
email: damien.doligez@inria.fr

Frédéric Gilbert
email: frederic.charles.gilbert@inria.fr

Pierre Halmagrand
email: pierre.halmagrand@inria.fr

Olivier Hermant
email: olivier.hermant@mines-paristech.fr

Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo ⋆

Keywords: Tableaux, Deduction Modulo, Rewriting, Automated Theorem Proving, Proof Checking, Zenon, Dedukti

We propose an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. We also present a heuristic to perform this latter step automatically, and assess our approach by providing some experimental results obtained on the benchmarks provided by the TPTP library, where this heuristic is able to prove difficult problems in set theory in particular. Finally, we describe an additional backend for Zenon that outputs proof certificates for Dedukti, which is a proof checker based on the λΠ-calculus modulo.

Introduction

Proof search in axiomatic theories, such as Peano arithmetic and set theory, or decidable fragments (Presburger arithmetic, arrays and pointers, axiomatizations of memory models, etc.) is receiving increasing attention, driven by the applications of formal methods in industrial settings. Leaving axioms wandering among the hypotheses is not a reasonable option, as it induces a combinatorial explosion in the proof search space. Moreover, axioms themselves generally do not bear any specific meaning that could be used by automated theorem provers.

A solution to address this problem is to use a cutting-edge combination of a first order automated theorem proving method (resolution) with theory-specific decision procedures. This approach has drawbacks, namely the need for a specific decision procedure for each given theory. This imposes a decidability constraint on the theories that we can work with, as well as a lack of automatability. As a consequence, we lose genericity over the theories. However, SMT solvers are well-suited for industrial applications, where those problems are not a concern.

Our approach is to make use of the advances of deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF], which allows us to transform axioms into rewrite rules. For example, Peano arithmetic or Zermelo set theory can be expressed without axioms. This way, we turn proof search among the axioms into computations, avoiding unnecessary blowups, and we shrink the size of proofs by recording only their meaningful steps. Deduction modulo has already been experimented within first order automated theorem provers. This is the case of iProver Modulo [START_REF] Burel | Experimenting with Deduction Modulo[END_REF], where a resolution-based automated theorem prover has been extended to deduction modulo. This is also the case of Super Zenon [START_REF] Jacquel | Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover[END_REF], which is an extension of the Zenon tableau-based automated theorem prover [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] to superdeduction [START_REF] Brauner | Principles of Superdeduction[END_REF], a variant of deduction modulo.

In this paper, we go further along this path by adapting Zenon to deduction modulo itself, and following some of the ideas of [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF]. Compared to the approach of Super Zenon, this new tool, called Zenon Modulo, allows us to capture more computational aspects of theories, since deduction modulo also adds the possibility to rewrite over terms, while superdeduction only considers rewrite rules over propositions. Moreover, it will also allow us to compare this extension with that of iProver Modulo, and assess the impact of the integration of deduction modulo into different proof search techniques (i.e. resolution and tableaux).

Another contribution introduced in this paper is a heuristic that automatically transforms any set of axioms (and therefore any theory) into a set of rewrite rules, which can be used during the proof search step of Zenon. With this heuristic, we observe significant improvements over the pure axiomatic proof search of Zenon, as can be seen in the experimental results obtained on the set of problems provided by the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF]. In particular, this heuristic appears to be quite appropriate for set theory, where we are able to prove difficult problems.

It should be noted that in the short term, we also plan to work on the dual approach, which consists in building theories modulo manually. In particular, we aim to consider the set theory of the B method [START_REF] Hermant | The B-Book, Assigning Programs to Meanings[END_REF], in order to apply Zenon Modulo to the verification of proof obligations coming from industrial applications, which is one of the goals of the BWare project [START_REF]The BWare Project[END_REF].

One of the major interests of Zenon to experiment deduction modulo resides in its certifying approach, i.e. its ability to produce proof certificates that can be skeptically checked by other proof assistants such as Coq or Isabelle. Extending Zenon to deduction modulo means to also provide a backend able to check proofs in deduction modulo. To do so, we have provided Zenon with a backend that outputs proofs for Dedukti [START_REF] Boespflug | The λΠ-Calculus Modulo as a Universal Proof Language[END_REF], a proof checker based on the λΠ-calculus modulo.

This paper is organized as follows: in Sec. 2, we first introduce the principles of deduction modulo; we then present, in Sec. 3, the rules of Zenon for deduction modulo, and describe, in Sec. 4, the corresponding implementation and the experimental results obtained on the benchmarks provided by the TPTP library; finally, in Sec. 5, we provide an overview of the Dedukti backend.

Deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] focuses on the computational part of a theory, where axioms are transformed into rewrite rules, which induces a congruence over propositions, and where reasoning is performed modulo this congruence. For example, considering the inclusion in set theory ∀X, Y (X ⊆ Y ⇔ ∀x (x ∈ X ⇒ x ∈ Y )), the proof of A ⊆ A in sequent calculus has the following form:

Ax . . . , x ∈ A ⊢ A ⊆ A, x ∈ A ⇒R . . . ⊢ A ⊆ A, x ∈ A ⇒ x ∈ A ∀R . . . ⊢ A ⊆ A, ∀x (x ∈ A ⇒ x ∈ A) Ax . . . , A ⊆ A ⊢ A ⊆ A ⇒L . . . , ∀x (x ∈ A ⇒ x ∈ A) ⇒ A ⊆ A ⊢ A ⊆ A ∧L A ⊆ A ⇔ ∀x (x ∈ A ⇒ x ∈ A) ⊢ A ⊆ A ∀L × 2 ∀X, Y (X ⊆ Y ⇔ ∀x (x ∈ X ⇒ x ∈ Y )) ⊢ A ⊆ A
In deduction modulo, the axiom of inclusion can be seen as a computation rule, and therefore replaced by the rewrite rule

X ⊆ Y -→ ∀x (x ∈ X ⇒ x ∈ Y ).
The previous proof is then transformed as follows:

Ax x ∈ A ⊢ x ∈ A ⇒R ⊢ x ∈ A ⇒ x ∈ A ∀R, A ⊆ A -→ ∀x (x ∈ A ⇒ x ∈ A) ⊢ A ⊆ A
where it can be seen that computations are interleaved with the deduction rules. It can be noticed that the proof is much simpler than the one completed using sequent calculus. In addition to simplicity, deduction modulo also allows for unbounded proof size reduction [START_REF] Burel | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo[END_REF].

There exist some other approaches, which can be considered as variants of deduction modulo. This is the case of superdeduction [START_REF] Brauner | Principles of Superdeduction[END_REF], the formalism at the origin of Super Zenon [START_REF] Jacquel | Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover[END_REF], which proposes to use axioms to enrich the deduction system with new deduction rules (called superdeduction rules). Thus, while deduction modulo integrates some axioms of the theory as computations, superdeduction integrates them as deduction rules, following Prawitz's ideas [START_REF] Prawitz | Natural Deduction. A Proof-Theoretical Study[END_REF].

However, in contrast with superdeduction, deduction modulo can also capture some computational aspects that are modeled by means of equational axioms. For instance, if we consider an equational sequent calculus with the theory of Peano arithmetic, the proof of ∃x (x + s(0) = s(s(0))) is the following without deduction modulo (in the proof context, we only provide the two axioms of Peano arithmetic required to complete the proof, referring to them as P):

Ax P, s(0) + s(0) = s(s(0) + 0) ⊢ s(0) + s(0) = s(s(0) + 0) ∀L × 2 P ⊢ s(0) + s(0) = s(s(0) + 0) Π Subst P P ⊢ s(0) + s(0) = s(s(0)) ∃R ∀x (x + 0 = x) ∀x, y (x + s(y) = s(x + y)) ⊢ ∃x (x + s(0) = s(s(0)))
where Π is the proof expressed as follows: Ax P, s(0) + 0 = s(0) ⊢ s(0) + 0 = s(0) ∀L P ⊢ s(0) + 0 = s(0) Refl P ⊢ s(s(0)) = s(s(0))

Subst P P ⊢ s(s(0) + 0) = s(s(0))

In deduction modulo, the two axioms are transformed into computation rules on terms, and therefore replaced by the two rewrite rules x + 0 -→ x and x + s(y) -→ s(x + y). The corresponding proof is then the following:

Refl, s(0) + s(0) -→ * s(s(0)) ⊢ s(0) + s(0) = s(s(0)) ∃R ⊢ ∃x (x + s(0) = s(s(0)))
As previously, it can be noticed that the proof in deduction modulo is much simpler and shorter than the one obtained using the equational sequent calculus.

Deduction Modulo Rules for Zenon

In this section, we provide the adaptation of the proof search rules of Zenon to deduction modulo. This mainly consists in extending the usual rules of Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] by allowing them to work modulo a congruence relation over propositions induced by a set of rewrite rules over propositions and a set of equational axioms and rewrite rules over terms (this extension is partially inspired by the presentation of tableaux modulo presented in [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF]).

In the following, we borrow some of the notations, definitions, and propositions of [START_REF] Dowek | Theorem Proving Modulo[END_REF], and we call FV the function that returns the set of free variables of a formula. In particular, we introduce the notion of class rewrite system: Definition 1 (Class Rewrite System). A term rewrite rule is a pair of terms denoted by l -→ r, where FV(r) ⊆ FV(l). An equational axiom is a pair of terms denoted by l = r. A proposition rewrite rule is a pair of propositions denoted by l -→ r, where l is an atomic proposition and r is an arbitrary proposition, and where FV(r) ⊆ FV(l).

A class rewrite system is a pair, denoted by RE, consisting of:

-R: a set of proposition rewrite rules; -E: a set of term rewrite rules and equational axioms.

Given a class rewrite system RE, the relations = E and = RE are the congruences generated respectively by the sets E and R ∪ E. We then define the notion of RE-rewriting. In the definition below, we use the standard concepts of subterm and term replacement: given an occurrence ω in a proposition P , we write P |ω for the term or proposition at ω, and P [t] ω for the proposition obtained by replacing P |ω by t in P at ω. Definition 2 (RE-Rewriting). Given a class rewrite system RE, the proposition P RE-rewrites to P ′ , denoted by

P -→ RE P ′ , if P = E Q, Q |ω = σ(l), and P ′ = E Q[σ(r)
] ω , for some rule l -→ r ∈ R, some proposition Q, some occurrence ω in Q, and some substitution σ.

The relation = RE is not decidable in general, but there are some cases where this relation is decidable depending on the class rewrite system RE and the rewrite relation -→ RE , as identified by the following proposition: Given a class rewrite system RE, the proof search rules of Zenon adapted to deduction modulo are summarized in Figs. 1 and2 (for the sake of simplification, the unfolding and extension rules are omitted), where the "|" symbol is used to separate the formulas of two distinct nodes to be created, ǫ is Hilbert's operator (ǫ(x).P (x) means some x that satisfies P (x), if it exists, and is considered as a term), capital letters are used for metavariables, and R r , R s , R t , and R ts are respectively reflexive, symmetric, transitive, and transitive-symmetric relations (the corresponding rules also apply to equality). As hinted by the use of Hilbert's operator, the δ-rules are handled by means of ǫ-terms rather than using Skolemization. What we call here metavariables are often named free variables in the tableau-related literature. However, metavariables are not used as variables as they are never substituted, and do not even help to generate a global constraint closing all the branches of the tableau at once; metavariables are instead used as clues (through unification attempts) for the "real" instantiation rules γ ∀inst /γ ¬∃inst . The proof search rules are applied with the usual tableau method: starting from the negation of the goal, apply the rules in a top-down fashion to build a tree. When all branches are closed (i.e. end with a closure rule), the tree is closed, and this closed tree is a proof of the goal. This algorithm is applied in strict depth-first order: we close the current branch before starting working on another branch. Moreover, we work in a non-destructive way: working on a branch will never change the formulas of another branch.

Compared to [START_REF] Dowek | Theorem Proving Modulo[END_REF] and [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF], it should be noticed that there is no explicit rule of extended narrowing in the proposed deduction modulo rules for Zenon, since the relation = RE is actually disseminated in all the initial rules of Zenon. However, the extended narrowing rule is not only a rule that allows us to apply rewrite rules, but also a rule that may suggest instantiations for metavariables. The technique used by Zenon to find those instantiations must therefore be extended as well. Initially, Zenon tries to close a branch by looking for two formulas P and ¬P that can be unified by a substitution σ (over metavariables), and this substitution σ is then used in the γ ∀inst /γ ¬∃inst rules corresponding to the unified metavariables. In deduction modulo, this method must be extended as follows: we look for two formulas P and Q s.t. P = RE P ′ , Q = RE ¬Q ′ , and there exists a substitution σ s.t. σ(P ′ ) = E σ(Q ′ ). To be complete, we must also extend this metavariable instantiation search to any propositional narrowing (even if we are Closure and Cut Rules not trying to close a branch): we look for a formula P and a substitution σ s.t. P = RE P ′ , and there exist P ′ |ω and a rule l -→ r of R ∪ E s.t. σ(P ′ |ω ) = E σ(l).

P ¬Q ⊙ if P = RE Q ⊙ cut if P = RE Q P | ¬Q P ⊙ ⊥ if P = RE ⊥ ⊙ ¬P ⊙ ¬⊤ if P = RE ⊤ ⊙ ¬P ⊙r if P = RE Rr (t,t) ⊙ P ¬Q ⊙s if P = RE Rs(a,b) and Q = RE Rs(b,a) ⊙ Analytic Rules S α∧ if S = RE P ∧Q P, Q ¬S β¬∧ if S = RE P ∧Q ¬P | ¬Q S β∨ if S = RE P ∨Q P | Q ¬S α¬∨ if S = RE P ∨Q ¬P, ¬Q S β⇒ if S = RE P ⇒Q ¬P | Q ¬S α¬⇒ if S = RE P ⇒Q P, ¬Q S β⇔ if S = RE P ⇔Q ¬P, ¬Q | P, Q ¬S β¬⇔ if S = RE P ⇔Q ¬P, Q | P, ¬Q ¬S ᬬ if S = RE ¬P P S δ ∃ if S = RE ∃x P (x) P (ǫ(x).P (x)) ¬S δ ¬∀ if S = RE ∀x P (x) ¬P (ǫ(x).¬P (x)) γ-Rules S γ ∀M if S = RE ∀x P (x) P (X) ¬S γ ¬∃M if S = RE ∃x P (x) ¬P (X) S γ ∀inst if S = RE ∀x P (x) P (t) ¬S γ ¬∃inst if S = RE ∃x P (x) ¬P (t)

Implementation and Experimental Results

In this section, we present our implementation of the extension of Zenon to deduction modulo, as well as a heuristic to transform an axiomatic theory into a theory modulo automatically. We also discuss the results obtained on the benchmarks provided by the TPTP library, and we detail a problem that is difficult according to the TPTP ranking, and whose proof is found by our extension.

sym if P (s,t) = RE Rs(s,t) and Q(u,v) = RE Rs(u,v) t = u | s = v ¬P (s, t) ¬refl if P (s,t) = RE Rr (s,t) s = t P (s, t) ¬Q(u, v) trans if P (s,t) = RE R t (s,t) and Q(u,v) = RE R t (u,v) u = s, ¬Rt(u, s) | t = v, ¬Rt(t, v) P (s, t) ¬Q(u, v) transsym if P (s,t) = RE R ts (s,t) and Q(u,v) = RE R ts (u,v) v = s, ¬Rts(v, s) | t = u, ¬Rts(t, u) P (s, t) ¬Q(u, v) transeq if P (s,t) = RE (s=t) and Q(u,v) = RE R t (u,v) u = s, ¬Rt(u, s) | ¬Rt(u, s), ¬Rt(t, v) | t = v, ¬Rt(t, v) P (s, t) ¬Q(u, v) transeqsym if P (s,t) = RE (s=t) and Q(u,v) = RE R ts (u,v) v = s, ¬Rts(v, s) | ¬Rts(v, s), ¬Rts(t, u) | t = u, ¬Rts(t, u)

Implementation

The extension of Zenon to deduction modulo described in Sec. 3 has been implemented in a tool called Zenon Modulo 4 . In this implementation, the class rewrite system RE is assumed to be a pure rewrite system, i.e. there are only rewrite rules and no equational axiom in E. In addition, the rewrite relation -→ RE is assumed to be confluent and (weakly) terminating, and the relation = RE is therefore decidable (see Prop. 1 in Sec. 3). Thus, given two propositions P and Q, it is sufficient to compare their normal forms (w.r.t. -→ RE ) to decide whether P = RE Q. A solution to deal with the relation = RE is then to normalize all the formulas of the proof search tree. However, this solution is not efficient in general, as it may perform many useless rewritings. To alleviate this problem, we use an alternate (but equivalent) solution, which consists in performing rewriting only if the formula is a literal. In this case, the terms of the formula are normalized, and one step of proposition rewriting is then applied; if the obtained formula is still a literal, the process is reiterated.

To generate the rewrite system R ∪ E, we have implemented two options. With the first one, the user builds a theory modulo (with axioms and rewrite rules) and provides this theory to Zenon Modulo through an extension of the TPTP input syntax [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF], which is one of the input formats used by Zenon, to natively support rewrite rules. With the second option, the user provides a purely axiomatic theory and Zenon Modulo transforms it into a theory modulo automatically. This transformation relies on a heuristic described in Subsec. 4.2.

Zenon Modulo is still in an early stage of development and some features have not been implemented yet. In particular, this is the case of the narrowing for terms and propositions. As a consequence, this leads to incompleteness cases, some of which arise in the benchmarks presented in this paper.

A Heuristic to Build Theories Modulo

To obtain a theory modulo from an axiomatic theory automatically, we propose a heuristic that generates rewrite rules from axioms based on the shape of the latter. In general, this heuristic does not preserve cut-free completeness. Here are the shapes of axioms that can be handled by our heuristic, as well as the rewrite rules that are generated from them (in the following P is an atomic formula that is not an equation, ϕ an arbitrary formula, and s and t two terms):

-Axiom of the form ∀x (P ⇔ ϕ): the proposition rewrite rule P -→ ϕ is generated if FV(ϕ) ⊆ FV(P ), otherwise if ϕ is a literal and FV(P ) ⊂ FV(ϕ) then we apply the heuristic to the formula ∀x (ϕ ⇔ P ); -Axiom of the form ∀x (¬P ⇔ ϕ): the proposition rewrite rule P -→ ¬ϕ is generated if FV(ϕ) ⊆ FV(P ), otherwise if ϕ is a literal and FV(P ) ⊂ FV(ϕ) then we apply the heuristic to the formula ∀x (ϕ ⇔ ¬P ); -Axiom of the form ∀x s = t: the term rewrite rule s -→ t is generated if FV(t) ⊆ FV(s), otherwise the term rewrite rule t -→ s if FV(s) ⊂ FV(t).

In addition, all the axioms expressing the commutativity of a given symbol are excluded from this rule of our heuristic.

In this heuristic, it should be noticed that we exclude the axioms where P is an equation in order to benefit from the equational reasoning of Zenon. To illustrate this heuristic, an example is provided in Subsec. 4.4, where it is shown how a part of the theory is transformed into rewrite rules automatically.

Experimental Results

We propose a test of our approach on a benchmark drawn from the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF] (v.5.5.0), which is a large library of standard benchmark examples for automated theorem proving systems. On this benchmark, we compare Zenon with two different heuristics of Zenon Modulo. The first heuristic consists in only selecting the axioms that can be transformed into proposition rewrite rules (equational axioms that can be transformed into term rewrite rules are ignored), while the second one is a greedy heuristic that transforms every axiom that matches one of the patterns described above, producing both term and propositional rewrite rules. The results of this experiment (run on an Intel Xeon X5650 2.67GHz computer, with a memory limit of 1GB and a timeout of 300s) are summarized in Tab. 1, where we have considered the first order problems of the whole library (FOF category) and the problems of set theory (SET category). This table has three columns: the first one provides the number of problems proved by Zenon for each category, while the two other columns show the results of Zenon Modulo with each of the heuristics described above. For Zenon Modulo, there are three numbers per category and heuristic: the left-hand side number is the number of problems proved by Zenon Modulo, while the two right-hand side numbers represent, from top to bottom, the number of problems proved by Zenon Modulo but not by Zenon, and the number of problems proved by Zenon but not by Zenon Modulo.

From the results of Tab. 1, we observe that Zenon Modulo always proves more problems than Zenon whatever the considered category and the selected heuristic. If the gain seems to be low for the whole FOF category (less than 3%) in spite of a significant proportion of problems proved by Zenon Modulo but not by Zenon (about 7% and 11% depending on the heuristic), this is essentially due to incompleteness cases of Zenon Modulo, where narrowing is actually required and for which Zenon succeeds in finding a proof (about 5% and 9% of the cases depending the heuristic). Once narrowing will have been implemented, we can reasonably hope to drastically reduce the number of these cases, and obtain a quite higher gain (probably up to about 11% in the best case scenario).

However, even without narrowing, the gain of Zenon Modulo becomes quite significant for the SET category (about 50% for both heuristics). This very promising result in the SET category tends to show that set theory is a good candidate for automated reasoning with deduction modulo, even when using an automated heuristic. Moreover, as said in the introduction, we plan to apply Zenon Modulo in the context of the B method [START_REF] Hermant | The B-Book, Assigning Programs to Meanings[END_REF], in particular to verify proof obligations coming from industrial applications. This is one of the tasks of the BWare project [START_REF]The BWare Project[END_REF]. As the modeling technique used by the B method relies on a customized set theory, which will have a hand-tailored expression as a rewrite system, we can therefore be quite confident in the effectiveness of our tool in the verification of these proof obligations.

The results of the two instances of Zenon Modulo are close, but the heuristic based on term and proposition rewriting proves more problems that are not proved by Zenon (about 11% for FOF and 58% for SET), and once narrowing will be implemented, this heuristic should therefore be preferred.

It should be also noticed that among the 86 problems of the SET category proved by Zenon Modulo (with the heuristic based on and proposition rewriting) but not by Zenon, there are 29 difficult problems according to the TPTP ranking, namely 29 with a ranking greater than 0.75 , 9 with a ranking greater than 0.8, and 1 with a ranking greater than 0.9.

A Nontrivial Example from the TPTP Library

To show the effectiveness of Zenon Modulo, let us describe the proof found for the problem SET815+4, which has the highest ranking (0.91) among those solved, and which deals with the theory of ordinal numbers. The conjecture states that any ordinal number is equal to the union of the elements of its successor. The axioms used to complete this proof are the following:

∀A, B (A ⊆ B ⇔ ∀X (X ∈ A ⇒ X ∈ B)) (subset) ∀A, B (A = set B ⇔ A ⊆ B ∧ B ⊆ A) (eqset) ∀X, A, B (X ∈ A ∪ B ⇔ X ∈ A ∨ X ∈ B) (union) ∀X, A (X ∈ {A} ⇔ X = A) (singleton) ∀X, A (X ∈ A ⇔ ∃Y (Y ∈ A ∧ X ∈ Y )) (sum) ∀A (A ∈ On ⇔ set(A) ∧ ∀X (X ∈ A ⇒ X ⊆ A) ∧ (ordinal ) strict_wo(mem_pred, A)) ∀X, A (X ∈ A + 1 ⇔ X ∈ A ∪ {A}) (successor )
where set is a predicate that requires the argument to be a set, and where On is the "set" of ordinal numbers, mem_pred the membership relation over ordinal numbers (this relation is related to ∈ by means of an axiom not shown here as it is not required to complete the proof), and strict_wo a formula encoding the strict well-order relation.

According the rules of the heuristic described in Subsec. 4.2, all these axioms can be turned into proposition rewrite rules (we use the first rule of the heuristic, and each axiom is oriented from left to right). Once this theory modulo has been built, we can then try to prove the conjecture, which is expressed as follows:

∀A (A ∈ On ⇒ (A + 1) = set A) ¬(∀A (A ∈ On ⇒ (A + 1) =set A)) l1 ¬( (τ1 + 1) ⊂ τ1 ∧ τ1 ⊂ (τ1 + 1)), ∀X (X ∈ τ1 ⇒ X ⊂ τ1) l2 ¬(∀X (X ∈ (τ1 + 1) ⇒ X ∈ τ1)) l3 Π1 ¬(∀X (X ∈ τ1 ⇒ X ∈ (τ1 + 1))) l4 Π2 Π1 τ3 ∈ τ1 ∨ τ3 ∈ {τ1}, ¬(τ2 ∈ τ1), τ2 ∈ τ3 l5 τ3 ∈ τ1 l6 τ3 ∈ τ1 ⇒ τ3 ⊂ τ1 l7 ¬(τ3 ∈ τ1) ⊙ ⊙ ∀X (X ∈ τ3 ⇒ X ∈ τ1) l8 τ2 ∈ τ3 ⇒ τ2 ∈ τ1 l9 ¬(τ2 ∈ τ3) ⊙ ⊙ τ2 ∈ τ1 ⊙ ⊙ τ3 = τ1 l10 τ2 = τ2 ⊙r ⊙ τ3 = τ1 ⊙ ⊙ Π2 ¬(∃Y (Y ∈ (τ1 + 1) ∧ τ4 ∈ Y )), τ4 ∈ τ1 l11 ¬(τ1 ∈ (τ1 + 1) ∧ τ4 ∈ τ1) l12 τ1 = τ1 ⊙r ⊙ ¬(τ4 ∈ τ1) ⊙ ⊙
where : When applied to this specification, Zenon Modulo produces the (rather short) proof of Fig. 3. The proof is presented using the rules of Sec. 3, even though these rules are more used for proof search rather than for proof presentation (for that purpose, Zenon actually uses an intermediate format, which is described in detail in [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF]). Moreover, to make the presentation more compact, one proof step may consist of several rules. Notice the clever instantiation rule l 6 , which cannot be done before the δ ∃ of l 3 .

τ1 = ǫ(A).¬(A ∈ On ⇒ (A + 1) = A) τ2 = ǫ(X).¬(X ∈ (τ1 + 1) ⇒ X ∈ τ1) τ3 = ǫ(Y ).(Y ∈ (τ1 + 1) ∧ τ2 ∈ Y ) τ4 = ǫ(X).¬(X ∈ τ1 ⇒ X ∈ (τ1 + 1)) l1 = δ ¬∀ , α¬⇒, ordinal, eqset l2 = β¬∧, subset l3 = δ ¬∀ , α¬⇒, sum, δ ∃ , α∧, successor, union l4 = δ ¬∀ , α¬⇒, sum l5 = β∨, singleton l6 = γ ∀inst l7 = β⇒, subset l8 = γ ∀inst l9 = β⇒ l10 = pred l11 = γ ¬∃inst l12 = β¬∧,

Proof Verification with Dedukti

In this section, we describe the Dedukti backend that has been implemented for Zenon Modulo, and which relies in particular on a proof transformation from classical to constructive logic.

Dedukti as a Backend for Deduction Modulo

Skeptically checking proof traces produced by an automated theorem prover imposes that the traces contain all the information needed by the proof checker to assert the validity of proofs. A naive way to check proofs performed by Zenon Modulo would be to record rewriting as a special rule, but this method would be very expensive in space, because an arbitrary number of rewrite rules can occur between any consecutive nodes of the proof. To circumvent this problem, the proof checker or the formalization of the proof must not distinguish propositions or terms belonging to the same equivalence class modulo rewriting. The only information needed is the set of rewrite rules, which cannot be bigger than the problem statement itself. Dedukti fits this specific constraint in a simple way: if the set of rewrite rules is translated into Dedukti rewrite rules specified in the header of the proof, any proposition or term used in the proof can be replaced by an equivalent proposition or term modulo rewriting.

Dedukti [START_REF] Boespflug | The λΠ-Calculus Modulo as a Universal Proof Language[END_REF] is a type checker for the λΠ-calculus modulo, which is an extension of the λ-calculus with dependent types and rewrite rules. In order to check proofs of a given logical system, we have to define an embedding of this system into the λΠ-calculus modulo. A logical system is embedded into the λΠ-calculus modulo using declarations of constants and declarations of rewrite rules. As an example, let us consider the implicative fragment of natural deduction and a predicate P . To encode this example, we provide the context of Fig. 4, where the syntax of λΠ-calculus modulo is used. In this context, we can check the trivial proof of Imp P P by verifying that the term Intro P P (λt : (Proof P ). t) has type Proof (Imp P P ). This technique, which consists in defining rules as constants in the λΠ-calculus modulo, is called deep embedding.

However, the λΠ-calculus modulo allows us to define rewrite rules that avoid the definitions of the previous encoding and therefore get shorter proofs. For example, we can replace the Intro and Elim constants by the rewrite rule Proof (Imp A B) -→ (Proof A → Proof B), where A and B are variables of type Prop. The previous term then reduces to λt : (Proof P ).t, which has the same type. This technique, which consists in reusing the language features (here, the λΠ-calculus modulo) is called shallow embedding. In particular, the compu- The definition of an output to deduction modulo first consists in providing the declaration of the language (terms, predicates, connectives, etc.), and the shallow embedding of the natural deduction rules that is close to λΠ-calculus.

We then proceed to the definition of the rewrite rules for propositions and terms, according to the input set of rewrite rules. Once this encoding has been defined, proofs can be checked in this context. As an example, we can extend the previous encoding with a predicate Q and two axioms Imp Q (Imp P P ) and Imp (Imp P P ) Q. The heuristic of Sec. 4 will replace these two axioms by a single rewrite rule (these two axioms represent an equivalence), and we just have to declare the rewrite rule Q -→ Imp P P , modulo which Q admits the same proof as before, i.e. λt : (Proof P ).t.

From Classical to Constructive Proofs

Zenon's logic is classical and expressed in a formalism very close to sequent calculus [START_REF] Troelstra | Basic Proof Theory[END_REF]. As a consequence, using Dedukti as a backend requires two steps: the first one is to translate classical proofs of Zenon into proofs of constructive sequent calculus with equality, which we discuss here, and the second one is a standard translation from sequent calculus to natural deduction.

The translation from classical to constructive logic relies on an optimized double-negation translation [START_REF] Troelstra | Constructivism in Mathematics: An Introduction[END_REF], presented in Tab. 2, where other connectives (¬ and ⊤) are defined as usual through ⇒ and ⊥. With these definitions, it is possible to show that a formula A has a classical proof if and only if ϕ(A) has a constructive proof. The purpose of defining the three functions of Tab. 2 is that the algorithm introduces a minimal number of double negations. In particular, we improve over both Kuroda's and Gödel's translations [START_REF] Troelstra | Constructivism in Mathematics: An Introduction[END_REF] by combining their principles: double negation only after universal quantifiers and double negation only in front of disjunctive and existentially quantified propositions, respectively. At top level, we push double negations as far as possible inside the formula, as Gödel, in front of the first encountered disjunction/existential quantifier (the role of ϕ); at this point, we stop introducing double negations until, as Kuroda, we meet a universal quantifier, in which case we start again the process (the role of ψ). We refine our translation with the polarity of formulas (i.e. the side of the sequent on which the formula appears): if a formula appears on the left-hand side of a sequent, we do not put a double-negation in front of it (the role of χ).

Furthermore, the algorithm analyses the structure of the classical proof in order to remove more double negations. For instance, a disjunction can be proved constructively even in a classical calculus. As a consequence, the statement of many proofs remains unchanged. This is the case of the TPTP problem SET815+4, discussed in Sec. 4, whose proof certificate (expressed in λΠ-calculus modulo), is given in Figs. 5 and6 of Appx. A. This algorithm of proof transformation has been implemented for Zenon Modulo to produce Dedukti proof certificates. In particular, Zenon Modulo succeeds in producing a proof certificate for the previous problem SET815+4, which is correctly checked by Dedukti.

Conclusion

We have proposed an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. This extension essentially consists in considering a part of a given theory as rewrite rules (over terms and propositions), and integrating these rewrite rules into the proof search rules of Zenon. We have also presented an implementation of this extension, called Zenon Modulo, as well as a heuristic to turn axioms of theories into rewrite rules automatically. This new tool significantly improves the proof search of Zenon, as shown by the experimental results obtained on the benchmarks provided by the TPTP library.

In particular, this is the case of the SET category, where Zenon Modulo is able to prove difficult problems according to the TPTP ranking. Finally, we have also described an additional backend for Zenon that outputs proof certificates for Dedukti, which is a proof checker based on the λΠ-calculus modulo.

As future work, we first aim to complete our implementation to deal with narrowing when trying to find instantiations for metavariables. This will allow us to ensure completeness for our extension of Zenon, even though narrowing may paradoxically widen the proof search space in some cases (e.g., in set theory, a metavariable representing a set can be "narrowed" using the major part of rewrite rules defining the set operators). To deal with these cases, we will probably implement a switch that will allow us to activate/deactivate the use of narrowing. It might be also desirable to extend our proof search method to polarized deduction modulo [START_REF] Dowek | What is a Theory?[END_REF], which is a refinement of deduction modulo to deal with theories formed with axioms using implications. This extension would allow us to consider more theories, where a significant part of the axioms are expressed neither by equivalences, nor by equations, but only by implications. Finally, in the framework of the BWare project [START_REF]The BWare Project[END_REF], we plan to apply this tool in the context of the B method [START_REF] Hermant | The B-Book, Assigning Programs to Meanings[END_REF], with in particular the verification of proof obligations coming from industrial applications. To achieve this task, we have to build a theory modulo for the modeling method of B, which is actually a typed set theory, and we should be able to reuse some ideas of [START_REF] Jacquel | Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover[END_REF], where a B set theory is proposed using superdeduction. Given the very promising results of our tool in the SET category of the TPTP library, we are quite confident in the effectiveness of our tool in the verification of B proof obligations.

Proposition 1 (

 1 Decidability of = RE ). If the rewrite relation -→ RE is confluent and (weakly) terminating, then the relation = RE is decidable.

Fig. 1 .

 1 Fig. 1. Deduction Modulo Rules for Zenon (Part 1)

Fig. 2 .

 2 Fig. 2. Deduction Modulo Rules for Zenon (Part 2)

Fig. 3 .

 3 Fig. 3. Proof of Problem SET815+4

Fig. 4 .

 4 Fig. 4. Encoding of Natural Deduction in λΠ-Calculus Modulo

  ) ∧ ϕ(B) χ(A) ∧ χ(B) ψ(A) ∧ ψ(B) A ∨ B ¬¬(ψ(A) ∨ ψ(B)) χ(A) ∨ χ(B) ψ(A) ∨ ψ(B) A ⇒ B χ(A) ⇒ ϕ(B) ψ(A) ⇒ χ(B) χ(A) ⇒ ψ(B) ∀x A ∀x ϕ(A) ∀x χ(A) ∀x ϕ(A)

Table 1 .

 1 Experimental Results over the TPTP Library

	TPTP Category	Zenon	Zenon Modulo (Prop. Rewriting)	Zenon Modulo (Term & Prop. Rewriting)
	FOF 6,659 problems	1,586	1,626 (2.5%)	+114 (7.2%) -74 (4.7%)	1,616 (1.9%)	+170 (10.7%) -140 (8.8%)
	SET 462 problems	149	219 (47%)	+78 (52.3%) -8 (5.4%)	222 (49%)	+86 (57.7%) -13 (8.7%)

Table 2 .

 2 Translation from Classical to Constructive Logic

Available on demand (sending a mail to the authors).

It means that at least 70% of the tested automated theorem provers fail in proving the considered problems.

Acknowledgement. Many thanks to G. Dowek, F. Irigoin, and P. Jouvelot for their detailed comments on this paper, to G. Burel for helpful discussions, and to the Deducteam Inria research team for the many interactions.

⋆ This work is supported by the BWare project [13] (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR).

Rewrite Rules:

where [•] is the typing context of a rewrite rule.