Mélanie Jacquel
email: melanie.jacquel@siemens.com

Karim Berkani
email: karim.berkani@siemens.com

David Delahaye
email: david.delahaye@cnam.fr

Catherine Dubois
email: dubois@ensiie.fr

Karim

Tableaux Modulo Theories Using Superdeduction

Keywords: Automated Deduction, Tableaux, Superdeduction, Zenon, Set Theory, B Method, First Order Theories

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

Reasoning modulo a theory like arithmetic in first order logic may appear as a complex task, since even simple formulas become difficult to be proved (using natural deduction or sequent calculus), and the corresponding proofs are hardly readable. This is actually due to the fact that Gentzen's deductive systems, even if more elaborate than systems à la Hilbert, consist of low-level languages for deduction. Over the last few years, several approaches have been developed to palliate this problem, and for instance, deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] and superdeduction [START_REF] Brauner | Principles of Superdeduction[END_REF], which respectively focus on the computational and deductive parts of a theory, can be considered as steps toward high-level deductive languages.

Superdeduction has been adapted for usual deductive systems, such as natural deduction or sequent calculus (see [START_REF] Brauner | Principles of Superdeduction[END_REF], for example). In these systems, we have to deal with some common permutability problems of automated proof search, since superdeduction systems are in fact embedding a part of compiled automated deduction. As a consequence, superdeduction can be naturally integrated into automated deduction methods, and we propose to do so in the framework of the tableau method (this corresponds to an alternative approach to the work described in [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF], where a tableau method for deduction modulo is proposed).

The integration of superdeduction into the tableau method is actually motivated by an experiment that is managed by Siemens IC-MOL regarding the verification of B proof rules [START_REF] Jacquel | Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving[END_REF]. The B method [START_REF] Karim | The B-Book: Assigning Programs to Meanings[END_REF], or B for short, allows engineers to develop software with high guarantees of confidence; more precisely it allows them to build correct by design software. B is a formal method based on set theory and theorem proving, and which relies on a refinement-based development process. The Atelier B environment [START_REF][END_REF] is a platform that supports B and offers, among other tools, both automated and interactive provers. In practice, to ensure the global correctness of formalized applications, the user must discharge proof obligations. These proof obligations may be proved automatically, but otherwise, they have to be handled manually either by using the interactive prover, or by adding new proof rules that the automated prover can exploit. These new proof rules can be seen as axioms and must be verified by other means, otherwise the global correctness may be endangered.

In [START_REF] Jacquel | Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving[END_REF], we develop an approach based on the use of the Zenon automated theorem prover [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF], which relies on classical first order logic with equality and applies the tableau method as proof search. In this context, the choice of Zenon is strongly influenced by its ability of producing comprehensible proof traces under the form of Coq proofs [START_REF]Coq, version 8.4pl4. Inria[END_REF] in particular. The method used in this approach consists in first normalizing the formulas to be proved, in order to obtain first order logic formulas containing only the membership set operator, and then calling Zenon on these new formulas. This experiment gives satisfactory results in the sense that it can prove a significant part of the rules coming from the database maintained by Siemens IC-MOL (we can deal with about 1,400 rules, 1,100 of which can be proved automatically, over a total of 5,300 rules). However, this approach is not complete (after the normalization, Zenon proves the formulas without any axiom of set theory, while some instantiations may require to be normalized), and suffers from efficiency issues (due to the preliminary normalization). To deal with these problems, the idea developed in this paper is to integrate the axioms and constructs of the B set theory into the Zenon proof search method by means of superdeduction rules. This integration can be concretely achieved thanks to the extension mechanism offered by Zenon, which allows us to extend its core of deductive rules to match specific requirements.

In this paper, we also propose another extension of Zenon with superdeduction, which is able to deal with any first order theory, and which must be seen as a generalization of the extension of Zenon with superdeduction and for the B set theory that has been described previously. This other extension of Zenon has been developed as a tool called Super Zenon [START_REF] Jacquel | Super Zenon, version 0.0.1. Siemens and Cnam[END_REF], where each theory is analyzed to determine the axioms which can be turned into superdeduction rules, and these superdeduction rules are automatically computed on the fly to enrich the deductive kernel of Zenon.

The paper is organized as follows: in Sec. 2, we start by briefly reviewing some related work; in Secs. 3 and 4, we then respectively introduce superdeduction and present the computation of superdeduction rules from axioms in the framework of the tableau method used by Zenon; next, we explain, in Sec. 5, the superdeduction rules corresponding to the set theory which the B method relies on, and describe, in Sec. 6, the implementation of our extension of Zenon for the B set theory and provide some comparative benchmarks concerning the verification of B proof rules coming from the database maintained by Siemens IC-MOL; thereafter, in Sec. 7, we present the other extension of Zenon with superdeduction, which is able to deal with any first order theory, and also provide a comparative benchmark coming from the TPTP library, which contains a large set of first order problems in particular; finally, in Sec. 8, we discuss more generally the use of superdeduction for proof search in axiomatic theories.

Related Work

In the framework of verification of B (or Event-B) proof obligations, and in addition to B dedicated provers, such as the main prover of Atelier B, some similar work has been done to use external provers, relying on either SMT (Satisfiability Modulo Theories) solvers like veriT [START_REF] Déharbe | Integration of SMT-Solvers in B and Event-B Development Environments[END_REF], or proof assistants like Coq [START_REF] Colin | BRIL-LANT: An Open Source and XML-based platform for Rigourous Software Development[END_REF] or Isabelle/HOL [START_REF] Schmalz | Term Rewriting in Logics of Partial Functions[END_REF]. However, veriT does not provide proof traces, and automation is poor in the considered proof assistants, even though dedicated tactics are offered. More generally, there are also some provers covering set theory, such as Muscadet [START_REF] Pastre | Strong and Weak Points of the Muscadet Theorem Prover -Examples from CASC-JC[END_REF] or Theorema [START_REF] Windsteiger | An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema[END_REF], but they do not provide traces either.

Regarding the ability of reasoning modulo theories, there exist some alternative approaches, such as the technology of SMT solvers. This technology is based on a SAT solver and a combination of several decision procedures for several theories. There are several methods to combine the considered decision procedures, such as the Nelson-Oppen [START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF] or Shostak [START_REF] Shostak | Deciding Combinations of Theories[END_REF] methods. The approach used by SMT solvers is actually restrictive in the sense that the considered theories have to be decidable. To preserve this decidability, the combination methods also impose some restrictions over the theories to be combined, which must have disjoint signatures. The techniques of deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] and superdeduction [START_REF] Brauner | Principles of Superdeduction[END_REF], proposed in this paper in particular, are more general approaches to integrate theories into proof search methods since there is no constraint over the theories to be integrated, which may be decidable or not.

Rationale for Superdeduction

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. Superdeduction [START_REF] Brauner | Principles of Superdeduction[END_REF] is actually a variant of deduction modulo, where axioms are used to enrich the deduction system with new deduction rules, which are called superdeduction rules. For example, considering the definition of inclusion in set theory ∀a∀b ((a ⊆ b) ⇔ (∀x (x ∈ a ⇒ x ∈ b))), 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 ∀a∀b ((a ⊆ b) ⇔ (∀x (x ∈ a ⇒ x ∈ b))) ⊢ A ⊆ A
In deduction modulo, the axiom of inclusion can be seen as a computation rule and therefore replaced by the rewrite rule a ⊆ b → ∀x (x ∈ a ⇒ x ∈ b). 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
It can be noticed that the obtained proof is much simpler than the one completed using sequent calculus. In addition to simplicity, deduction modulo also allows us for unbounded proof size speed-up [START_REF] Burel | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo[END_REF].

Superdeduction proposes to go further than deduction modulo precisely when the considered axiom defines a predicate P with an equivalence ∀x (P ⇔ ϕ). While deduction modulo replaces the axiom by a rewrite rule, superdeduction adds to this transformation the decomposition of the connectives occurring in this definition. This corresponds to an extension of Prawitz's folding (resp. unfolding) rules [START_REF] Prawitz | Natural Deduction. A Proof-Theoretical Study[END_REF], where a maximum of connectives of the definition are introduced (resp. eliminated). Superdeduction may be seen as the alliance of deduction modulo with focusing, which is a technique initially introduced in the framework of linear logic [START_REF] Andreoli | Logic Programming with Focusing Proofs in Linear Logic[END_REF]. For the axiom of inclusion, the proposed superdeduction rule is therefore the following (there is also a corresponding left rule):

Γ , x ∈ a ⊢ x ∈ b, ∆ IncR, x ∈ Γ , ∆ Γ ⊢ a ⊆ b, ∆
Hence, proving A ⊆ A with this new rule can be performed as follows:

Ax x ∈ A ⊢ x ∈ A IncR ⊢ A ⊆ A
This new proof is not only simpler and shorter than in deduction modulo, but also follows a natural human reasoning scheme usually used in mathematics (in the same vein, see [START_REF] Delahaye | Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction[END_REF] for more details about how superdeduction allows us to recover intuition from automated proofs).

From Axioms to Superdeduction Rules

As mentioned previously, reasoning modulo a theory in a tableau method using superdeduction requires to generate new deduction rules from some axioms of the theory. The axioms which can be considered for superdeduction are of the form ∀x (P ⇔ ϕ), where P is atomic. This specific form of axiom allows us to introduce an orientation of the axiom from P to ϕ, and we introduce the notion of proposition rewrite rule (this notion appears in [START_REF] Brauner | Principles of Superdeduction[END_REF], from which we borrow the following definition and notation):

Definition 1 (Proposition Rewrite Rule). The notation R : P → ϕ denotes the axiom ∀x (P ⇔ ϕ), where R is the name of the rule, P an atomic proposition, ϕ a proposition, and x the free variables of P and ϕ.

It should be noted that P may contain first order terms and therefore that such an axiom is not just a definition. For instance, x ∈ a ∩ b → x ∈ a ∧ x ∈ b (where a ∩ b is a first order term) is a proposition rewrite rule.

As said in the introduction, one of our main objectives is to develop a proof search procedure for the set theory of the B method using the Zenon automated theorem prover [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF]. In the following, we will thus consider the tableau method used by Zenon as the framework in which superdeduction rules will be generated from proposition rewrite rules.

The proof search rules of Zenon are described in detail in [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] and summarized in Fig. 1 (for the sake of simplification, we have omitted the unfolding and extension rules), where ǫ is Hilbert's operator (ǫ(x).P (x) means some x that satisfies P (x), 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 the equality in particular). 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; they are not used as variables as they are never substituted. The proof search rules are applied with the normal 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 an application of a closure rule), the tree is closed, and this closed tree is a proof of the goal. Note that this algorithm is applied in strict depth-first order: we close the current branch before starting work on another branch. Moreover, we work in a non-destructive way: working on one branch will never change the formulas of any other branch. We divide these rules into five distinct classes to be used for a more efficient proof search. This extends the usual sets of rules dealing with α, β, δ, γ-formulas and closure (⊙) with the specific rules of Zenon. We list below the five sets of rules and their elements:

α α ¬∨ , α ∧ , α ¬⇒ , α ¬¬ , ¬ refl β β ∨ , β ¬∧ , β ⇒ , β ⇔ , β ¬⇔ , pred, fun, sym, trans * δ δ ∃ , δ ¬∀ γ γ ∀M , γ ¬∃M , γ ∀inst , γ ¬∃inst ⊙ ⊙ ⊤ , ⊙ ⊥ , ⊙, ⊙ r , ⊙ s
where "trans * " gathers all the transitivity rules.

Closure and Cut Rules

⊥ ⊙ ⊥ ⊙ ¬⊤ ⊙ ¬⊤ ⊙ cut P | ¬P ¬Rr(t, t) ⊙r ⊙ P ¬P ⊙ ⊙ Rs(a, b) ¬Rs(b, a) ⊙s ⊙ Analytic Rules ¬¬P ᬬ P P ⇔ Q β⇔ ¬P, ¬Q | P, Q ¬(P ⇔ Q) β¬⇔ ¬P, Q | P, ¬Q P ∧ Q α∧ P, Q ¬(P ∨ Q) α¬∨ ¬P, ¬Q ¬(P ⇒ Q) α¬⇒ P, ¬Q P ∨ Q β∨ P | Q ¬(P ∧ Q) β¬∧ ¬P | ¬Q P ⇒ Q β⇒ ¬P | Q ∃x P (x) δ ∃ P (ǫ(x).P (x)) ¬∀x P (x) δ ¬∀ ¬P (ǫ(x).¬P (x)) γ-Rules ∀x P (x) γ ∀M P (X) ¬∃x P (x) γ ¬∃M ¬P (X) ∀x P (x) γ ∀inst P (t) ¬∃x P (x) γ ¬∃inst ¬P (t)
Relational Rules P (t1, ..., tn) ¬P (s1, .., sn) pred Let us now describe how the computation of superdeduction rules for Zenon is performed from a given proposition rewrite rule.

t1 = s1 | ... | tn = sn f (t1, ..., tn) = f (s1, ..., sn) fun t1 = s1 | ... | tn = sn Rs(s, t) ¬Rs(u, v) sym t = u | s = v ¬Rr(s, t) ¬ refl s = t Rt(s, t) ¬Rt(u, v) trans u = s, ¬Rt(u, s) | t = v, ¬Rt(t, v) Rts(s, t) ¬Rts(u, v) transsym v = s, ¬Rts(v, s) | t = u, ¬Rts(t, u) s = t ¬Rt(u, v) transeq u = s, ¬Rt(u, s) | ¬Rt(u, s), ¬Rt(t, v) | t = v, ¬Rt(t, v) s = t ¬Rts(u, v) transeqsym v = s, ¬Rts(v, s) | ¬Rts(v, s), ¬Rts(t, u) | t = u, ¬Rts(t, u)
Definition 2 (Computation of Superdeduction Rules). Let S be a set of rules composed by the subset of the proof search rules of Zenon formed of the closure rules, the analytic rules, as well as the γ ∀M and γ ¬∃M rules. Given a proposition rewrite rule R : P → ϕ, two superdeduction rules (a positive one R and a negative one ¬R) are generated in the following way: 1. To get the positive rule R, initialize the procedure with the formula ϕ. Next, apply the rules of S until there is no open leaf anymore on which they can be applied. Then, collect the premises and the conclusion, and replace ϕ by P to obtain the positive rule R. 2. To get the negative rule ¬R, initialize the procedure with the formula ¬ϕ.

Next, apply the rules of S until there is no open leaf anymore on which they can be applied. Then, collect the premises and the conclusion, and replace ¬ϕ by ¬P to obtain the negative rule ¬R.

If the rule R (resp. ¬R) involves metavariables, an instantiation rule R inst (resp. ¬R inst ) is added, where one or several metavariables can be instantiated.

Integrating these new deduction rules to the proof search rules of Zenon is trivially correct as they are generated from a subset of the rules of Zenon, while the considered subset of rules only consists of reversible rules, which is a necessary condition for completeness.

Let us illustrate the computation of superdeduction rules from a proposition rewrite rule with the example of the set inclusion.

Example 1 (Set Inclusion).

From the definition of the set inclusion, we introduce the proposition rewrite rule Inc : a ⊆ b → ∀x (x ∈ a ⇒ x ∈ b), and the corresponding superdeduction rules Inc and ¬Inc are generated as follows:

∀x (x ∈ a ⇒ x ∈ b) γ ∀M X ∈ a ⇒ X ∈ b β ⇒ X ∈ a | X ∈ b ¬∀x (x ∈ a ⇒ x ∈ b) δ ¬∀ ¬(ǫ x ∈ a ⇒ ǫ x ∈ b) α ¬⇒ ǫ x ∈ a, ǫ x ∈ b where ǫ x = ǫ(x).¬(x ∈ a ⇒ x ∈ b).
The resulting superdeduction rules are then the following:

a ⊆ b Inc X ∈ a | X ∈ b a ⊆ b Inc inst t ∈ a | t ∈ b a ⊆ b ¬Inc ǫ x ∈ a, ǫ x ∈ b

Superdeduction Rules for the B Set Theory

The purpose of this section is to build a superdeduction system for the B set theory, which can be used for the verification of proof rules of Atelier B, such as the rules coming from the database maintained by Siemens IC-MOL (see Sec. 6). To do so, the idea is to apply the computational algorithm of superdeduction rules described in Sec. 4 to the several axioms of the B set theory.

The B Set Theory

As said in the introduction, the B method [START_REF] Karim | The B-Book: Assigning Programs to Meanings[END_REF] aims to assist experts to develop certified software. The initial step is defined with abstract properties of a model. Several steps of property refinement are then applied until the release of the complete software. A refinement step is characterized by adding details on the software behavior under construction. For each step, generated proof obligations must be demonstrated to ensure the global correctness of the formalization.

The B method is based on a typed set theory. There are two rule systems: one for demonstrating that a formula is well-typed, and one for demonstrating that a formula is a logical consequence of a set of axioms. The main aim of the type system is to avoid inconsistent formulas, such as Russell's paradox for example. The B proof system is based on a sequent calculus with equality. Six axioms define the basic operators and the extensionality which, in turn, defines the equality of two sets. In addition, the other operators (∪, ∩, etc.) are defined using the previous basic ones. Fig. 2 gathers a part of the axioms and constructs of the B set theory, where BIG is an infinite set (mostly only used to build natural numbers in the foundational theory). In this figure, we only consider the four first axioms of the B set theory, as we do not need the two remaining axioms in the rules that we want to verify (see Sec. 6). Regarding functions and due to space restrictions, we only present the notion of partial function, even though we can deal with the other function constructs in our superdeduction system. Compared to [START_REF] Karim | The B-Book: Assigning Programs to Meanings[END_REF], all type information has been removed from the axioms and constructs. This can be done since typechecking is performed before proving a formula, and the pieces of type information dispersed throughout the axioms and constructs are useless when building a proof (see [START_REF] Abrial | On Using Conditional Definitions in Formal Theories[END_REF] for details regarding the modularity between the type and proof systems). Finally, we do not deal with substitution explicitly (see the axiom for comprehension sets, for example), as we do not intend to manage rules involving explicit substitutions (see Sec. 6).

Generating the Superdeduction Rules

To generate the superdeduction rules corresponding to the axioms and constructs defined in Fig. 2, we use the algorithm described in Def. 2 of Sec. 4, and we must therefore identify the several proposition rewrite rules. On the one hand, the axioms are all of the form P i ⇔ Q i , and the associated proposition rewrite rules are R i : P i → Q i , where each axiom is oriented from left to right. On the other hand, the constructs are expressed by the definitions E i F i , where E i and F i are expressions, and the corresponding proposition rewrite rules are

R i : x ∈ E i → x ∈ F i ; if E i
and F i represent relations, the proposition rewrite rules are R i : (x, y) ∈ E i → (x, y) ∈ F i , where we consider that relations are defined by means of ordered pairs. The superdeduction rules generated from this set of proposition rewrite rules are described in Figs. 3 and4. Due to space restrictions, we do not include the definitions of ⊆ (as well as ⊂), and • in these figures, but their rules can be respectively deduced from the rules of P and ";". For the same reasons, we do not describe the instantiation rules associated with

Axioms (x, y) ∈ a × b ⇔ x ∈ a ∧ y ∈ b a ∈ P(b) ⇔ ∀x (x ∈ a ⇒ x ∈ b) x ∈ { y | P (y) } ⇔ P (x) a = b ⇔ ∀x (x ∈ a ⇔ x ∈ b) Derived Constructs a ⊆ b ⇔ a ∈ P(b) a ⊂ b ⇔ a ⊆ b ∧ a = b a ∪ b { x | x ∈ a ∨ x ∈ b } a ∩ b { x | x ∈ a ∧ x ∈ b } a -b { x | x ∈ a ∧ x ∈ b } ∅ BIG -BIG { e1, . . . , en } { x | x = e1 } ∪ . . . ∪ { x | x = en } Binary Relation Constructs: First Series a ↔ b P(a × b) a -1 { (y, x) | (x, y) ∈ a } dom(a) { x | ∃y (x, y) ∈ a } ran(a) dom(a -1 ) a; b { (x, z) | ∃y ((x, y) ∈ a ∧ (y, z) ∈ b } a • b b; a id(a) { (x, y) | (x, y) ∈ a × a ∧ x = y } a ⊳ b id(a); b a ⊲ b a; id(b) a -⊳ b (dom(b) -a) ⊳ b a -⊲ b a ⊲ (ran(a) -b)
Binary Relation Constructs: Second Series

a[b] ran(b ⊳ a) a - ⊳ b (dom(b) -⊳ a) ∪ b a ⊗ b { (x, (y, z)) | (x, y) ∈ a ∧ (x, z) ∈ b } prj 1 (a, b) (id(a) ⊗ (a × b)) -1 prj 2 (a, b) ((b × a) ⊗ id(b)) -1 a || b { (x, y), (z, t) | (x, z) ∈ a ∧ (y, t) ∈ b } Function Constructs: First Series a → b { t | t ∈ a ↔ b ∧ ∀(x, y, z) ((x, y) ∈ t ∧ (x, z) ∈ t ⇒ y = z) } Fig. 2.
Axioms and Constructs of the B Set Theory each rule involving metavariables. It should also be noted that the computation of these superdeduction rules goes further than the one proposed in Sec. 4, since given a proposition rewrite rule R : P → Q, we apply to Q not only all the rules considered by Definition 2, but also the new generated superdeduction rules (except the rules for the extensional equality, in order to benefit from the dedicated rules of Zenon for equality) whenever applicable.

Regarding the superdeduction rules for the constructs, we can notice that given a definition E F , the generation of superdeduction rules is performed from the proposition rewrite rule R : x ∈ E → x ∈ F , and we can therefore wonder if completeness can still be ensured. In particular, we have to show that P (E) ⇔ P (F ), where P is a predicate symbol. This is actually possible using Rules for Axioms

(x, y) ∈ a × b × x ∈ a, y ∈ b a ∈ P(b) P X ∈ a | X ∈ b x ∈ { y | P (y) } {|} P (x) (x, y) ∈ a × b ¬× x ∈ a | y ∈ b a ∈ P(b) ¬P ǫx ∈ a, ǫx ∈ b with ǫx = ǫ(x).¬(x ∈ a ⇒ x ∈ b) x ∈ { y | P (y) } ¬{|} ¬P (x) a = b = X ∈ a, X ∈ b | X ∈ a, X ∈ b a = b = ǫx ∈ a, ǫx ∈ b | ǫx ∈ a, ǫx ∈ b with ǫx = ǫ(x).¬(x ∈ a ⇔ x ∈ b) Rules for Derived Constructs x ∈ a ∪ b ∪ x ∈ a | x ∈ b x ∈ a ∩ b ∩ x ∈ a, x ∈ b x ∈ a -b - x ∈ a, x ∈ b x ∈ a ∪ b ¬∪ x ∈ a, x ∈ b x ∈ a ∩ b ¬∩ x ∈ a | x ∈ b x ∈ a -b ¬- x ∈ a | x ∈ b x ∈ { e1, . . . , en } {} x = e1 | . . . | x = e1 x ∈ { e1, . . . , en } ¬{} x = e1, . . . , x = en x ∈ ∅ ∅ ⊙
Rules for Binary Relation Constructs: First Series

(x, y) ∈ a -1 ¬a -1 (y, x) ∈ a x ∈ dom(a) ¬dom (x, Y ) ∈ a y ∈ ran(a) ¬ran (X, y) ∈ a (x, z) ∈ a; b ; (x, ǫy) ∈ a, (ǫy, z) ∈ b with ǫy = ǫ(y).((x, y) ∈ a ∧ (y, z) ∈ b) (x, z) ∈ a; b ¬; (x, Y ) ∈ a | (Y, z) ∈ b (x, y) ∈ id(a) id x = y, x ∈ a, y ∈ a (x, y) ∈ id(a) ¬id x = y | x ∈ a | y ∈ a (x, y) ∈ a ⊳ b ⊳ (x, y) ∈ b, x ∈ a (x, y) ∈ a ⊳ b ¬⊳ (x, y) ∈ b | x ∈ a
(x, y) ∈ a -⊳ b -⊳ (x, y) ∈ b, x ∈ a (x, y) ∈ a ⊲ b ⊲ (x, y) ∈ a, y ∈ b (x, y) ∈ a -⊲ b -⊲ (x, y) ∈ a, y ∈ b (x, y) ∈ a -⊳ b ¬-⊳ (x, y) ∈ b | x ∈ a (x, y) ∈ a ⊲ b ¬⊲ (x, y) ∈ a | y ∈ b (x, y) ∈ a -⊲ b ¬-⊲ (x, y) ∈ a | y ∈ b
Rules for Binary Relation Constructs: Second Series

y ∈ a[b] a[b] ǫx ∈ b, (ǫx, y) ∈ a with ǫx = ǫ(x).(x ∈ b ∧ (x, y) ∈ a) (x, y) ∈ a - ⊳ b - ⊳ (x, y) ∈ a, (x, Y ) ∈ b | (x, y) ∈ b y ∈ a[b] ¬a[b] X ∈ b | (X, y) ∈ a (x, y) ∈ a - ⊳ b ¬ - ⊳ (x, y) ∈ a, (x, y) ∈ b | (x, ǫy) ∈ b, (x, y) ∈ b with ǫy = ǫ(y).((x, y) ∈ b) (x, (y, z)) ∈ a ⊗ b ⊗ (x, y) ∈ a, (x, ∈ b ((x, y), z) ∈ prj 1 (a, b) prj 1 x ∈ a, y ∈ z ∈ a, z = x (x, (y, z)) ∈ a ⊗ b ¬⊗ (x, y) ∈ a | (x, z) ∈ b ((x, y), z) ∈ prj 1 (a, b) ¬prj 1 x ∈ a | y ∈ b | z ∈ a | z = x ((x, y), z) ∈ prj 2 (a, b) prj 2 x ∈ a, y ∈ b, z ∈ b, z = y (x, y), (z, t)) ∈ a || b || (x, z) ∈ a, (y, t) ∈ b ((x, y), z) ∈ prj 2 (a, b) ¬prj 2 x ∈ a | y ∈ b | z ∈ b | z = y (x, y), (z, t)) ∈ a || b ¬|| (x, z) ∈ a | (y, t) ∈ b
Rules for Functions

a ∈ b → c → T / ∈ a, (X, Y ) ∈ a | T / ∈ a, (X, Z) ∈ a | T / ∈ a, Y = Z | ∆, (X, Y ) / ∈ a | ∆, (X, Z) / ∈ a | ∆, Y = Z with ∆ ≡ T = (ǫx, ǫy), ǫx ∈ b, ǫy ∈ c
where ǫx = ǫ(x).∃y the extensional equality (rules = and =) together with the substitution rules (rules pred and fun) as follows:

(T = (x, y) ∧ (x, y) ∈ b × c) ǫy = ǫ(y).(T = (ǫx, y) ∧ (ǫx, y) ∈ b × c) a ∈ b → c ¬ → ǫ ′ x ∈ a, ǫ ′ x = (Y, Z) | ǫ ′ x ∈ a, Y / ∈ b | ǫ ′ x ∈ a, Z / ∈ c | (ǫx, ǫy) ∈ a, (ǫx, ǫz) ∈ a, ǫy = ǫz with ǫ ′ x = ǫ(x).¬(x ∈ a ⇒ x ∈ b × c) ǫx = ǫ(x).¬(∀y∀z ((x, y) ∈ a ∧ (x, z) ∈ a ⇒ y = z)) ǫy = ǫ(y).¬(∀z ((ǫx, y) ∈ a ∧ (ǫx, z) ∈ a ⇒ y = z)) ǫz = ǫ(z).¬((ǫx, ǫy) ∈ a ∧ (ǫx, z) ∈ a ⇒ ǫy = z)
¬(P (E) ⇔ P (F )) β ¬⇔ ¬P (E), P (F ) pred E = F = ǫ x ∈ E, ǫ x ∈ F . . . ⊙ ǫ x ∈ E, ǫ x ∈ F . . . ⊙ P (E), ¬P (F ) . . .

⊙

where ǫ x = ǫ(x).¬(x ∈ E ⇔ x ∈ F ), and where the superdeduction rules for R : x ∈ E → x ∈ F can be respectively applied on ǫ x ∈ E and ǫ x ∈ E.

Dealing with Relations

As mentioned previously, the superdeduction rules for relations are generated from proposition rewrite rules of the form R : (x, y) ∈ E → (x, y) ∈ F , where E and F are relations, and the roots of these rules are therefore either (x, y) ∈ E, or (x, y) ∈ E. As a consequence, these rules cannot be applied to formulas in which pairs are not explicit, such as x ∈ E or x ∈ E for example. To deal with this problem, the idea is to add another proposition rewrite rule for the product, i.e. the rule R : x ∈ a × b → ∃y∃z (x = (y, z) ∧ (y, z) ∈ a × b), which generates the two following superdeduction rules:

x ∈ a × b × * x = (ǫ y , ǫ z ), ǫ y ∈ a, ǫ z ∈ b x ∈ a × b ¬× * x = (Y, Z) | Y ∈ a | Z ∈ b
where the first rule introduces ǫ y = ǫ(y).(∃z (x = (y, z) ∧ (y, z) ∈ a × b)), and

ǫ z = ǫ(z).(x = (ǫ y , z) ∧ (ǫ y , z) ∈ a × b)).
For each relation p, we also need to add another proposition rewrite rule of the form R : x ∈ p → ∃y∃z (x = (y, z) ∧ (y, z) ∈ p), and then generate the corresponding superdeduction rules. For example, for the inverse relation, we obtain the rules as follows:

x ∈ a -1 a -1 * x = (ǫ y , ǫ z ), (ǫ z , ǫ y ) ∈ a x ∈ a -1 ¬a -1 * x = (Y, Z) | (Z, Y ) ∈ a
where the first rule introduces ǫ y = ǫ(y).(∃z (x = (y, z) ∧ (y, z) ∈ a -1 )), and

ǫ z = ǫ(z).(x = (ǫ y , z) ∧ (ǫ y , z) ∈ a -1 ).
With these new rules, we can prove p ⊆ a × b ⇒ x ∈ p ⇒ x ∈ (p -1 ) -1 in the following way (we start the proof after the series of α ¬⇒ has been applied, and we do not detail the definitions of the involved ǫ-terms):

p ⊆ a × b, x ∈ p, x ∈ (p -1 ) -1 ⊆ X ∈ p . . . ⊙ X ∈ a × b × * X = (ǫ y , ǫ z ), ǫ y ∈ a, ǫ z ∈ b ¬a -1 * x = (Y, Z) . . . ⊙ (Z, Y ) ∈ p -1 ¬a -1 (Y, Z) ∈ p pred x = (Y, Z) . . . ⊙ p = p ⊙ r ⊙
where X, Y , and Z are respectively instantiated by x, ǫ y , and ǫ z .

Implementation and Benchmarks

The implementation of our extension of Zenon for the B set theory described in Sec. 5 has been possible thanks to the ability of Zenon to extend its core of deductive rules to match specific requirements like superdeduction. Concretely, this extension is an OCaml file in which the superdeduction rules of Figs. 3 and4 are implemented (about 2,000 lines of code). This file is loaded through command-line options when Zenon is started, along with a Coq file containing the translation of the superdeduction rules and used to generate Coq proofs.

As said in the introduction, one of the main motivations for this extension of Zenon for the B set theory is to verify B proof rules of Atelier B [START_REF][END_REF], and in particular rules coming from the database maintained by Siemens IC-MOL. Concretely, a rule is mainly a set formula with guards, which are used to control the application of the rule (verifying that a given hypothesis is in the context, for example). The verification of a rule has been formally described in [START_REF] Jacquel | Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving[END_REF], and consists in verifying that the rule is well-typed, well-defined, and that it can be derived using the rules of the B proof system (see [START_REF] Karim | The B-Book: Assigning Programs to Meanings[END_REF]). Over the last few years, Siemens IC-MOL has developed a formal and mechanized environment, named BCARe, which is dedicated to the rule verification, and which relies in particular on a deep embedding of the B set theory in Coq, called BCoq. In this environment, our extension of Zenon is supposed to deal with the last step of verification of a rule, i.e. the derivation of the rule within the B proof system.

Regarding benchmarks, we consider a selection of B proof rules coming from the database maintained by Siemens IC-MOL. This selection actually consists of well-typed and well-defined rules, which involve all the B set constructs currently handled by the implementation of our extension of Zenon, i.e. all the constructs of Chap. 2 of the B-Book [START_REF] Karim | The B-Book: Assigning Programs to Meanings[END_REF] until the override construct (noted -⊳ ). This represents a subset of 1,397 rules, and we propose two benchmarks whose results are gathered in Figs. 5 and6.

The first benchmark aims to compare our extension of Zenon with the approach coming from another experiment described in [START_REF] Jacquel | Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving[END_REF]. In this approach, Zenon is simply used as a first order theorem prover (no set theory is added), and the set formulas must be preliminarily normalized in order to obtain first order logic formulas containing only the ∈ set operator (which is considered as an uninterpreted predicate symbol). This pre-normalization is performed in Coq (within the BCoq embedding), before calling Zenon. Over the 1,397 selected rules, our extension of Zenon is able to prove 1,340 rules (96%), while our initial approach can deal with 1,145 rules (82%), which represents an increase of 195 rules (14%). The difference of proved rules mostly comes from ineffective parts of the implementation of our initial approach, which still have to be optimized, and is not due to the incompleteness of this approach (which is not pointed out over the considered subset of rules). The graph of Fig. 5 presents a comparison of both approaches in terms of proof time (run on an Intel Core i5-2500K 3.30GHz/12GB computer) for a subset of the 1,397 selected rules, where both approaches succeed in finding a proof (the time measurement includes the compilation of Coq proofs generated by Zenon), i.e. for 1,145 rules. In this figure, a point represents the result for a rule, and the x/y-axes respectively correspond to the Zenon approach with pre-normalization of the formulas and to our extension of Zenon using superdeduction. For each point under the triangled curve, our extension based on superdeduction is at least 10 times faster than our initial approach with pre-normalization of the formulas; under the crossed curve, it is 100 times faster, and under the squared curve, it is 1,000 times faster. We can observe that there is a lot of rules for which the proof is 10 or 100 times faster with superdeduction, and on average, the superdeduction proofs are obtained 67 times faster (the best ratio is 1,540). These results are quite satisfactory in the sense that our extension based on superdeduction solves the inefficiency issues of our initial approach (mainly due to the pre-normalization, which is highly time-consuming).

We propose a second benchmark whose purpose is to emphasize the proof size speed-up offered by superdeduction. In this benchmark, the idea is to compare our extension of Zenon using superdeduction with another extension of Zenon for the B set theory, where the proposition rewrite rules are not computed into superdeduction rules, but just unfolded/folded (like in Prawitz's initial approach [START_REF] Prawitz | Natural Deduction. A Proof-Theoretical Study[END_REF]). The comparison consists in computing the number of proof nodes of each proof generated by Zenon. We consider a subset of 1,340 rules, i.e. the rules for which both extensions succeed in finding a proof. The results are summarized by the graph of Fig. 6, where a point represents the result for a rule, and where the x/y-axes respectively correspond to the extension without and with superdeduction. As can be seen, the major part of proofs in superdeduction are shorter than the proofs where the rules have not been computed and on average, the former have 1.6 times less proof nodes than the latter (the best ratio is 6.25).

The previous benchmarks tend to show that the use of our extension of Zenon for the B set theory and based on superdeduction is quite effective in practice, and very promising in terms of scalability. In particular, this could be also applied to the verification of B proof obligations (which involve much larger formulas than B proof rules).

A Generic Implementation for First Order Theories

In this section, we present another extension of Zenon with superdeduction, which is able to deal with any first order theory. In this extension, the theory is analyzed to determine the axioms that can be turned into superdeduction rules, and these superdeduction rules are automatically computed on the fly to enrich the deductive kernel of Zenon. We also provide a comparative benchmark coming from the TPTP library, which contains a large set of first order problems, and which is usually used to test the implementations of automated theorem provers.

From Theories to Superdeduction Systems

This extension of Zenon is actually a generalization of the previous one dedicated to the B set theory, where superdeduction rules are automatically computed on the fly. In the previous extension, superdeduction rules are hard-coded since the B set theory is a higher order theory due to one of the axioms of the theory (the comprehension scheme), and we have to deal with this axiom specifically in the implementation of Zenon. Even though some techniques exist to handle higher order theories as first order theories (like the theory of classes, for example), a hard-coding of these theories may be preferred as these techniques unfortunately tend to increase the entropy of the proof search. In addition, in the previous extension, some of the superdeduction rules must be manually generated as they must be shrewdly tuned (ordering the several branches of the rules, for instance) to make the tool efficient. The new extension of Zenon dealing with any first order theory has been developed as a tool called Super Zenon [START_REF] Jacquel | Super Zenon, version 0.0.1. Siemens and Cnam[END_REF], where each theory is analyzed to determine the axioms that are candidates to be turned into superdeduction rules. As said in Sec. 4, axioms of the form ∀x (P ⇔ ϕ), where P is atomic, can be transformed, but we can actually deal with more axioms, in particular with axioms of the form ∀x (P ⇒ ϕ), which is actually equivalent to perform polarized deduction modulo as introduced in [START_REF] Dowek | What is a Theory?[END_REF]. Here is the exhaustive list of axioms that can be handled by Super Zenon, as well as the corresponding superdeduction rules that can be generated (in the following, P and P ′ are atomic, and ϕ is an arbitrary formula):

-Axiom of the form ∀x (P ⇔ ϕ): we consider the proposition rewrite rule R : P → ϕ, and the two superdeduction rules R and ¬R are generated; -Axiom of the form ∀x (P ⇒ P ′ ): we consider the proposition rewrite rules R : P → P ′ and R ′ : ¬P ′ → ¬P , and only the superdeduction rules R and R ′ are generated; -Axiom of the form ∀x (P ⇒ ϕ): we consider the proposition rewrite rule R : P → ϕ, and only the superdeduction rule R is generated; -Axiom of the form ∀x (ϕ ⇒ P ): we consider the proposition rewrite rule R : ¬P → ¬ϕ, and only the superdeduction rule R is generated; -Axiom of the form ∀x P : we consider the degenerated proposition rewrite rule R : ¬P → ⊥, and only the superdeduction rule R is generated.

The axioms of the theory that are not of these forms are left as regular axioms. An axiom that is of one of these forms is also left as a regular axiom if the conclusion of one of the generated superdeduction rules (i.e. the top formula of one of these rules) unifies with the conclusion of an already computed superdeduction rule (in this case, the theory is actually non-deterministic, and we try to minimize this source of non-determinism by dividing these incriminated axioms among the sets of superdeduction rules and regular axioms). An axiom that is of one of these forms is still left as a regular axiom if P is an equality (as we do not want to interfere with the specific management of equality by the kernel of Zenon). Finally, for axioms of the form ∀x (P ⇒ P ′ ), we also consider the proposition rewrite rule that corresponds to the converse of the initial formula; this actually allows us to keep cut-free completeness in this particular case.

Benchmark from the TPTP Library

To assess the effectiveness of Super Zenon compared to the regular version of Zenon, we propose a benchmark that consists of problems coming from the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF]. This library is a large collection of problems, which is used to test the implementations of automated theorem provers in particular. From this library, we consider a selection of problems that consists of the set of non-clausal first order problems, i.e. the problems of the FOF category in the TPTP library. The results of this experiment (run on an Intel Pentium D Xeon 3.60GHz/32GB computer) are summarized in Tab. 1, where both Zenon and Super Zenon are called over the problems of the FOF category. As can be observed, Super Zenon is able to prove more problems than Zenon in the whole FOF category with a significant rate (about 7%). This rate becomes even much better in some specific sub-categories of the FOF category, like in the SET sub-category (about 37%), which gathers problems of set theory. These results in the SET sub-category tend to confirm the other results described in Sec. 6 in the framework of the B method, and also tend to show that set theory is an appropriate theory to be handled by superdeduction and by deduction modulo more generally. In addition to the problems of the FOF category, Super Zenon has been also applied to the counter-satisfiable problems of the TPTP library, i.e. problems that are not valid, and Super Zenon does not find any proof for these problems, which allows us to have a relative confidence in the correctness of the implementation of this tool. Superdeduction can be seen as a generic method to integrate axiomatic first order theories into deductive formal proof systems, like sequent calculus, as well as into proof search methods that are very closed to deductive formal proof systems, like the tableau method, which is a proof search method in sequent calculus without cut. In particular, as seen previously, it has allowed us to smoothly integrate the set theory of the B method into the tableau method, which has been implemented as an extension of the Zenon automated theorem prover, and which has been used for the verification of B proof rules. The considered approach is actually so generic that it has been generalized into a new extension of Zenon, called Super Zenon, which is able to deal with any axiomatic first order theory. Thus, any user that aims to perform automated deduction in a given axiomatic first order theory must just provide the theory to Super Zenon, which is able to automatically integrate a part of this theory as superdeduction rules. The approach is even more generic since it can be actually implemented in any tool based on a tableau method. As for the application of superdeduction to other proof search methods, such as resolution for example, the approach is probably less straightforward since resolution proofs are actually far from proofs in usual deductive formal proof systems, like sequent calculus, which makes the introduction of superdeduction rules harder as these rules are pure deduction rules. However, some work has been done in this direction in the framework of deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] (whose superdeduction may be considered as a variant), with a concrete development, called iProver Modulo [START_REF] Burel | Experimenting with Deduction Modulo[END_REF], implemented as an extension of iProver [START_REF] Korovin | iProver -An Instantiation-Based Theorem Prover for First-Order Logic (System Description)[END_REF], which is a resolution-based automated theorem prover.

Conclusion

We have proposed a method that allows us to develop tableaux modulo theories using superdeduction. This method has been presented in the framework of the Zenon automated theorem prover, and applied to the set theory of the B method. This has allowed us to provide another prover to Atelier B, which can be used to verify B proof rules automatically. We have also proposed some benchmarks using rules coming from the database maintained by Siemens IC-MOL. These benchmarks have emphasized significant speed-ups both in terms of proof time and proof size compared to previous and alternative approaches. Finally, we have described another extension of Zenon with superdeduction, called Super Zenon, which is able to deal with any first order theory. In this extension, the theory is analyzed to determine the axioms that can be turned into superdeduction rules, and these superdeduction rules are automatically computed on the fly to enrich the deductive kernel of Zenon. A comparative benchmark that consists of a large set of first order problems coming from the TPTP library has shown a significant improvement of Super Zenon over the regular version of Zenon.

As future work, we must extend our specific implementation realized for verifying B proof rules in order to deal with a larger set of rules coming from the database maintained by Siemens IC-MOL. More precisely, the next step is to consider functions, and the corresponding rules should point out the incompleteness of our initial approach that consists in pre-normalizing the set formulas. For instance, formulas such as { (x, y) | x = y } ∈ a → a ⇒ ∃f (f ∈ a → a ∧ (b, b) ∈ f ) should be proved by our extension based on superdeduction, but not by our initial approach (since an additional normalization is required once f has been instantiated by the comprehension set in hypothesis). We also plan to enhance the heuristic used by Super Zenon to transform axioms into superdeduction rules in order to increase the improvement of Super Zenon over Zenon in the framework of generic theories. In addition, it should be worth building an heuristic with transformation rules that preserves some important properties (from the automated deduction point of view) of the initial axiomatic theories, such as cut-free completeness for example.

Fig. 1 .

 1 Fig. 1. Proof Search Rules of Zenon

(

  x, y) ∈ a -1 a -1 (y, x) ∈ a x ∈ dom(a) dom (x, ǫy) ∈ a with ǫy = ǫ(y).((x, y) ∈ a) y ∈ ran(a) ran (ǫx, y) ∈ a with ǫx = ǫ(x).((x, y) ∈ a)

Fig. 3 .

 3 Fig. 3. Superdeduction Rules for the B Set Theory (Part 1)

Fig. 4 .

 4 Fig. 4. Superdeduction Rules for the B Set Theory (Part 2)

Fig. 5 .

 5 Fig. 5. Proof Time Comparative Benchmark

Fig. 6 .

 6 Fig. 6. Proof Size Comparative Benchmark

Table 1 .

 1 Experimental Results over the TPTP Library 8 Superdeduction for Automated Deduction

	TPTP Category	Zenon	Super Zenon
	FOF 6,644 problems	1,646	1,765 (7.2%)
	SET 462 problems	147	202 (37.4%)

Acknowledgement. Many thanks to G. Burel and O. Hermant for their detailed comments on this paper, to G. Dowek for seminal discussions about this work, and to D. Doligez for his help in the integration of superdeduction into Zenon.


David Delahaye

Mélanie Jacquel

Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction

HAL is

Introduction

These days, theorem proving appears as an appropriate support for education in subjects such as mathematics and more generally logic, where proofs play a significant role. This can be explained by the fact that some of the existing theorem prover based systems have a long history of development, and constantly provide technical innovations not only in terms of design, but also in terms of theory. Among these theorem prover based systems, interactive theorem provers, such as Coq [20] for example, appear to be quite appropriate tools, since they offer special environments dedicated to proving. In particular, these special environments offer syntax and type checking, as well as a bounded set of tactics, i.e. commands building proofs when applied to proof goals. These environments also provide some assistance in the way of building proofs, since tactics are able to automatically and incrementally produce proofs when applied to goals. This assistance does not only concern the application of tactics, but may also be related to other aspects regarding modeling, such as the automated generation of induction schemes from inductive types for instance. However, these mechanized frameworks do not offer any guidance in the way of finding the right proof of a theorem, and if the user does not have the intuition of this proof (which may be acquired by thinking of the proof on paper), it is likely that he/she would experience some difficulties in building the corresponding proof, even with an interactive proof loop (even worse, he/she would probably get lost by unnecessarily applying some tactics in an endless way, like induction tactics for example). To deal with this problem of finding proofs, we may consider the use of automated theorem provers as long as they at least provide proof traces which are comprehensible enough to recover the intuition of the corresponding proofs.

Automated theorem proving is a quite wide and still very active domain of research. In automated theorem proving, we generally distinguish the semantic methods from the syntactic methods. The semantic methods, such as the Davis-Putnam algorithm [START_REF] Davis | A Computing Procedure for Quantification Theory[END_REF] or the Binary Decision Diagrams [5] (BDDs) for instance, have the advantage to be quite intuitive, but are limited to propositional calculus. To deal with first order logic, we preferably rely on syntactic methods, which may be split into two large families of methods. The first family of methods is the saturation-based theorem proving, which was actually introduced by Robinson with the resolution calculus [START_REF] Alan | A Machine-Oriented Logic Based on the Resolution Principle[END_REF]. Resolution is a complete method working by refutation: a contradiction (i.e. the empty clause) has to be deduced from an unsatisfiable set of clauses. The search for a contradiction proceeds by saturating the given set of clauses, that is, systematically (and exhaustively) applying all applicable inference rules. The principle of resolution is general enough to allow many calculi to be seen as resolution-based calculi (binary resolution, positive resolution, semantic resolution, hyper-resolution, the inverse method, etc). However, a proof produced by resolution is not appropriate to get the intuition of the proof, since resolution actually works on a formula in clausal form (a preliminary step therefore consists in clausifying the initial formula), and there is little chance to understand the proof of the initial formula from the resolution proof (unless the initial formula is already in clausal form). The second family of syntactic methods tend to palliate this difficulty and are called tableau-based methods. Tableaux are actually much older than resolution-based methods and were introduced by pioneers Hintikka [START_REF] Jaakko | Form and Content in Quantification Theory[END_REF] and Beth [2] from the cut-free version of Gentzen's sequent calculus [11]. The tableau method still works by refutation but over the initial formula contrary to resolution, and by case distinction. More precisely, it allows us to systematically generate subcases until elementary contradictions are reached, building a kind of tree from which it is possible to almost directly produce a proof. Compared to resolution, tableaux therefore offer the possibility to build comprehensible proofs which are directly related to the corresponding initial formulas.

If tableaux allow us to produce more comprehensible proofs, some recent deduction techniques have been developed and tend to improve the presentation of proofs in the usual deductive systems, in particular when reasoning modulo a theory. Among these new deduction techniques, there are, for example, deduction modulo [10] and superdeduction [4], which respectively focus on the computational and deductive parts of a theory, and which can be considered as steps toward high-level deductive languages. If deduction modulo and superdeduction are equivalent when reasoning modulo a theory, superdeduction appears to be more appropriate to produce proofs close to the human intuition as it allows us to naturally encode custom deduction schemes. In addition, the principle of superdeduction relies on the generation of specific deduction rules (called superdeduction rules) from the axioms of the theory, and in practice, it is quite easier to extend existing tools with ad hoc deduction rules than with a congruence over the formulas (coming from the computational rules of deduction modulo).

In this paper, we propose an automated deduction method based both on tableaux and superdeduction. As said previously, the main motivation is to build a system able to provide a significant help in matter of education by automatically producing proofs comprehensible enough to recover the intuition of these proofs. To show that such a system is actually effective in practice, we also propose to implement this system by realizing an extension of an existing automated theorem prover called Zenon [3], and which relies on classical first order logic with equality and applies the tableau method as proof search. In this context, the choice of Zenon is strongly influenced by its ability of producing comprehensible proof traces (with several levels of details). In addition, Zenon offers an extension mechanism, which allows us to extend its core of deductive rules to match specific requirements, and which is therefore quite appropriate to integrate superdeduction. Two extensions of Zenon with superdeduction have been implemented and will be considered in this paper. The first implementation is dedicated to the set theory of the B method [1] (or B for short), which is a formal method and allows engineers to develop software with high guarantees of confidence. This implementation is used by Siemens IC-MOL to automatically verify B proof rules coming from a database which is built adding rules from their several projects and applications, such as driverless metro systems for instance (see [13,14] for more details). The second implementation is generic and works over any first order theory, which allows us to use it to prove problems from the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF] (which is a library of test problems for automated theorem proving systems).

The paper is organized as follows: in Section 2, we first introduce the principles of superdeduction; we then present, in Section 3, the computation of superdeduction rules from axioms in the framework of the tableau method used by Zenon; finally, in Sections 4 and 5, we respectively describe the implementation of our extensions of Zenon for the B set theory and for any first order theory, and also provide some examples respectively coming from the database of B proof rules maintained by Siemens IC-MOL and the TPTP library.

Principles of Superdeduction

In this section, we present the principles of superdeduction, which is a variant of deduction modulo, and which allows us to describe proofs in a more compact format in particular. In addition, we show that proofs in superdeduction are not only shorter, but also follow a more natural human reasoning scheme, and that custom deduction schemes, such as structural induction over Peano natural numbers for example, can be naturally encoded using superdeduction.

Deduction Modulo and Superdeduction

Deduction modulo [10] 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. Superdeduction [4] is a variant of deduction modulo, where axioms are used to enrich the deduction system with new deduction rules, which are called superdeduction rules. For instance, considering the inclusion in set theory ∀a, b (a ⊆ b ⇔ ∀x (x ∈ a ⇒ x ∈ b)), 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 ∀a, b (a ⊆ b ⇔ ∀x (x ∈ a ⇒ x ∈ b)) ⊢ A ⊆ A
In deduction modulo, the axiom of inclusion can be seen as a computation rule and therefore replaced by the rewrite rule a ⊆ b → ∀x (x ∈ a ⇒ x ∈ b). 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
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 us for unbounded proof size speed-up [6].

Superdeduction proposes to go further than deduction modulo precisely when the considered axiom defines a predicate P with an equivalence ∀x (P ⇔ ϕ). While deduction modulo replaces the axiom by a rewrite rule, superdeduction adds to this transformation the decomposition of the connectives occurring in this definition. This corresponds to an extension of Prawitz's folding and unfolding rules [17] (called introduction and elimination rules by Prawitz), where the connectives of the definition are introduced and eliminated. The proposed (right) superdeduction rule is then the following (there is also a corresponding left rule):

Γ, x ∈ a ⊢ x ∈ b, ∆ IncR, x ∈ Γ, ∆ Γ ⊢ a ⊆ b, ∆
Hence, proving A ⊆ A with this new rule can be performed as follows:

Ax x ∈ A ⊢ x ∈ A IncR ⊢ A ⊆ A
This new proof is not only simpler and shorter than in deduction modulo, but also follows a natural human reasoning scheme usually used in mathematics as shown more precisely in the next subsection.

Human Reasoning with Superdeduction

Considering the previous example of inclusion in set theory, we can notice that the superdeduction rule is more natural and intuitive than a simple folding rule à la Prawitz. Given two sets A and B, if we aim to prove A ⊆ B, it seems a little unusual to propose to prove ∀x (x ∈ A ⇒ x ∈ B), instead we propose to prove x ∈ B given x s.t. x ∈ A, which amounts to implicitly introducing the connectives of the unfolded proposition. This implicit introduction of connectives is precisely proposed by the previous superdeduction rule, which can be read as "if any element of a is an element of b, then a ⊆ b".

Similarly, superdeduction can also be used to naturally encode custom deduction schemes. For example, let us consider the structural induction scheme over Peano natural numbers (i.e. non-negative integers). This scheme can be defined as follows (i.e. the natural numbers are seen as the set of terms verifying the inductive predicate):

∀n (n ∈ AE ⇔ ∀P (0 ∈ P ⇒ ∀m (m ∈ P ⇒ S(m) ∈ P ) ⇒ n ∈ P ))
In sequent calculus, this scheme can be encoded by the two following (right) superdeduction rules (there are also two corresponding left rules):

Γ, 0 ∈ P, H(P ) ⊢ n ∈ P, ∆ IndR, P ∈ Γ, ∆ Γ ⊢ n ∈ AE, ∆ Γ, m ∈ P ⊢ S(m) ∈ P, ∆ HeredR, m ∈ Γ, ∆ Γ ⊢ H(P ), ∆
Let us notice that the induction scheme actually requires two superdeduction rules, whose one of the rules (the rule HeredR) focuses on the heredity part of the scheme in particular. This focus is motivated by the need of avoiding permutability problems (between Skolemization and instantiation), which may occur when computing superdeduction rules. These permutability problems are quite common in automated proof search, and appear here since superdeduction systems are in fact embedding a part of compiled automated deduction. In [4] and in order to deal with these permutability problems, the authors use a method inspired by focusing techniques in the framework of sequent calculus. It is worth noting that these permutability problems are managed in different ways by automated deduction methods, and in particular, we will therefore not have to use focusing techniques when integrating superdeduction to the tableau method in Section 3.

Tableaux with Superdeduction

In this section, we present the tableau method used by the Zenon automated theorem prover, which deals with classical first order logic with equality and a specific support for equivalence relations. Once the rules of this method have been described, we show how it is possible to compute superdeduction rules from axiomatic theories, and how these new rules extend the kernel of rules of Zenon.

The Tableau Method

The proof search rules of Zenon are described in detail in [3] and summarized in Figure 1 (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), 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 the equality in particular). 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; they are not used as variables as they are never substituted. The proof search rules are applied with the normal 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 an application of 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 work on another branch. Moreover, we work in a non-destructive way: working on one branch will never change the formulas of another branch.

From Axioms to Superdeduction Rules

As mentioned in Section 2, reasoning modulo a theory in a tableau method using superdeduction requires to generate new deduction rules from some axioms of the theory. The axioms which can be Closure and Cut Rules

⊥ ⊙ ⊥ ⊙ ¬⊤ ⊙ ¬⊤ ⊙ cut P | ¬P ¬R r (t, t) ⊙ r ⊙ P ¬P ⊙ ⊙ R s (a, b) ¬R s (b, a) ⊙ s ⊙ Analytic Rules ¬¬P α ¬¬ P P ⇔ Q β ⇔ ¬P, ¬Q | P, Q ¬(P ⇔ Q) β¬ ⇔ ¬P, Q | P, ¬Q P ∧ Q α ∧ P, Q ¬(P ∨ Q) α ¬∨ ¬P, ¬Q ¬(P ⇒ Q) α ¬⇒ P, ¬Q P ∨ Q β ∨ P | Q ¬(P ∧ Q) β ¬∧ ¬P | ¬Q P ⇒ Q β ⇒ ¬P | Q ∃x P (x) δ ∃ P (ǫ(x).P (x)) ¬∀x P (x) δ ¬∀ ¬P (ǫ(x).¬P (x)) γ-Rules ∀x P (x) γ ∀M P (X) ¬∃x P (x) γ ¬∃M ¬P (X) ∀x P (x) γ ∀inst P (t) ¬∃x P (x) γ ¬∃inst ¬P (t)
Relational Rules

P (t 1 , . . . , t n ) ¬P (s 1 , . . . , s n ) pred t 1 = s 1 | . . . | t n = s n f (t 1 , . . . , t n ) = f (s 1 , . . . , s n ) fun t 1 = s 1 | . . . | t n = s n R s (s, t) ¬R s (u, v) sym t = u | s = v ¬R r (s, t) ¬ refl s = t R t (s, t) ¬R t (u, v) trans u = s, ¬R t (u, s) | t = v, ¬R t (t, v) R ts (s, t) ¬R ts (u, v) transsym v = s, ¬R ts (v, s) | t = u, ¬R ts (t, u) s = t ¬R t (u, v) transeq u = s, ¬R t (u, s) | ¬R t (u, s), ¬R t (t, v) | t = v, ¬R t (t, v) s = t ¬R ts (u, v) transeqsym v = s, ¬R ts (v, s) | ¬R ts (v, s), ¬R ts (t, u) | t = u, ¬R ts (t, u)
Figure 1: Proof Search Rules of Zenon considered for superdeduction are of the form ∀x (P ⇔ ϕ), where P is atomic. This specific form of axiom allows us to introduce an orientation of the axiom from P to ϕ, and we introduce the notion of proposition rewrite rule (this notion appears in [4], from which we borrow the following definition and notation): Definition 1 (Proposition Rewrite Rule) The notation R : P → ϕ denotes the axiom ∀x (P ⇔ ϕ), where R is the name of the rule, P an atomic proposition, ϕ a proposition, and x the free variables of P and ϕ.

It should be noted that P may contain first order terms and therefore that such an axiom is not just a definition. For instance,

x ∈ { y | y ∈ a ∧ y ∈ b } → x ∈ a ∧ x ∈ b (
where the comprehension set is a first order term) is a proposition rewrite rule.

Let us now describe how the computation of superdeduction rules for Zenon is performed from a given proposition rewrite rule.

Definition 2 (Computation of Superdeduction Rules) Let S be a set of rules composed by the subset of the proof search rules of Zenon formed of the closure rules, the analytic rules, as well as the γ ∀M and γ ¬∃M rules. Given a proposition rewrite rule R : P → ϕ, two superdeduction rules (a positive one R and a negative one ¬R) are generated in the following way: 1. To get the positive rule R, initialize the procedure with the formula ϕ. Next, apply the rules of S until there is no open leaf anymore on which they can be applied. Then, collect the premises and the conclusion, and replace ϕ by P to obtain the positive rule R.

2. To get the negative rule ¬R, initialize the procedure with the formula ¬ϕ. Next, apply the rules of S until there is no open leaf anymore on which they can be applied. Then, collect the premises and the conclusion, and replace ¬ϕ by ¬P to obtain the negative rule ¬R.

If the rule R (resp. ¬R) involves metavariables, an instantiation rule R inst (resp. ¬R inst ) is added, where one or several metavariables can be instantiated.

Integrating these new deduction rules to the proof search rules of Zenon is sound as they are generated from a subset of rules of Zenon, while cut-free completeness cannot be preserved in general (i.e. for any theory). In practice, soundness can be ensured by the ability of Zenon of producing proofs for some proof assistants, such as Coq and Isabelle, which can be used as proof checkers.

Let us illustrate the computation of superdeduction rules from a proposition rewrite rule with the example of the set inclusion.

Example 3 (Set Inclusion)

From the definition of the set inclusion, we introduce the proposition rewrite rule Inc : a ⊆ b → ∀x (x ∈ a ⇒ x ∈ b), and the corresponding superdeduction rules Inc and ¬Inc are generated as follows:

∀x (x ∈ a ⇒ x ∈ b) γ ∀M X ∈ a ⇒ X ∈ b β ⇒ X ∈ a | X ∈ b ¬∀x (x ∈ a ⇒ x ∈ b) δ ¬∀ ¬(ǫ x ∈ a ⇒ ǫ x ∈ b) α ¬⇒ ǫ x ∈ a, ǫ x ∈ b where ǫ x = ǫ(x).¬(x ∈ a ⇒ x ∈ b).
The resulting superdeduction rules are then the following:

a ⊆ b Inc X ∈ a | X ∈ b a ⊆ b Inc inst t ∈ a | t ∈ b a ⊆ b ¬Inc ǫ x ∈ a, ǫ x ∈ b

An Implementation for the B Set Theory

In this section, we describe our first extension of Zenon with superdeduction in the case of the B set theory, which is the underlying theory of the B formal method, and where superdeduction rules are hard-coded from the initial axiomatic theory. We also propose an example of B proof rule coming from the database maintained by Siemens IC-MOL, and that can be verified by this tool producing a quite comprehensible proof.

Superdeduction Rules for the B Set Theory

This extension of Zenon for the B set theory is actually motivated by an experiment which is managed by Siemens IC-MOL regarding the verification of B proof rules [13,14]. The B method [1], or B for short, allows engineers to develop software with high guarantees of confidence; more precisely it allows them to build correct by design software. B is a formal method based on set theory and theorem proving, and which relies on a refinement-based development process. The Atelier B environment [7] is a platform that supports B and offers, among other tools, both automated and interactive provers. In practice, to ensure the global correctness of formalized applications, the user must discharge proof obligations. These proof obligations may be proved automatically, but otherwise, they have to be handled manually either by using the interactive prover, or by adding new proof rules that the automated prover can exploit. These new proof rules can be seen as axioms and must be verified by other means, otherwise the global correctness may be endangered.

In [13], we develop an approach based on the use of Zenon to verify B proof rules. The method used in this approach consists in first normalizing the formulas to be proved, in order to obtain first order formulas containing only the membership set operator, and then calling Zenon on these new formulas. This experiment gives satisfactory results in the sense that it can prove a significant part of the rules coming from the database maintained by Siemens IC-MOL (we can deal with about 1,400 rules, 1,100 of which can be proved automatically, over a total of 5,300 rules). However, this approach is not complete (after the normalization, Zenon proves the formulas without any axiom of set theory, while some instantiations may require to be normalized), and suffers from efficiency issues (due to the preliminary normalization). To deal with these problems, the idea developed in [14] is to integrate the axioms and constructs of the B set theory into the Zenon proof search method by means of superdeduction rules. This integration is concretely achieved thanks to the extension mechanism offered by Zenon, which allows us to extend its core of deductive rules to match specific requirements. This new tool has emphasized significant speed-ups both in terms of proof time and proof size compared to the previous approach (see [14] for more details).

The B method is based on a typed set theory. There are two rule systems: one for demonstrating that a formula is well-typed, and one for demonstrating that a formula is a logical consequence of a set of axioms. The main aim of the type system is to avoid inconsistent formulas, such as Russell's paradox for example. The B proof system is based on a sequent calculus with equality. Six axiom schemes define the basic operators and the extensionality which, in turn, defines the equality of two sets. In addition, the other operators (∪, ∩, etc.) are defined using the previous basic ones. To generate the superdeduction rules corresponding to the axioms and constructs, we use the algorithm described in Section 2, and we must therefore identify the several proposition rewrite rules. Regarding the axioms, they are all of the form P i ⇔ Q i , and the associated proposition rewrite rules are therefore R i : P i → Q i , where each axiom is oriented from left to right. For instance, let us consider the equality of two sets, which is defined by the following axiom:

a = b ⇔ ∀x (x ∈ a ⇔ x ∈ b)
From this axiom, we can compute two superdeduction rules as follows (a third rule dealing with instantiation is also implicitly computed since one of the generated rules involves metavariables):

a = b = X ∈ a, X ∈ b | X ∈ a, X ∈ b a = b = ǫ x ∈ a, ǫ x ∈ b | ǫ x ∈ a, ǫ x ∈ b with ǫx = ǫ(x).¬(x ∈ a ⇔ x ∈ b)
Concerning the constructs, they are expressed by definitions of the form E i F i , where E i and F i are expressions, and the corresponding proposition rewrite rules are

R i : x ∈ E i → x ∈ F i .
Let us illustrate the computation of superdeduction rules for constructs with the example of domain restriction, which is defined in the following way:

a ⊳ b id(a); b where: a; b { (x, z) | ∃y ((x, y) ∈ a ∧ (y, z) ∈ b } id(a) { (x, y) | (x, y) ∈ a × a ∧ x = y }
The corresponding superdeduction rules are computed as follows:

(x, y) ∈ a ⊳ b ⊳ (x, y) ∈ b, x ∈ a (x, y) ∈ a ⊳ b ¬⊳ (x, y) ∈ b | x ∈ a
For further details regarding the computation of superdeduction rules for the B set theory, as well as the corresponding implementation using Zenon, the reader can refer to [14].

Verification of a B Proof Rule

To assess our extension of Zenon for the B set theory using superdeduction and to show that it can produce proofs comprehensible enough to recover the intuition of these proofs, we propose to consider the example of a B proof rule coming from the database maintained by Siemens IC-MOL. The rule being considered is the rule named "SimplifyRelDorXY.27" (this rule is actually part of the Atelier B set of rules), and whose proof is small enough to be understood easily and described in the space restrictions for this paper. The definition of this rule is the following:

∅ ⊳ a = ∅
When applied to this rule, our extension of Zenon produces the proof of Figure 2 (Zenon proposes several proof formats, and the proof presented in this figure uses the format with the highest level of abstraction). The statement of the rule, i.e. the command starting with "fof", is provided using the TPTP syntax [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF], and the proof (if found) is displayed after this statement. The proof consists of several numbered steps, where each of them is a set of formulas together with a proof rule which has been applied to the considered proof step. Formulas of a proof step are signed formulas, and formulas starting with "-." are negative formulas. A proof rule appears at the end of a proof step and after the string "###", and also provides, after the string "->", the other proof steps to which it is connected (these other proof steps represent the result of the application of this proof rule to the set of formulas of the considered proof step). For example, in this proof, Step 1 is connected to Steps 2 and 3. This connection between proof steps provides the proof with a tree-like structure, where proof steps with axiomatic rules, i.e. starting with "Axiom", are leaves, while the other proof steps are nodes. Among these other proof steps, there are in particular superdeduction rules, which start with "Extension". In this proof, the B constructs are prefixed by "b_", and "b_empty", "b_BIG", "b_in", "b_eq", and "b_drest" respectively represent the empty set ∅, the set BIG (which is an infinite set, mostly only used to build natural numbers in the foundational theory), the membership operator "∈", the (extensional) equality "=", and the domain restriction construct "⊳". As can be observed, this proof expressed in this format can be easily understood not only thanks to the tableau method which follows a natural way to find the proof in this case, but also thanks to superdeduction rules which allow us to shorten the proof removing formal details useless for the comprehension of the proof. To justify this claim, let us describe the formal proof sketch which can be extracted from this formal proof, and which is appropriate to provide the intuition of the proof. This formal proof sketch is built as follows:

1. The proof starts from the sequent "⊢ ∅ ⊳ a = ∅", which corresponds to Hypothesis H0 in Step 1 in the formal proof (where the initial formula has been negated since the tableau method works by refutation). The proof rule applied to this sequent is a superdeduction rule which deals with the equality, and which corresponds to the superdeduction rule named "b_not_eq" in the formal proof, i.e. the negation of the equality still because the initial formula has been negated. In sequent calculus, this superdeduction rule is the following:

Γ, x ∈ a ⊢ x ∈ b, ∆ Γ, x ∈ b ⊢ x ∈ a, ∆ =R, x ∈ Γ, ∆ Γ ⊢ a = b, ∆ 2.
Applying the superdeduction rule for equality, we obtain two cases to prove (as shown by the rule above). The formal proof focuses on the right-hand side of the rule at first, and we therefore have to prove the sequent "x ∈ ∅ ⊢ x ∈ ∅ ⊳ a", which corresponds to Step 2. As can be seen, in the set of formulas of each proof step, the formal proof only displays the formulas which are useful to complete the proof. For instance, in Step 2, the formula "x ∈ ∅ ⊳ a" is not displayed (even though it is present in the set of formulas), because it is not used in the following of the proof. The formal proof therefore focuses on the hypothesis "x ∈ ∅" and applies the superdeduction rule named "b_in_empty" and corresponding to the empty set. In B, the empty set is defined as follows: ∅ BIG -BIG. In sequent calculus, the corresponding superdeduction rule is then computed as follows:

Γ, x ∈ BIG, x ∈ BIG ⊢ ∆ ∅L Γ, x ∈ ∅ ⊢ ∆
Once this rule has been applied, we obtain the sequent "x ∈ BIG, x ∈ BIG ⊢ x ∈ ∅ ⊳ a", which is proved by reductio ad absurdum and corresponds to Step 4 in the formal proof.

3. The second case following the application of the superdeduction rule for equality corresponds to the sequent "x ∈ ∅ ⊳ a ⊢ x ∈ ∅", which appears to be Step 3 in the formal proof. In this step, the formal proof focuses on the hypothesis "x ∈ ∅ ⊳ a", and applies the superdeduction rule named "b_in_drest" and corresponding to the domain restriction. This superdeduction rule is the following in sequent calculus:

Γ, x = (y, z), (y, z) ∈ b, y ∈ a ⊢ ∆ ⊳L, y, z ∈ Γ, ∆ Γ, x ∈ a ⊳ b ⊢ ∆
Once this rule has been applied, we obtain the sequent "x = (y, z), (y, z) ∈ a, y ∈ ∅ ⊢ x ∈ ∅", where the formal proof can again focus on the hypothesis y ∈ ∅ in Step 5 and close the proof as previously in Step 6.

From this formal proof sketch, it is now quite easy to produce an informal and short proof (as it would have been done in a textbook) as follows:

• To show ∅ ⊳ a = ∅, we have to consider two cases: given x ∈ ∅, we must show x ∈ ∅ ⊳ a, and given x ∈ ∅ ⊳ a, we must show x ∈ ∅;

1. If x ∈ ∅ then x ∈ BIG and x ∈ BIG, which is therefore absurd;

2. If x ∈ ∅ ⊳ a then x = (y, z), (y, z) ∈ a, and y ∈ ∅, which is absurd as previously.

A Generic Implementation for First Order Theories

In this section, we present our second extension of Zenon with superdeduction, which is able to deal with any first order theory. In this extension, the theory is analyzed to determine the axioms which can be turned into superdeduction rules, and these superdeduction rules are automatically computed on the fly to enrich the deductive kernel of Zenon. We also describe the proofs of two examples coming from the TPTP library and produced by this tool, and which are quite comprehensible as well.

From Theories to Superdeduction Systems

This extension of Zenon is actually a generalization of the previous one dedicated to the B set theory, where superdeduction rules are henceforth automatically computed on the fly. In the previous extension, superdeduction rules are hard-coded since the B set theory is a higher order theory due to one of the axioms of the theory (the comprehension scheme), and we have to deal with this axiom specifically in the implementation of Zenon. Even though some techniques exist to handle higher order theories as first order theories (like the theory of classes, for example), a hard-coding of these theories may be preferred as these techniques unfortunately tend to increase the entropy of the proof search. In addition, in the previous extension, some of the superdeduction rules must be manually generated as they must be shrewdly tuned (ordering the several branches of the rules, for instance) to make the tool efficient. The new extension of Zenon dealing with any first order theory has been developed as a tool called Super Zenon [15], where each theory is analyzed to determine the axioms which are candidates to be turned into superdeduction rules. As said in Section 3, axioms of the form ∀x (P ⇔ ϕ), where P is atomic, can be transformed, but we can actually deal with more axioms.

Here is the exhaustive list of axioms that can be handled, as well as the corresponding superdeduction rules that can be generated (in the following, P and P ′ are atomic, and ϕ is an arbitrary formula):

• Axiom of the form ∀x (P ⇔ ϕ): we consider the proposition rewrite rule R : P → ϕ, and the two superdeduction rules R and ¬R are generated;

• Axiom of the form ∀x (P ⇒ P ′ ): we consider the proposition rewrite rules R : P → P ′ and R ′ : ¬P ′ → ¬P , and only the superdeduction rules R and R ′ are generated;

• Axiom of the form ∀x (P ⇒ ϕ): we consider the proposition rewrite rule R : P → ϕ, and only the superdeduction rule R is generated;

• Axiom of the form ∀x (ϕ ⇒ P ): we consider the proposition rewrite rule R : ¬P → ¬ϕ, and only the superdeduction rule R is generated;

• Axiom of the form ∀x P : we consider the proposition rewrite rule R : ¬P → ⊥, and only the superdeduction rule R is generated.

The axioms of the theory, which are not of these forms, are left as regular axioms. An axiom, which is of one of these forms, is also left as a regular axiom if the conclusion of one of the generated superdeduction rules (i.e. the top formula of one of these rules) unifies with the conclusion of an already computed superdeduction rule (in this case, the theory is actually non-deterministic and we try to minimize this source of non-determinism by dividing these incriminated axioms among the sets of superdeduction rules and regular axioms). An axiom, which is of one of these forms, is still left as a regular axiom if P is an equality (as we do not want to interfere with the specific management of equality by the kernel of Zenon). Finally, it should be noted that for axioms of the form ∀x (P ⇒ P ′ ), we also consider the proposition rewrite rule which corresponds to the converse of the initial formula; this actually allows us to keep cut-free completeness in this particular case.

Proof of a Logic Puzzle

As the Super Zenon tool is able to deal with any first order theory, it can be used in many contexts, and in particular, it can be applied to all the first order problems of the TPTP library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF] (about 6,600 problems), which is a library of test problems for automated theorem proving systems. To assess the effectiveness of this tool and to show that it can also produce comprehensible proofs, let us consider an example of the puzzle category of TPTP and called "Crime in Beautiful Washington" (Puzzle #132), which is a problem in the same vein as the "Who Killed Aunt Agatha?" well-known puzzle. This kind of problems is quite appropriate for educational purposes when teaching artificial intelligence and logic for example. The problem being considered consists of the following axioms:

∀x (capital(x) ⇒ city(x)) (capital _city_type) capital(washington) (washington_type) country(usa) (usa_type) ∀x (country(x) ⇒ capital(capital_city(x))) (country_capital _type) ∀x (city(x) ⇒ has_crime(x))
(crime_axiom) capital_city(usa) = washington (usa_capital _axiom) ∀x (country(x) ⇒ beautiful(capital_city(x))) (beautiful _capital _axiom) As can be observed, all the axioms can be turned into superdeduction rules, except the axiom (usa_capital _axiom) since it is an equality, and the axiom (beautiful _capital _axiom) since one of the generated superdeduction rules for this axiom overlap with one of the superdeduction rules computed previously for the axiom (country_capital _type).

The conjecture to be proved is expressed as follows:

beautiful(washington) ∧ has_crime(washington)

When applied to this specification, Super Zenon produces the proof of Figure 3 for the previous conjecture (we still use the proof format with the highest level of abstraction). As in the example of verification of a B proof rule in Section 4, it is possible to build quite directly the following informal proof sketch from this formal proof:

• To show beautiful(washington) ∧ has_crime(washington), we have to consider the two cases beautiful(washington) and has_crime(washington);

1. To show beautiful(washington), we apply the axiom (beautiful _capital _axiom) instantiated with usa, and we have to consider two cases: we must show country(usa), and given beautiful(capital_city(usa), we must show beautiful(washington);

(a) To show country(usa), we use the axiom (usa_type); 2. To show has_crime(washington), we apply the axiom (crime_axiom), and we must show city(washington);

-To show city(washington), we apply the axiom (capital _city_type), and we must show capital(washington); -To show capital(washington), we use the axiom (washington_type).

Proof of a Geometry Problem

As a second example of proof, we consider a problem coming from the geometry category of the TPTP library. This problem (Problem #170+3) states that if two distinct points are incident with a line, then this line is equivalent with the connecting line of these points. The interest of such an example is actually twofold. First, the corresponding proof is larger (but remains reasonably large to be presented in this paper) than for the previous considered examples, which tends to show that our approach is effective even when the proofs require more than 20 steps. Second, the subject of geometry is quite fundamental in the high school curriculum in the sense that it is generally the only mathematical topic where proofs are explicitly mentioned and where formal reasoning is actually considered. The axioms considered in this example are the axioms of constructive geometry, but Super Zenon uses classical logic and constructive geometry plus classical logic is equivalent to textbook theories. The proof of this example uses the following axioms of this theory (we use the names given in the TPTP files): ∀x, y (distinct_points(x, y) ⇒ ¬apart_point_and_line(x, line_connecting(x, y))) (ci1 ) ∀x, y (distinct_points(x, y) ⇒ ¬apart_point_and_line(y, line_connecting(x, y))) (ci2 ) ∀x, y, u, v (distinct_points(x, y) ∧ distinct_lines(u, v) ⇒ apart_point_and_line(x, u) ∨ apart_point_and_line(x, v) ∨ apart_point_and_line(y, u) ∨ apart_point_and_line(y, v)) (cu1 ) ∀x, y (equal_lines(x, y) ⇔ ¬distinct_lines(x, y)) (ax2 ) ∀x, y (incident_point_and_line(x, y) ⇔ ¬apart_point_and_line(x, y))

where distinct_points(x, y) (resp. distinct_lines(x, y)) means that x and y are two distinct points (resp. lines), incident_point_and_line(x, y) (resp. apart_point_and_line(x, y)) means that the point x is (resp. is not) incident with the line y, equal_lines(x, y) means that x and y denote the same line, and line_connecting(x, y) denotes the line connecting the points x and y.

Among these axioms, the axioms (ci2 ), (ax2 ), and (a4 ) are turned into superdeduction rules. The axiom (ci1 ) is left as an axiom because one of its superdeduction rules overlap with one of the superdeduction rules computed previously for the axiom (ci2 ). The axiom (cu1 ) is also left as an axiom because it has not the right form to be turned into superdeduction rules. It should be noted that for the axiom (ax2 ), a superdeduction rule corresponding to the converse of this axiom is also generated since both sides of the implication are atomic.

The conjecture given previously is formally expressed as follows:

∀x, y, z (distinct_points(x, y) ∧ incident_point_and_line(x, z) ∧ incident_point_and_line(y, z) ⇒ equal_lines(z, line_connecting(x, y)))

When applied to this problem, Super Zenon is able to produce the proof of Figures 4 and5 (we use the same proof format than for the previous examples), where the preliminary Skolemization steps are compressed (Steps 2 and 3 are left implicit). From this proof, it is possible to build the following informal proof sketch as previously:

• Given the points x, y, and the line z s.t. distinct_points(x, y), incident_point_and_line(x, z), and incident_point_and_line(y, z), we have to show equal_lines(z, line_connecting(x, y));

• From the hypotheses incident_point_and_line(x, z) and incident_point_and_line(y, z), we have ¬apart_point_and_line(x, z) and ¬apart_point_and_line(y, z) using the axiom (a4 );

• Using the axiom (ax2 ), the goal equal_lines(z, line_connecting(x, y)) to be proved is equivalent to ¬distinct_lines(z, line_connecting(x, y));

• Using the axiom (cu1 ) with x, y, z, and line_connecting(x, y), we have to show the previous goal in the following cases: 1. Given ¬distinct_points(x, y), we have also distinct_points(x, y) in hypothesis, which is therefore absurd;

(distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### [NotAllEx H0] --> [...]
2. Given ¬distinct_lines(z, line_connecting(x, y)), it is exactly the goal to be proved, which is then proved directly by hypothesis;

3. Given apart_point_and_line(x, z), we have also ¬apart_point_and_line(x, z) in hypothesis, which is therefore absurd;

4. Given apart_point_and_line(x, line_connecting(x, y)), we use the axiom (ci1 ) with x, y, and distinct_points(x, y), to have ¬apart_point_and_line(x, line_connecting(x, y)), which is therefore absurd;

5. Given apart_point_and_line(y, z), we have also ¬apart_point_and_line(y, z) in hypothesis, which is therefore absurd;

6. Given apart_point_and_line(y, line_connecting(x, y)) used with the converse of the axiom (ci2 ) with x and y, we have ¬distinct_points(x, y), which is therefore absurd as we have also distinct_points(x, y) in hypothesis.

Conclusion

In this paper, we have proposed an automated deduction method which allows us to produce proofs close to the human intuition and practice. This method is based on tableaux and uses the principles of superdeduction, among which the theory is used to enrich the deduction system with new deduction rules, called superdeduction rules. We have presented two implementations of this method, which consist of extensions of the Zenon automated theorem prover. The first implementation is a version dedicated to the B set theory, where the superdeduction rules are hard-coded from the initial axiomatic theory. The second implementation is a generic version able to deal with any first order theory, where the theory is analyzed to determine the axioms which can be turned into superdeduction rules, and where these superdeduction rules are automatically computed on the fly to enrich the deductive kernel of Zenon. For information, these two implementations are available as free software at [15]. We have also provided some examples of problems, which can be handled by these tools and which come from different theories, such as the B set theory or theories of the TPTP library (in the puzzle and geometry categories, in particular). In these examples, we have shown that both tools are able to produce formal proofs comprehensible enough to recover the intuition of these proofs, and that the user can therefore easily extract informal proof sketches from these proofs.

As future work, it would be interesting to improve the readability of the produced proofs in order to get more natural proofs and in particular, it might be desirable to turn proofs into pure direct proofs (searching for a proof of the initial formula), rather than refutational proofs (searching to invalidate the negation of the initial formula). In a way, this corresponds to get back to Gentzen's initial purely proof theoretical motivation when trying to find proofs in the cut-free version of sequent calculus, and in particular, this is opposed to Hintikka and Beth's semantic view of tableaux, which consists of a procedure systematically trying to find a counter example for a given formula (i.e. a model in which its negation is true). Such an improvement evokes some similar initiatives in other automated theorem provers, such as Muscadet [16], which is based on natural deduction and which uses methods resembling those used by humans.

To increase the readability of the proofs generated by our extensions, it would also be interesting to export these proofs to other kinds of languages, which appear more appropriate regarding readability. In particular, we could export the proofs to declarative proof languages, such as Isar [22] for Isabelle, which tends to bridge the semantic gap between internal notions of proof given by state-of-the-art interactive theorem proving systems and an appropriate level of abstraction for user-level work. This translation should be automatic, and to be more effective, it should also be probably combined with an interactive layer over the automated deduction tool (see below) in order to produce intelligible proofs, i.e. proofs where a certain number of cuts can be manually introduced. We could even go further and automatically produce proofs in natural languages using, for example, the ideas of [START_REF] Coscoy | A Natural Language Explanation for Formal Proofs[END_REF], where Coq formal proofs are translated in a pseudo natural language.

Finally, in this paper, our extensions only produce proofs automatically without any interaction with the user. In an educational setting, a system able to present sample proofs is already a valuable bonus, but the students must also be involved in the process of building proofs. To do so, the idea is to implement an interactive layer over our extensions in the spirit of [21], which will aim to offer the user the possibility to guide the proof search. This interactive layer would be a benefit for both the user and the automated deduction tool. For the user, this layer could make the interface with the proof engine, which could propose a set of applicable rules or next-step hints. For the automated deduction tool, this layer could be used to find proofs with the help of the user, who could propose to focus on some branches of the proof search, which would allow the tool to find a proof, while the strategy of the tool would have focused on inappropriate branches resulting in an endless proof search.

  fof(simplifyRelDorXY_27, conjecture, b_eq (b_drest (b_empty, a), b_empty)). ( * PROOF-FOUND * ) 1. H0: (-. (b_eq (b_drest (b_empty) (a)) (b_empty))) ### [Extension/b/b_not_eq H0 H1 H2 H3 H4 H5 H6] --> 2 3 2. H2: (b_in T_7 (b_empty)) ### [Extension/b/b_in_empty H2 H8 H9 H7] --> 4 4. H9: (-. (b_in T_7 (b_BIG))) H8: (b_in T_7 (b_BIG)) ### [Axiom H8 H9] 3. H3: (b_in T_7 (b_drest (b_empty) (a))) ### [Extension/b/b_in_drest H3 H10 H11 H12 H7 H6 H13] --> 5 5. H12: (b_in T_14 (b_empty)) ### [Extension/b/b_in_empty H12 H15 H16 H14] --> 6 6. H16: (-. (b_in T_14 (b_BIG))) H15: (b_in T_14 (b_BIG)) ### [Axiom H15 H16]

Figure 2 :

 2 Figure 2: Proof of Rule "SimplifyRelDorXY.27" of Atelier B

Figure 3 :

 3 Figure 3: Proof of Puzzle #132 of TPTP

  fof(geometry_conjecture, conjecture, (! [X, Y, Z] : ((distinct_points (X, Y) & incident_point_and_line (X, Z) & incident_point_and_line (Y, Z)) => equal_lines (Z, line_connecting(X, Y))))). ( * PROOF-FOUND * ) 1. H0: (-. (All X, (All Y, (All Z, (((distinct_points X Y) /\ ((incident_point_and_line X Z) /\ (incident_point_and_line Y Z))) => (equal_lines Z (line_connecting X Y))))))) H1: (All X, (All Y, ((distinct_points X Y) => (-. (apart_point_and_line X (line_connecting X Y)))))) H2: (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\

4 4 .

 4 H7: (incident_point_and_line T_4 T_8) H9: (-. (equal_lines T_8 (line_connecting T_4 T_6))) H10: (distinct_points T_4 T_6) H11: (incident_point_and_line T_6 T_8) ### [Extension/szen/a4 H7 H12 H4 H8] --> 5 5. H12: (-. (apart_point_and_line T_4 T_8)) ### [Extension/szen/a4 H11 H13 H6 H8] --> 6 6. H13: (-. (apart_point_and_line T_6 T_8)) ### [Extension/szen/not_ax2 H9 H14 H8 H15] --> 7 7. H14: (distinct_lines T_8 (line_connecting T_4 T_6)) ### [All H2] --> 8 8. H16: (All Y, (All U, (All V, (((distinct_points T_4 Y) /\ (distinct_lines U V)) => ((apart_point_and_line T_4 U) \/ ((apart_point_and_line T_4 V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) ### [All H16] --> 9 9. H17: (All U, (All V, (((distinct_points T_4 T_6) /\ (distinct_lines U V)) => ((apart_point_and_line T_4 U) \/ ((apart_point_and_line T_4 V) \/ ((apart_point_and_line T_6 U) \/ (apart_point_and_line T_6 V))))))) ### [All H17] --> 10

Figure 4 :Figure 5 :

 45 Figure 4: Proof of Geometry Problem #170+3 of TPTP (Part 1)

The Electronic Journal of Mathematics and Technology, Volume 1,Number 1, ISSN 1933-2823