Guillaume Burel

Ali Assaf

Translating HOL to Dedukti

Dedukti is a logical framework based on the λ Π-calculus modulo rewriting, which extends the λ Πcalculus with rewrite rules. In this paper, we show how to translate the proofs of a family of HOL proof assistants to Dedukti. The translation preserves binding, typing, and reduction. We implemented this translation in an automated tool and used it to successfully translate the OpenTheory standard library.

Introduction

Dedukti is a logical framework for defining logics and expressing proofs in those logics [START_REF] Boespflug | The lambda-Pi-calculus modulo as a universal proof language[END_REF]. Following the LF legacy [START_REF] Harper | A framework for defining logics[END_REF], it is based on the λ Π-calculus modulo rewriting, which extends the λ Π-calculus with rewrite rules. Cousineau and Dowek [START_REF] Cousineau | Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo[END_REF] showed that functional pure type systems (PTS), a large class of calculi that are at the basis of many proof systems, can be embedded in the λ Π-calculus modulo rewriting in a way that is complete and that preserves reductions (i.e. program evaluation). This led to propose Dedukti as a universal proof framework.

In this paper, we focus on translating the proofs of HOL to Dedukti. HOL refers to a family of theorem provers built on a common logical system known as higher-order logic or simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF]. It includes systems such as HOL Light, HOL4, and ProofPower-HOL. These systems are fairly popular and a large number of important mathematical results have been formalized in them [START_REF] Thomas | The Jordan Curve Theorem, Formally and Informally[END_REF][START_REF] Thomas | A Revision of the Proof of the Kepler Conjecture[END_REF][START_REF] Wiedijk | The QED manifesto revisited[END_REF].

Universal proof checking

Using Dedukti as a logical framework serves two goals. First, in the short term, it serves as an alternative, independent proof checker, providing an additional layer of confidence over each system. The second, longer term goal, is interoperability. Proof systems are becoming increasingly important, both in the formalization of mathematics and in software engineering. However, they are usually developed separately, with very little interoperability in mind. As a result, it is currently very difficult to reuse a proof from one system in another one. Embedding these different systems in a single unified framework is the first step to bring them closer together, and opens the way for theory management systems [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF][START_REF] Rabe | A scalable module system[END_REF] to combine their proofs in order to construct and verify larger theories.

The λ Π-calculus as a logical framework

The λ Π-calculus, also known as LF, is a typed λ -calculus with dependent types. Through the Curry-Howard correspondence, it can express a wide variety of logics [START_REF] Harper | A framework for defining logics[END_REF]. Several formalizations of HOL in LF have been proposed [START_REF] Appel | Foundational Proof-Carrying Code[END_REF][START_REF] Schürmann | An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf[END_REF][START_REF] Rabe | Representing Isabelle in LF[END_REF].

The main concept behind this correspondence is the "propositions as types" principle. Typically, we define a context declaring the types, terms, and judgments of the original logic, in such a way that provability in the logic corresponds to type inhabitation in the context. For HOL, the signature would be: type : Type bool : type arrow : type → type → type term : type → Type lam : (term α → term β ) → term (arrow α β ) app : term (arrow α β ) → term α → term β proof : term bool rule_1 : . . . rule_2 : . . .

For each proposition φ of the logic, we assign a type φ in the λ Π-calculus. The provability of the proposition φ corresponds to the inhabitation of the type φ . Similarly, we translate proofs as terms inhabiting those types, and the correctness of the proof corresponds to the well-typedness of the term.

However, because the λ Π-calculus does not have polymorphism, we cannot translate propositions directly as types, as doing so would prevent us from quantifying over propositions for example. Instead, for each proposition φ , we have two translations: one translation |φ | as a term, and another φ = proof |φ | as a type. This correspondence has been successfully used to embed logics in the LF framework [START_REF] Harper | A framework for defining logics[END_REF][START_REF] Geuvers | Some logical and syntactical observations concerning the firstorder dependent type system lambda-P[END_REF], implemented in Twelf [START_REF] Pfenning | System Description: Twelf -A Meta-Logical Framework for Deductive Systems[END_REF].

The λ Π-calculus vs. the λ Π-calculus modulo rewriting An important limitation of LF is that these encodings do not preserve reduction (i.e. program evaluation), and therefore it does not preserve equivalence: if M ≡ β M then |M| ≡ β |M |. For example, the term (λ x : α. x) x is encoded as app (lam (λ x : term α. x)) x which is not equivalent to x. This is problematic not only because it makes the representation larger and hence less efficient but also because conversion proofs may be very long.

By extending the λ Π-calculus with rewrite rules such as

term (arrow α β ) term α → term β ,
we can identify the type term (arrow α β ) with the type term α → term β and thus define a translation that is lighter and that preserves reductions. The encoding of the terms becomes more compact, as we represent λ -abstractions by λ -abstractions, applications by applications, etc. For example, the term (λ x : α. x) x is encoded as (λ x : term α. x) x. Such an encoding is impossible in LF for higher-order theories such as system F, HOL, or the calculus of constructions. Moreover, our translation is modular enough so that we can extend the notion of reduction to the proofs of HOL and recover the pure type system nature of HOL [START_REF] Barendregt | Lambda Calculi with Types[END_REF]. This might be beneficial for several reasons:

1. It gives a reduction semantics for the proofs of HOL.

It allows compressing the proofs further by replacing conversion proofs with reflexivity.

3. Several other proof systems (Coq, Agda, etc.) are based on pure type systems, so expressing HOL as a PTS fits in the large scale of interoperability.

HOL and OpenTheory

The theorem provers of the HOL family (HOL Light, HOL4, ProofPower-HOL, etc.) are built on a common logical formalism known as higher-order logic, and have fairly similar core implementations.

A recurrent issue when trying to retrieve proofs from these systems is that they do not keep a trace of their proofs [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF][START_REF] Keller | Importing HOL Light into Coq[END_REF][START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF]. Following the LCF architecture, they represent their theorems using an abstract datatype and thus guarantee their safety without the need to remember their proofs. This approach reduces memory consumption but hinders their ability to share proofs.

Fortunately, several proposals have already been made to solve this problem [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF][START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF]. Among them is the OpenTheory project. It defines a standard format called the article format for recording and sharing HOL theorems. An article file contains a sequence of elementary commands to reconstruct proofs. Importing a theorem requires only a mechanical execution of the commands.

The format is limited to the HOL family, and cannot be used to communicate the proofs of Coq for example. However, it is an excellent starting point for our translation. Choosing OpenTheory as a front-end has several advantages:

• We cover all the systems of the HOL family that can export their proofs to OpenTheory with a single implementation. As of today, this includes HOL Light, HOL4, and ProofPower-HOL. 1• The implementation of a theorem prover can change, so the existence of this standard, documented proof format is extremely helpful, if not necessary.

• The OpenTheory project also defines a large common standard theory library, covering the development of common datatypes and mathematical theories such as lists and natural numbers. This substantial body of theories was used as a benchmark for our implementation.

Related work

Several formalizations of HOL in LF have been proposed [START_REF] Appel | Foundational Proof-Carrying Code[END_REF][START_REF] Rabe | Representing Isabelle in LF[END_REF][START_REF] Schürmann | An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf[END_REF]. To our knowledge, they lack an actual implementation of the translation. Other translations have been proposed to automatically extract the proofs of HOL to other systems such as Isabelle/HOL [START_REF] Kaliszyk | Scalable LCF-Style Proof Translation[END_REF][START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF], Nuprl [START_REF] Naumov | The HOL/NuPRL Proof Translator[END_REF], or Coq [START_REF] Keller | Importing HOL Light into Coq[END_REF]. With the exception of the implementation of Kalyszyk and Krauss [START_REF] Kaliszyk | Scalable LCF-Style Proof Translation[END_REF], these tools suffer from scalability problems. Our translation is lightweight enough to be scalable and provides promising results. The implementation of Kalyszyk and Krauss is the first efficient and scalable translation of HOL Light proofs, but its target is Isabelle/HOL, a system that, unlike Dedukti, is foundationally very close to HOL Light. ProofCert [START_REF] Chihani | Foundational proof certificates in first-order Logic[END_REF] is another project like Dedukti that aims at providing a universal framework for checking proofs. Unlike Dedukti, it is based on sequent calculus. It can handle linear, intuitionistic, and classical logics. To our knowledge, there are no automated translations of systems like HOL to ProofCert that have been implemented yet.

A project complementary to ours is Coqine [START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo[END_REF], which proposes a translation of the calculus of inductive constructions (CIC), the formalism behind Coq, to Dedukti. The translation has been implemented in an automated tool that translates the proofs compiled by Coq to Dedukti. It can handle most of the features of Coq, and has been used to translate a part of its standard library.

Contributions

We define a translation of the types, terms and proofs of HOL to Dedukti. We use the rewriting techniques of Cousineau and Dowek [START_REF] Cousineau | Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo[END_REF] to obtain a shallow embedding that is lightweight and modular. We implemented this translation in an automated tool called Holide, which automatically translates the proofs of HOL written in the OpenTheory format to Dedukti. We used it to successfully translate the OpenTheory standard library.

Outline

The rest of this paper is organized as follows. Section 2 presents Dedukti and the λ Π-calculus modulo rewriting. Section 3 presents HOL and the logical system behind it. Section 4 defines the translation of HOL to Dedukti. In Section 5, we show that the translation is correct. Section 6 discusses the details of our implementation and the results obtained by translating the OpenTheory standard library. Section 7 discusses some additional applications of rewriting. Finally, Section 8 summarizes and considers future work.

Dedukti

Dedukti is essentially a type checker for the λ Π-calculus modulo rewriting [START_REF] Boespflug | The lambda-Pi-calculus modulo as a universal proof language[END_REF], which extends the λ Πcalculus with rewrite rules. We choose a presentation based on pure type systems [START_REF] Barendregt | Lambda Calculi with Types[END_REF], which makes no syntactic distinction between terms, usually denoted by M or N, and types, usually denoted by A or B.

We assume countably infinite sets of variables and constants. There are two sorts, Type and Kind. The sort Type is the type of types and the sort Kind is the type of Type. We write λ x : A. M for abstractions and M N for applications. The type of functions is written Πx : A. B, or A → B when x does not appear free in B. Application is left-associative while the arrow → is right-associative. Terms are considered up to α-equivalence. Contexts contain the types of variables while signatures contain the types of constants and their rewrite rules. Each rewrite rule is accompanied by a context Γ to ensure it is well-typed.

= x | c | s | Πx : A. B | λ x : A. M | M N contexts Γ, ∆ ::= • | Γ, x : A signatures Σ ::= • | Σ, c : A | Σ, [Γ] M N
If R is a set of rewrite rules, we write -→ R for the induced reduction relation, -→ + R for its transitive closure, -→ * R for its reflexive transitive closure, and ≡ R for its reflexive symmetric transitive closure. Given a signature Σ, we write β Σ for the union of the β rule with the rewrite rules of Σ.

The typing judgments Σ | Γ M : A are accompanied by context formation judgments Σ | Γ context and signature formation judgments Σ signature. We write Γ M : A and Γ context instead of Σ | Γ M : A and Σ | Γ context when the signature is not ambiguous. The rules are presented in Figure 1.

Example 2.2. Let Σ be the signature containing The term λ x : f c. x c x is well-typed in Σ and has the type f c → f c. Notice that this term would not be well-typed without the rewrite rule, even if we replace all occurences of f c by Πy : α. f y → f y.

α : Type, c : α, f : α → Type Γ context (x : A) ∈ Γ Γ x : A VAR Γ context (c : A) ∈ Σ Γ c : A CONST Γ context Γ Type : Kind TYPE Γ A : Type Γ, x : A B : s Γ Πx : A. B : s PROD Γ A : Type Γ, x : A M : B Γ λ x : A. M : Πx : A. B ABS Γ M : Πx : A. B Γ N : A Γ M N : [N/x]B APP Γ M : A Γ B : Type A ≡ β Σ B Γ M : B CONV Σ signature • context EMPTYCTX Γ A : Type x ∈ Γ Γ, x : A context VARCTX • signature EMPTYSIG Σ | • A : s c ∈ Σ Σ, c : A signature CONSTSIG Σ | Γ M : A Σ | Γ N : A Σ, [Γ] M N signature REWRITESIG
Dedukti imposes some additional restrictions on the rewrite rules to keep type-checking decidable. In particular, the left side of a rewrite rule must belong to the higher-order pattern fragment [START_REF] Miller | Unification of simply typed lambda-terms as logic programming[END_REF][START_REF] Miller | Proofs in higher-order logic[END_REF] and the free variables of the right side must appear on the left side. Moreover, the reduction relation -→ β Σ should be confluent and strongly normalizing. This property is not verified by the system and it is up to the user to ensure that it is indeed the case. We discuss this in Section 5.

HOL

There are many different formulations for higher-order logic. The intuitionistic formulation is based on implication and universal quantification as primitive connectives, but the current systems generally use a formulation called Q 0 [START_REF] Peter | An introduction to mathematical logic and type theory: to truth through proof[END_REF] based on equality as a primitive connective. We take as reference the logical system used by OpenTheory [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF], which we will now briefly present.

The terms of the logic are terms of the simply typed λ -calculus, with a base type bool representing the type of propositions and a type ind of individuals. The terms can contain constant symbols such as (=), the symbol for equality, or select, the symbol of choice. The logic supports a restricted form of polymorphism, known as ML-style polymorphism, by allowing type variables, such as α or β , to appear in types. For example, the type of (=) is α → α → bool. Types can be parameterized through type operators of the form p(A 1 , . . . , A n ). For example, list is a type operator of arity 1, and list(bool) is the type of lists of booleans. Type variables and type operators are enough to describe all the types of HOL, because bool can be seen as a type operator of arity 0, and the arrow → as a type operator of arity 2. Hence the type of (= α ) is in fact → (α, → (α, bool())). We still write A → B instead of →(A, B) for arrow types, p instead of p() for type operators of arity 0, and M = N instead of (=) M N when it is more convenient. The propositions of the logic are the terms of type bool and the predicates are the terms of type A → bool. We use letters such as φ or ψ to denote propositions. The contexts, denoted by Γ or ∆, are sets of propositions, and the judgments of the logic are of the form Γ φ . The derivation rules are presented in Figure 2. Example 3.2. Here is a derivation of the transitivity of equality: if Γ x = y and ∆ y = z, then Γ ∪ ∆ x = z.

M = M REFL M Γ M = N Γ λ x : A. M = λ x : A. N ABSTHM x Γ F = G ∆ M = N Γ ∪ ∆ F M = G N APPTHM (λ x : A. M) x = M BETA x M {φ } φ ASSUME Γ φ = ψ ∆ φ Γ ∪ ∆ ψ EQMP Γ φ ∆ ψ (Γ -{ψ}) ∪ (∆ -{φ }) φ = ψ DEDUCTANTISYM Γ φ Γ[σ ] φ [σ ] SUBST σ
((=) x) = ((=) x) REFL ∆ y = z ∆ (x = y) = (x = z) APPTHM Γ x = y Γ ∪ ∆ x = z
EQMP HOL supports mechanisms for defining new types and constants in a conservative way. We will not consider them here. In addition to the core derivation rules, three axioms are assumed:

• η-equality, which states that λ x : A. M x = M,

• the axiom of choice, with a predeclared symbol of choice called select,

• the axiom of infinity, which states that the type ind is infinite. It is important to note that from η-convertibility and the axiom of choice, we can derive the excluded middle [START_REF] Beeson | Foundations of Constructive Mathematics[END_REF], making HOL a classical logic.

Translation

In this section we show how to translate HOL to Dedukti. We define a signature Σ containing primitive declarations and definitions, and a translation function assigning, to every construct of the logic, a term that is well-typed in the signature Σ.

HOL Types

To translate the simple types of HOL, we declare a new Dedukti type called type and three constructors bool, ind and arrow.

type : Type bool : type ind : type arrow : type → type → type One should not confuse type, which is the type of Dedukti terms that represent HOL types, with Type, which is the type of Dedukti types. The translation of a HOL type as a Dedukti term is defined inductively on the structure of the type.

HOL Terms

We declare a new dependent type called term indexed by a type, and we identify the terms of type term(arrow A B) with the functions of type term A → term B by adding a rewrite rule. We also declare a constant eq for HOL equality and a constant select for the choice operator. The symbol term can be seen as a decoding function that assigns a Dedukti type to every HOL type. The translation of a term M of type A will then be a term of type term |A|.

|(λ x : α. x) x| = (λ x : term α. x) x
which is convertible to x.

HOL Proofs

We declare a new type proof, to express the proof judgments of HOL. It is a dependent type, indexed by the proposition φ that it is proving.

proof : term bool → Type We now take care of the derivation rules of HOL (Figure 2). In the following, we write Πx, y : A. B as a shortcut for Πx : A. Πy : A. B.

Equality proofs

We declare Refl, FunExt, and AppThm:

Refl

: Πα : type. Πx : term α. proof (eq α x x) FunExt : Πα, β : type. Π f , g : term (arrow α β ) .

(Πx : term α. proof (eq β ( f x) (g x))) → proof (eq (arrow α β ) f g) AppThm : Πα, β : type. Π f , g : term (arrow α β ) . Πx, y : term α.

proof (eq (arrow α β ) f g) → proof (eq α x y) → proof (eq β ( f x) (g y))

The constant FunExt corresponds to functional extensionality, which states that if two functions f and g of type A → B are equal on all values x of type A, then f and g are equal. We can use it to translate both the ABSTHM rule and the η axiom. Finally, since our encoding is shallow, β -equality can be proved by reflexivity.

D 1 D 2 Γ ∪ ∆ F M = G N APPTHM = AppThm |A| |B| |F| |G| |M| |N| |D 1 | |D 2 | (λ x : A. M) x = M BETA = Refl |B| |M| (where B is the type of M) .

Boolean proofs

We declare the constants PropExt and EqMp:

PropExt : Πp, q : term bool.

(proof q → proof p) → (proof q → proof p) → proof (eq bool p q) EqMp : Πp, q : term bool. proof (eq bool p q) → proof p → proof q

The constant PropExt corresponds to propositional extensionality and, together with EqMp, states that equality on booleans in HOL behaves like the connective "if and only if ". Definition 4.7. The rules ASSUME, DEDUCTANTISYM, and EQMP are translated to {φ } φ ASSUME = h φ (where h φ is a fresh variable)

D 1 D 2 (Γ -{ψ}) ∪ (∆ -{φ }) φ = ψ DEDUCTANTISYM = PropExt |φ | |ψ| λ h ψ : ψ . |D 1 | λ h φ : φ . |D 2 | D 1 D 2 Γ ∪ ∆ ψ EQMP = EqMp |φ | |ψ| |D 1 | |D 2 | .

Substitution proofs

The HOL rule SUBST derives Γ[σ ] φ [σ ] from Γ φ . In OpenTheory, the substitution can substitute for both term and type variables but type variables are instantiated first. For the sake of clarity, we split this rule in two steps: one for term substitution of the form σ = M 1 /x 1 , . . . , M n /x n , and one for type substitution of the form θ = A 1 /α 1 , . . . , A m /α m . In Dedukti, we have to rely on β -reduction to express substitution. We can correctly translate a parallel substitution M[M 1 /x 1 , . . . , M n /x n ] as

(λ x 1 : B 1 . . . . λ x n : B n . M) M 1 . . . M

Implementation

We implemented our translation in an automated tool called Holide. It works as an OpenTheory virtual machine that additionally keeps track of the corresponding proof terms for theorems. The program reads a HOL proof written in the OpenTheory article format (.art) and outputs a Dedukti file (.dk) containing its translation. We can run Dedukti on the generated file to verify it. All generated files are linked with a hand-written file hol.dk containing the signature Σ that we defined in Section 4. Our software is available online at https://www.rocq.inria.fr/deducteam/Holide/. HOL proofs are known to be very large [START_REF] Kaliszyk | Scalable LCF-Style Proof Translation[END_REF][START_REF] Keller | Importing HOL Light into Coq[END_REF][START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF], and we needed to implement sharing of proofs, terms, and types in order to reduce them to a manageable size. OpenTheory already provides some form of proof sharing but we found it easier to completely factorize the derivations into individual steps.

We used Holide to translate the OpenTheory standard library. The library is organized into logical packages, each corresponding to a theory such as lists or natural numbers. We were able to verify all of the generated files. The results are summarized in Table 1. We list the size of both the source files and the files generated by the translation after compression using gzip. The reason we use the size of the compressed files for comparison is because it provides a more reasonable measure that is less affected by syntax formatting and whitespace. We also list the time it takes to translate and verify each package. These tests were done on a 64-bit Intel Xeon(R) CPU @ 2.67GHz × 4 machine with 4 GB of RAM.

Overall, the size of the generated files is about 3 to 4 times larger than the source files. Given that this is an encoding in a logical framework, an increase in the size is to be expected, and we find that this factor is very reasonable. There are no similar translations to compare to except the one of Keller and Werner [START_REF] Keller | Importing HOL Light into Coq[END_REF]. The comparison is difficult because they work with a slightly different form of input, but they produce several hundred megabytes of proofs. Similary, an increase in verification time is to be expected compared to verifying OpenTheory directly, but our results are still very reasonable given the nature of the translation. Our time is about 4 times larger than OpenTheory, which takes about 5 seconds to verify the standard library. It is in line with the scalable translation of Kalyszyk and Krauss to Isabelle/HOL, which takes around 30 seconds [START_REF] Kaliszyk | Scalable LCF-Style Proof Translation[END_REF]. In comparison, Keller and Werner's translation takes several hours, although we should note that our work greatly benefited from their experience.

Extensions

In this section we show some additional advantages of having a translation which preserves reduction.

Compressing conversion proofs

One of the reasons why HOL proofs are so large is that conversion proofs have to traverse the terms using the congruence rules ABSTHM and APPTHM. Since we now prove β -reduction using reflexivity, large conversion proofs could be reduced to a single reflexivity step, therefore reducing the size of the proofs. 3Example 7.1. The following proof of f (g((λ x : A

. x) x)) = f (g(x)), f = f REFL f g = g REFL g (λ x : A. x) x = x BETA g((λ x : A. x) x) = g x APPTHM f (g((λ x : A. x) x)) = f (g x)
can be translated simply as ReflC( f (g x)), where A → B is the type of g and B → C is the type of f .

HOL as a pure type system

It turns out that HOL can be seen as a pure type system called λ HOL with three sorts [START_REF] Barendregt | Lambda Calculi with Types[END_REF][START_REF] Geuvers | Logics and type systems[END_REF]. This formulation corresponds to intuitionistic higher-order logic. However, this structure is lost in the Q 0 formulation used by the HOL systems. Our shallow embedding can be adapted to recover this structure, and thus obtain a constructive and computational version of HOL.

Instead of equality, we declare implication and universal quantification as primitive connectives, and we define what provability means through rewriting.

imp : term (arrow bool (arrow bool bool)) forall : Πα : type. term (arrow (arrow α bool) bool)

[p : term bool, q : term bool] proof (imp p q) proof p → proof q [α : type, p : term (arrow α bool)] proof (forall p)

Πx : term α. proof (p x)

However, this time we do not even need to declare constants like Refl and AppThm for the derivation rules, because they are derivable. Here is a derivation of the introduction and elimination rules for implication for example:

imp_intro : Πp, q : term bool. (proof p → proof q) → proof (imp p q) = λ p, q : term bool. λ h : (proof p → proof q) . h imp_elim : Πp, q : term bool. proof (imp p q) → proof p → proof q = λ p, q : term bool. λ h : proof (imp p q) . λ x : proof p. h x By translating the introduction rules as λ -abstractions, and the elimination rules as applications, we recover the reduction of the proof terms, which corresponds to cut elimination in the original proofs.

As for equality, it is also possible to define it in terms of these connectives. For example, we could use the Leibniz definition of equality, which is the one used by Coq: eq : Πα : type. term (arrow α (arrow α bool))

= λ α : type. λ x : term α. λ y : term α. forall (arrow α bool) (Πp : term (arrow α bool) . imp (p x) (p y))

We would still need to assume some axioms to prove all the rules of OpenTheory, namely FunExt and PropExt [START_REF] Keller | Importing HOL Light into Coq[END_REF], but at least this definition is closer to that of Coq. Since the λ HOL PTS is a strict subset of the calculus of inductive constructions, we can adapt our translation to inject HOL directly into an embedding of Coq in Dedukti [START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo[END_REF], or to combine HOL proofs with Coq proofs in Dedukti [START_REF] Assaf | Mixing HOL and Coq in Dedukti (Rough Diamond)[END_REF]. Further research into ways to eliminate these axioms (and thus maintain the constructive aspect) when possible is the subject of ongoing work.

Conclusion

We showed how to translate HOL to Dedukti by adapting techniques from Cousineau and Dowek [START_REF] Cousineau | Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo[END_REF] to define an embedding that is sound, complete, and reduction preserving. Using our implementation, we were able to translate the OpenTheory standard library and verify it in Dedukti.

Future work

The translation we have presented can be improved in several ways. The current implementation suffers from a lack of linking: if a package makes use of a type, constant, or theorem defined in another package, we do not have a reference to the original definition. This is due to a limitation of the OpenTheory article format. In OpenTheory, this problem is resolved by adding a theory management layer, which is responsible for composing and linking theories together [START_REF] Hurd | The OpenTheory Standard Theory Library[END_REF]. It would be beneficial to integrate this layer in our translation so that we can properly link the resulting files together. While we used several optimizations including term sharing in our implementation, there is still room for reducing the time and memory consumption of the translation and the size of the generated files. The caching techniques of Kaliszyk and Krauss [START_REF] Kaliszyk | Scalable LCF-Style Proof Translation[END_REF] could be used in this regard to handle larger libraries and formalizations.

Finally, we can study how to combine the proofs obtained by this translation with the proofs obtained from the translation of Coq [START_REF] Boespflug | CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo[END_REF]. That will require a careful examination of the compatibility of the two embeddings. First, the types of the two theories must coincide, so that a natural number from HOL is the same as a natural number from Coq for example. Second, we must make sure that the resulting theory is consistent. For instance, we know that every type in HOL is inhabited, which is inconsistent with the existence of empty types in Coq, so we will need to modify the translations to avoid this. A solution is to parameterize each HOL type variable by a witness ensuring that it is non-empty. Our translation can be adapted for this solution without much trouble. Some work has already been done in this direction [START_REF] Assaf | Mixing HOL and Coq in Dedukti (Rough Diamond)[END_REF].

Definition 2 . 1 .

 21 The syntax of the λ Π-calculus modulo rewriting is: variables x, y constants c sorts s ::= Type | Kind terms M, N, A, B ::

Figure 1 :

 1 Figure 1: Typing rules of the λ Π-calculus

Figure 2 :

 2 Figure 2: Derivation rules of HOL

Definition 3 . 1 .

 31 The syntax of HOL is: type variables α, β type operators p types A, B ::= α | p(A 1 , . . . , A n ) term variables x, y term constants c terms M, N ::= x | λ x : A. M | M N | c

Definition 4 . 1 (

 41 Translation of a HOL type as a Dedukti term). For any HOL type A, we define |A|, the translation of A as a term, to be |α| = α |bool| = bool |ind| = ind |A → B| = arrow |A| |B| . More generally, if we have an n-ary HOL type operator p, we declare a constant p of type type → . . . → type n → type, and we translate an instance p (A 1 , . . . , A n ) of this type operator to the term p |A 1 | • • • |A n |.

  term : type → Type eq : Πα : type. term (arrow α (arrow α bool)) select : Πα : type. term (arrow (arrow α bool) α) [α : type, β : type] term (arrow α β ) term α → term β

Definition 4 . 2 (

 42 Translation of a HOL type as a Dedukti type). For any HOL type A, we define A = term |A| .

Definition 4 . 3 (

 43 Translation of a HOL term as a Dedukti term). For any HOL term M, we define |M|, the translation of M as a term to be|x| = x |M N| = |M| |N| |λ x : A. M| = λ x : A . |M| |(= A )| = eq |A| |select A | = select |A| .More generally, for every HOL constant c of type A, if α 1 , . . . , α n are the free type variables that appear in A, we declare a new constant c of type Πα 1 : type. . . . Πα n : type. A and we translate an instance c A 1 ,...,A n of this constant by the term c |A 1 | • • • |A n |. Example 4.4. The term (λ x : α. x) x is translated to

Definition 4 . 5 (

 45 Translation of HOL propositions as Dedukti types). For any HOL proposition φ (i.e. a HOL term of type bool), we define φ = proof |φ | . For any HOL context Γ = φ 1 , . . . , φ n , we define Γ = h φ 1 : φ 1 , . . . , h φ n : φ n where h φ 1 , . . . , h φ n are fresh variables.

Definition 4 . 6 .

 46 The rules REFL, ABSTHM, APPTHM, and BETA are translated to M = M REFL = Refl |A| |M| (where A is the type of M) D Γ λ x : A. M = λ x : A. N ABSTHM = FunExt |A| |B| |λ x : A. M| |λ x : A. N| (λ x : |A| . |D|)

Table 1 :

 1 Translation of the OpenTheory standard library

	Package	Size (kB)		Time (s)
		OpenTheory Dedukti Translation Verification
	unit	5	13	0.2	0.0
	function	16	53	0.3	0.2
	pair	38	121	0.8	0.5
	bool	49	154	0.9	0.5
	sum	84	296	2.1	1.1
	option	93	320	2.2	1.2
	relation	161	620	4.6	2.8
	list	239	827	5.7	3.2
	real	286	945	6.5	3.1
	natural	343	1065	6.8	3.2
	set	389	1462	10.2	5.8
	Total	1702	5877	40.3	21.6

n where B i is the type of M i .

Isabelle/HOL can currently read from but not write to OpenTheory.

The terms soundness and completeness are interchanged in Cousineau and Dowek's paper[START_REF] Cousineau | Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo[END_REF].

This also applies to conversions involving constant definitions, which we did not cover here but are also assumed as an axiom in HOL.

Acknowledgments

We thank Gilles Dowek for his support, as well as Mathieu Boespflug and Chantal Keller for their comments and suggestions.

Correctness

The correctness of the translation is expressed by two properties: completeness and soundness. The first states that all the generated terms have the correct type. For example, the translation of a term of type A has type A while the translation of a proof of φ has type φ . The second states that if a proof term is well-typed in Dedukti, then the proof is correct in the original logic. These two properties ensure that we can use Dedukti as an independent proof checker: we can use it to re-verify the proofs of OpenTheory, and moreover we can be sure that, if a proof is accepted by Dedukti, then it is also valid in OpenTheory.

Completeness

Let Σ be the signature of HOL containing the declarations and rewrite rules of the previous sections. Proof. By induction on the structure of D.

Soundness

Proving the soundness of the embedding is less straightforward than proving completeness. In fact, it is closely related to the confluence and normalization properties of the system. We state the results here and refer the reader to the works of Assaf, Cousineau, and Dowek [START_REF] Assaf | Conservativity of embeddings in the lambda-Pi calculus modulo rewriting[END_REF][START_REF] Cousineau | Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo[END_REF][START_REF] Dowek | Models and termination of proof-reduction in the λ Π-calculus modulo theory[END_REF] for the complete proofs.


Guillaume Bury
email: guillaume.bury@inria.fr

David Delahaye
email: david.delahaye@cnam.fr

Damien Doligez
email: damien.doligez@inria.fr

Pierre Halmagrand
email: pierre.halmagrand@inria.fr

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

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo *

We introduce an encoding of the set theory of the B method using polymorphic types and deduction modulo, which is used for the automated verification of proof obligations in the framework of the BWare project. Deduction modulo is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We also present the associated automated theorem prover Zenon Modulo, an extension of Zenon to polymorphic types and deduction modulo, along with its backend to the Dedukti universal proof checker, which also relies on types and deduction modulo, and which allows us to verify the proofs produced by Zenon Modulo. Finally, we assess our approach over the proof obligation benchmark provided by the BWare project.

Introduction

Reasoning within theories, whether decidable or not, has become a crucial point in automated theorem proving. A theory, commonly formulated as a collection of axioms, is often necessary to specify, in a concise and understandable way, the properties of objects manipulated in software proofs, such as lists or arrays. Each theory has its own features and specificities, but a small number of them appear recurrently, among which arithmetic and set theory. For example, the B method relies on a variant of set theory [START_REF] Hermant | The B-Book, Assigning Programs to Meanings[END_REF], and this theory is supported by some tool sets, such as Atelier B [START_REF][END_REF], which are used in industry to specify and build, by stepwise refinements, software that is correct by design.

The Atelier B tool set still lacks automation: it comes with built-in automated theorem provers but in general a lot of Proof Obligations (POs), often generated during the refinement process, are left to the user. He/she must then discharge POs using the interactive theorem prover or by coming, with new proof rules that must be verified at a later stage, to the rescue of the automated theorem provers. Due to the large practical impact of the B method in particular in industry, the BWare project [START_REF] Delahaye | The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations[END_REF][START_REF]The BWare Project[END_REF] has committed itself to solve this issue by providing a proof platform with several Automated Theorem Provers (ATPs) aiming to support the verification of POs coming from the development of industrial applications.

Leaving the axioms and definitions of set theory at the same level as the hypotheses is not a reasonable option: first, it induces a combinatorial explosion in the search space and second, axioms do not bear any specific meaning that an ATP can take advantage of. To avoid these drawbacks, we replace axioms by rewrite rules, along the lines of deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF], a framework combining first order proof systems with a congruence generated by rewrite rules on terms and propositions. This last distinctive feature allows us to go beyond pure first order reasoning. However, we must take care of preserving desirable properties for proof search, such as consistency, cut elimination, or completeness.

In this paper, we define an encoding of the set theory of the B method as a theory modulo, i.e. a rewrite system rather than a set of axioms. As deduction modulo applies to proof search methods in classical first order logic [START_REF] Bonichon | TaMeD: A Tableau Method for Deduction Modulo[END_REF][START_REF] Dowek | Theorem Proving Modulo[END_REF], we also provide this encoding with an extension of the Zenon tableau-based ATP [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] to deduction modulo, getting a tool called Zenon Modulo [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF]. In addition, this tool features a backend [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF][START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF] to Dedukti [START_REF] Boespflug | The λΠ-Calculus Modulo as a Universal Proof Language[END_REF], a universal proof checker that also relies on deduction modulo, in order to verify the produced proofs [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF].

To cope properly with the POs provided by the industrial partners of the BWare project, we extend, in this paper, Zenon to typed proof search. We therefore provide Zenon with a polymorphic type system, which offers more flexibility, and in particular which allows us to deal with theories that rely on elaborate type systems, like the B set theory. If integrating types to tableaux has already been proposed in [START_REF] Weidenbach | First-Order Tableaux with Sorts[END_REF][START_REF] Giese | A Calculus for Type Predicates and Type Coercion[END_REF][START_REF] Brown | Analytic Tableaux for Simple Type Theory and its First-Order Fragment[END_REF], the novelty consists in considering polymorphic types à la ML, through a type system in the spirit of [START_REF] Blanchette | TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism[END_REF]. In addition and compared to those previous approaches, we also provide one of the very few concrete implementations of ATPs with polymorphic types.

The paper is organized as follows: in Sec. 2, we describe the extension of Zenon to typed proof search using a polymorphic type system; we then introduce, in Sec. 3, the adaptation of Zenon to deduction modulo, as well as our formulation of the B set theory as a theory modulo; finally, in Sec. 4, we describe the experimental results obtained on the benchmark of BWare.

Typed Proof Search for Zenon

In this section, we describe an extension of the Zenon ATP to typed proof search with a polymorphic type system. This extension allows the user to feed the tool with high-level theories as expressed in a flexible way thanks to polymorphism.

Polymorphic Type System

Before introducing the proof search rules of Zenon, which deal with classical first order logic with equality, we extend expressions to polymorphic types à la ML, through a type system in the spirit of [START_REF] Blanchette | TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism[END_REF]. The language of first order expressions with polymorphic types is provided in Fig. 1, where τ is a term-level type, σ a type scheme that may bind type variables, used for polymorphic symbols, and e an expression (term or formula), in which functions and predicates may now be polymorphic and bear type arguments. In this context, formulas may be quantified over types, as long as these quantifications occur before any quantification over terms (not enforced in our simplified Fig. 1). It should be noted that the very expressions of Fig. 1 are used during proof search. This explains why there are metavariables (capitalized here, often named free variables in the tableau-related literature), which are used to find instantiations by unification, as well as Hilbert's -terms ( (x).P (x) is a term/type meaning some x that satisfies P (x), if it exists), an alternative to Skolem terms. If the use of -terms at the level of types may appear as non-standard, it allows us to make the handling of quantification over terms and types uniform. In presence of empty types, these type -terms may introduce inconsistencies, but there is no empty type in our context (each type is inhabited by an infinity of variables of this type). In the sequel, we write e = τ e for ¬(e = τ e ), and f for f () when f has arity 0.

To introduce typing judgments, we need contexts. They contain pairs of symbols with a type: the global context Γ G contains function/predicate symbols and constructors, while the local context Γ L contains term and type variables. A typing context Γ is a pair Γ G ; Γ L . Fig. 2 presents the rules for a single (as customary for pure type systems) typing judgment for expressions, types, constructors, function/predicate symbols, and the Type constant. The relation Γ t : σ means that, in the context Γ, the term (type, expression, etc.) t is well-typed of type (scheme) σ. To factorize rules (e.g., ∀, Meta, or Sym), we embed the term-level types into Kind by the Sub rule. So, κ : Kind is either a term-level type, or Type. Similarly, κ o is either κ, or o (the type of formulas). It should be noted that o is not a type, just as Kind, but a pseudo-type, which does not appear in the syntax of types, and therefore does not have any corresponding typing rule. The usual freshness condition holds in the rules WF 1/2 , App, Var, ∀, ∃, , where in the four last cases, Γ, x : κ denotes Γ G ; Γ L , x : κ.

Γ G being provided by the built-in theory once and for all, we often elide it, writing t : σ for Γ G ; ∅ t : σ, and t 1 , . . . , t n : σ for t i : σ, i = 1 . . . n. In addition, we write ∀x 1 , . . . , x n : κ.e for ∀x 1 : κ. . . . .∀x n : κ.e, where κ is a Kind, as well as for the other binders ∃ and Π.

Proof Search Rules

The rules summarized in Figs. 3 and4 are an adaptation of the rules of Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] to typed formulas. For the sake of simplicity, we have omitted the unfolding and extension rules. The " " symbol is used for closure, while "|" separates two distinct nodes to be created, and R r , R s , R t , and R ts respectively denote reflexive, symmetric, transitive, and transitive-symmetric relations, including equality in particular. It should be noted that the δ and γ rules also deal with quantification over types.

The proof-search algorithm is the usual tableau method: starting from the negation of the goal, apply the rules in a top-down fashion to build a tree. When all branches end with a closure rule, the tree is closed, and it is a proof of the goal. Search is done in strict depth-first order: we close the current branch before we start working on another branch. Moreover, we work in a non-destructive way: extending a branch never changes the formulas elsewhere.

Given an initially well-typed formula, it should be noted that the proof search rules generate only well-typed formulas. All these generated formulas can be typed in the empty local context (we use Church-style -terms, decorating the bound variable with its type, and the metavariables carry their types), which explains the simplified form of the typing side conditions.

Within polymorphic theories, the typed version of Zenon allows us to narrow the search space and produce smaller proofs, since the typing constraints are handled at the metalevel, while the untyped version of Zenon needs an encoding of the polymorphic layer, as in [START_REF] Blanchette | Encoding Monomorphic and Polymorphic Types[END_REF]. This will become clear in Sec. 4 with a comparative benchmark in the B set theory, which is typed.

¬¬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 t : κ P (t) ¬∃x : κ.P (x) γ ¬∃inst t : κ ¬P (t)

Handling Metavariables

In Zenon, metavariables, introduced by the rules γ ∀M and γ ¬∃M , play a special role. They serve to simulate a closure rule to determine a substitution by unification. But we do not substitute them everywhere in the tableau, instead we instantiate the formulas that introduced the metavariables. A single metavariable may therefore generate several instances.

In presence of polymorphism, type metavariables may also be introduced (by the same rules). In contrast with terms, we can afford more simplicity. Figs. 3 and4 have rules with non-linearity constraints (e.g., the type arguments of P in the pred rule) and side conditions (e.g., in the γ ∀inst rule) on types. Type constraints do not turn into regular formulas (in contrast with the a i , b i in pred), so unification is not postponed to closure. Instead, when trying to apply such a rule, we directly look for a (type metavariable) substitution that satisfies the constraints. In case of success, we instantiate the initial formulas. This shortcut minimizes both the search space and the size of proof trees.

As an example, consider a relation P : Πα : Type.α → α → o, and constants τ : Type and a, b : τ . Assuming ∀α : Type.∀x, y : α.P (α; x, y), we prove P (τ ; a, b). The proof is given in Fig. 5 Relational Rules P (τ1, . . . , τm; a1, . . . , an), ¬P (τ1, . . . , τm; b1, . . . , bn) pred ai, bi : (before pruning of useless formulas; see [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF] for more details about pruning) where, once the formula P (A Type ; X AType , Y AType ) is introduced, we try to apply the pred rule, which requires first instantiating the type metavariable A Type with τ .

τ i , i = 1 . . . n a1 = τ 1 b1 | . . . | an =

A Theory Modulo for the B Set Theory

In this section, we introduce the notion of deduction modulo, as well as the corresponding extension of Zenon, and show how to express the set theory of the B method in this framework.

Deduction Modulo

Deduction modulo [START_REF] Dowek | Theorem Proving Modulo[END_REF] reasons over equivalence classes of formulas under a congruence generated by rewrite rules. Compared to [START_REF] Dowek | Theorem Proving Modulo[END_REF], we extend deduction modulo to first order logic with polymorphic types, so as to properly extend the typed proof search method of Zenon of Sec. 2. The language is that of Fig. 1, without metavariables and -terms. A term is an expression that is either a variable or an application, a proposition or formula is an expression that is not a term. In the following, given an expression e, FV(e) and FV τ (e) respectively stand for the set of (type and term) free variables and the set of free type variables of e.

Definition (Class Rewrite System). A term (resp. proposition) rewrite rule is a pair of terms (resp. formulas) l and r together with a local typing context Γ L , denoted l -→ Γ L r, verifying FV(r) ⊆ FV(l) ⊆ Γ L , and s.t. if l is a term, then it is not a variable, and if l is a formula, then it is atomic. An equational axiom is a pair of terms l and r together with a local typing context Γ L , denoted l = Γ L r. Rewrite rules and equational axioms are said to be well-formed in a global typing context Γ G if l and r have the same type in Γ G ; Γ L . A class rewrite system, denoted RE, consists of a set of proposition rewrite rules R and a set of term rewrite rules and equational axioms E. It is well-formed in a global typing context Γ G if all the rewrite rules are well-formed in Γ G .

Given a class rewrite system RE, the relations = E and = RE are the congruences respectively generated by E and R ∪ E.

Definition (RE-Rewriting). Given a global typing context Γ G and a class rewrite system RE that is well-formed in Γ G , a formula ϕ is said to RE-rewrite to ϕ , denoted ϕ -→ RE ϕ , if ϕ = E ψ, ψ |ω = σ(ρ(l)), and ϕ = ψ[σ(ρ(r))] ω , for some rule l -→ Γ L r ∈ R, some formula ψ, some occurrence ω in ϕ, some type substitution ρ, some term substitution σ, and where ψ |ω is the expression at occurrence ω in ψ, and ψ[σ(ρ(r))] ω is the expression ψ where ψ |ω has been replaced by σ(ρ(r)).

If the formula ϕ is well-typed in Γ G , then the type and term substitutions ρ and σ are well-formed in the sense that they replace types or terms with types or terms of the same type, and ϕ has the same type than ϕ in Γ G .

The relation = RE is not decidable in general, but this is in particular the case when -→ RE is confluent and (weakly) terminating, and = E is decidable.

Extension of Zenon to Deduction Modulo

Given a global typing context Γ G and a class rewrite system RE well-formed in Γ G , extending Zenon to deduction modulo then consists in adding to the proof search rules of Figs. 3 and4 the following conversion rule:

P conv, P = RE Q Q
This presentation is more modular than the one described in [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF], where the congruence = RE is part of every proof search rule.

The metavariable instantiation mechanism of Sec. 2.3 needs adaptation: we look for formulas P and Q s.t. P = RE P , Q = RE ¬Q , and there exist a type substitution ρ and a term substitution σ s.t. σ(ρ(P )) = E σ(ρ(Q )). To have a complete rewriting algorithm, we also extend metavariable instantiation to propositional narrowing: we look for a formula P , a type substitution ρ, and a term substitution σ s.t. P = RE P , and there exist P |ω and a rule l -→ Γ L r of RE s.t. σ(ρ(P |ω )) = E σ(ρ(l)).

Rules for a B Set Theory Modulo

Expressing the B set theory as a theory modulo amounts to building an adequate class rewrite system. To do so, we transform whenever possible the axioms and definitions of Chap. 2 of the B-Book [START_REF] Hermant | The B-Book, Assigning Programs to Meanings[END_REF] into rewrite rules (equational axiom are not needed), reusing the infix notation of the B-Book. The resulting theory is summarized in Figs. 6 and7, where we omit the set BIG (an arbitrary infinite set, only used to build natural numbers in the foundational theory), and the sets defined in extension (we only consider the singleton set, which can be used to derive sets defined in extension, and which is also used in other definitions). It should be noted that the constructs and notations are, for a large part of them, specific to the B method, as they are used for the modeling of industrial projects, and are not necessarily standard in set theory.

This theory is typed. The type constructors, i.e. tup for tuples and set for sets, and type schemes of the considered set constructs are provided in Fig. 8 of Appx. A. Type arguments are subscript annotations of the construct; for example, given two expressions s, t : set(τ ), where τ is a type, the intersection of s and t is noted s ∩ τ t, and is s.t. s ∩ τ t : set(τ ). To improve readability, we remove the type annotations in tuples when they are redundant with the membership construct, i.e. given the expressions e 1 , e 2 , and e 3 , s.t. e 1 : τ 1 and e 2 : τ 2 , where τ 1 and τ 2 are two types, (e 1 , e 2 ) τ1,τ2 ∈ tup(τ1,τ2) e 3 is simply noted (e 1 , e 2 ) ∈ tup(τ1,τ2) e 3 .

As can be seen, we only consider first order constructs. This means that we do not handle comprehension (Axiom SET 3 of the B-Book) or lambda abstractions. We therefore eliminate comprehension from the axioms where it appears. For example, the left-hand side formula below is the initial definition of the intersection construct, while the right-hand side formula is its unraveled variant:

s ∩ α t = {x : α | x ∈ α s ∧ x ∈ α t} ∀x : α.x ∈ α s ∩ α t ⇔ x ∈ α s ∧ x ∈ α t
This comprehension-free axiom (the right-hand side formula) can then be easily turned into the following rewrite rule:

x ∈ α s ∩ α t -→ x ∈ α s ∧ x ∈ α t
It should be noted that expressing the B set theory in a polymorphic way is necessary to transform it into a theory modulo, as it allows us to remove the parts of the formulas that are pure type information, and therefore obtain formulas that can be transformed into rewrite Axioms of Set Theory

(x, y) ∈ tup(α 1 ,α 2 ) s ×α 1 ,α 2 t -→ x ∈α 1 s ∧ y ∈α 2 t s ∈ set(α) Pα(t) -→ ∀x : α.x ∈α s ⇒ x ∈α t s = set(α) t -→ ∀x : α.x ∈α s ⇔ x ∈α t Set Inclusion s ⊆α t -→ s ∈ set(α) Pα(t) s ⊂α t -→ s ⊆α t ∧ s = set(α) t Derived Constructs x ∈α s ∪α t -→ x ∈α s ∨ x ∈α t x ∈α s ∩α t -→ x ∈α s ∧ x ∈α t x ∈ s -α t -→ x ∈α s ∧ x ∈α t x ∈α ∅α -→ ⊥ x ∈α {a}α -→ x =α a P1 α(s) -→ Pα(s) -α {∅α} set(α)
Binary Relation Constructs: First Series rules. For example, in pure first order logic (without types), as done in the B-Book, the axiom for intersection is expressed as follows:

p ∈ set(tup(α 1 ,α 2 )) u ↔α 1 ,α 2 v -→ ∀x : α1.∀y : α2.(x, y) ∈ tup(α 1 ,α 2 ) p ⇒ x ∈α 1 u ∧ y ∈α 2 v (y, x) ∈ tup(α 2 ,α 1 ) p -1 α 1 ,α 2 -→ (x, y) ∈ tup(α 1 ,α 2 ) p x ∈α 1 domα 1 ,α 2 (p) -→ ∃b : α2.(x, b) ∈ tup(α 1 ,α 2 ) p x ∈α 2 ranα 1 ,α 2 (p) -→ ∃a : α1.(a, x) ∈ tup(α 1 ,α 2 ) p (x, y) ∈ tup(α 1 ,α 3 ) p;α 1 ,α 2 ,α 3 q -→ ∃b : α2.(x, b) ∈ tup(α 1 ,α 2 ) p ∧ (b, y) ∈ tup(α 2 ,α 3 ) q q •α 1 ,α 2 ,α 3 p -→ p;α 1 ,α 2 ,α 3 q (x, y) ∈ tup(α,α) idα(u) -→ x ∈α u ∧ x =α y (x, y) ∈ tup(α 1 ,α 2 ) s ¡α 1 ,α 2 p -→ (x, y) ∈ tup(α 1 ,α 2 ) p ∧ x ∈α 1 s (x, y) ∈ tup(α 1 ,α 2 ) p £α 1 ,α 2 t -→ (x, y) ∈ tup(α 1 ,α 2 ) p ∧ y ∈α 2 t (x, y) ∈ tup(α 1 ,α 2 ) s -¡ α 1 ,α 2 p -→ (x, y) ∈ tup(α 1 ,α 2 ) p ∧ x ∈α 1 s (x, y) ∈ tup(α 1 ,α 2 ) p -£ α 1 ,α 2 t -→ (x, y) ∈ tup(α 1 ,α 2 ) p ∧ y ∈α 2 t
∀x.s ⊆ u ⇒ t ⊆ u ⇒ (x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t)
The rule corresponding to this axiom requires conditional rewriting (namely the guards s ⊆ u and t ⊆ u, that force s and t to belong to a same superset u: this is how the B-Book gives types to s and t). This has not yet been studied in the framework of deduction modulo (a start in this direction is [START_REF] Burel | Cut Admissibility by Saturation[END_REF]), and guard conditions must be therefore avoided in the axioms as much as possible.

To sum up, our formulation of the BIGand comprehension-free B set theory sticks closely to the B-Book. Still, we need conservativity results, which boils down to cross-derivability of the initial axioms and definitions in our system (completeness) and the formulas associated to our rewrite rules in the initial system (correctness). The correctness of our "inlined" rewrite rules follows from immediate applications of the comprehension axiom itself, but without further considerations, the completeness fails. Sometimes, it is necessary to introduce a set defined by comprehension, for example to prove that "a set is not in bijection with its power set". However, this kind of smart trick is seldom met in practice. This is also related to completeness of the proof search algorithm, which performs in a cut-free calculus. In fact, elaborating a theory Binary Relation Constructs: Second Series modulo does not only consist in turning axioms into rewrite rules, but we must be careful to keep cut-free completeness, especially when this theory is the heart of a proof search method. The problem of cut elimination is known to be very difficult in deduction modulo [START_REF] Bonichon | A Semantic Completeness Proof for Tableaux Modulo[END_REF], and we therefore leave these questions for future work.

x ∈α 2 p[w]α 1 ,α 2 -→ ∃a : α1.a ∈α 1 w ∧ (a, x) ∈ tup(α 1 ,α 2 ) p (x, y) ∈ tup(α 1 ,α 2 ) q + + + < α 1 ,α 2 p -→ ((x, y) ∈ tup(α 1 ,α 2 ) q ∧ x ∈α 1 domα 1 ,α 2 (p)) ∨ (x, y) ∈ tup(α 1 ,α 2 ) p (x, (y, z)) ∈ tup(α 1 ,tup(α 2 ,α 3 )) f ⊗α 1 ,α 2 ,α 3 g -→ (x, y) ∈ tup(α 1 ,α 2 ) f ∧ (x, z) ∈ tup(α 1 ,α 3 ) g ((x, y), z) ∈ tup(tup(α 1 ,α 2 ),α 1 ) prj 1 α 1 ,α 2 (s, t) -→ ((x, y), z) ∈ tup(tup(α 1 ,α 2 ),α 1 ) (s ×α 1 ,α 2 t) × tup(α 1 ,α 2 ),α 1 s ∧ x =α 1 z ((x, y), z) ∈ tup(tup(α 1 ,α 2 ),α 2 ) prj 2 α 1 ,α 2 (s, t) -→ ((x, y), z) ∈ tup(tup(α 1 ,α 2 ),α 1 ) (s ×α 1 ,α 2 t) × tup(α 1 ,α 2 ),α 1 t ∧ y =α 1 z ((x, y), (z, w)) ∈ tup(tup(α 1 ,α 3 ),tup(α 2 ,α 4 )) h|| α 1 ,α 2 ,α 3 ,α 4 k -→ (x, z) ∈ tup(α 1 ,α 2 ) h ∧ (y, w) ∈ tup(α 3 ,α 4 ) k Function Constructs: First Series f ∈ set(tup(α 1 ,α 2 )) s → α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s ↔α 1 ,α 2 t ∧ ∀x : α1.∀y, z : α2.(x, y) ∈ tup(α 1 ,α 2 ) f ∧ (x, z) ∈ tup(α 1 ,α 2 ) f ⇒ y =α 2 z f ∈ set(tup(α 1 ,α 2 )) s →α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s → α 1 ,α 2 t ∧ domα 1 ,α 2 (f ) = set(α 1 ) s f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s → α 1 ,α 2 t ∧ f -1 α 1 ,α 2 ∈ set(tup(α 2 ,α 1 )) t → α 2 ,α 1 s f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t ∧ f ∈ set(tup(α 1 ,α 2 )) s →α 1 ,α 2 t f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s → α 1 ,α 2 t ∧ ranα 1 ,α 2 (f ) = set(α 2 ) t f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t ∧ f ∈ set(tup(α 1 ,α 2 )) s →α 1 ,α 2 t f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t ∧ f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t -→ f ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t ∧ x ∈ set(tup(α 1 ,α 2 )) s α 1 ,α 2 t

Experimental Results

To assess the extensions of Zenon and the design of the B set theory modulo (see Secs. 2 and 3), we use a benchmark of POs provided by the industrial partners of the BWare project [START_REF] Delahaye | The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations[END_REF][START_REF]The BWare Project[END_REF]. This benchmark comes from four anonymized industrial projects that were selected by the industrial partners for the representativity of their POs. The POs are not necessarily tricky mathematical properties, their difficulty comes from their size, the large context provided, or the number of quantified variables (the mean size of the statements of these POs in TFF1 format is 515 KiB, with a maximum of 2,690 KiB). To run the tests, we rely on the BWare verification platform, which we outline briefly. The POs are initially produced by Atelier B.

They are then translated into Why3 files [START_REF] Bobot | Why3: Shepherd Your Herd of Provers[END_REF], using a Why3 encoding of the B set theory [START_REF] Mentré | Discharging Proof Obligations from Atelier B using Multiple Automated Provers[END_REF]. Next, from these files, the Why3 platform produces (through appropriate drivers) the POs for the automated deduction tools. Why3's B set theory is interpreted as rewrite rules (according to Sec. 3) for tools compliant with deduction modulo, otherwise as axioms. As this theory appeals to polymorphism, the output format may be either the new TFF1 format [START_REF] Blanchette | TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism[END_REF] of the TPTP community for the first order polymorphic ATPs (this translation is straightforward as there are very few differences between the polymorphic input language of Why3 and TFF1), or the regular FOF format with an encoding of the polymorphic layer [START_REF] Blanchette | Encoding Monomorphic and Polymorphic Types[END_REF] for the other first order ATPs, or the SMT-LIB format with the same encoding for SMT solvers, except for Alt-Ergo, which features a native format and polymorphism.

The benchmark of BWare consists in 12,876 POs1 , and the experiment was run on an Intel Xeon E5-2660 v2 2.20 GHz computer, with a timeout of 120 s and a memory limit of 1 GiB. The results are summarized in Tab. 1. In these results, the first table focuses on the results for five different versions of Zenon, mainly based on Zenon 0.8.0 and compared to the main prover (mp) of Atelier B 4.0. The second table compares the tools of BWare, i.e. mp, Zenon, Alt-Ergo 0.99.1, and iProver Modulo v0.7+0.2 (an extension of iProver v0.7 to deduction modulo), with a representative panel of first order ATPs, such as Vampire 2.6 and E 1.8, and SMT solvers, like CVC4 1.4 and Z3 4.3.2. Among these tools, only Zenon with deduction modulo and iProver Modulo implement deduction modulo, while only Zenon with types and Alt-Ergo have polymorphic types. Further information regarding this experiment can be found in Appx. C (in particular, the input format of the benchmark and the command line used for each tool are provided).

For both tables, we provide the number of proved POs, the corresponding rate, and the cumulative time for the successfully proved POs (not measured for mp, since it is not possible to split the timeout by PO). The "Unique" line refers to the number of POs that are only proved by a given prover; in the second table, "Uniq. (1)" ranges over the BWare tools, while "Uniq. (2)" considers all the tools. Coverage is given on top of tables; in the second table, we also distinguish the coverage for all the tools and among the BWare tools. In addition, Fig. 9 of Appx. B presents the cumulative times according to the numbers of proved POs, and shows the trends in terms of proof power w.r.t. the time resource.

In the first table, in addition to the regular version of Zenon, we present the extensions with (polymorphic) types, with types and arithmetic, with types and deduction modulo, and with types, deduction modulo, and arithmetic, which is currently the regular version of Zenon Modulo2 . The arithmetic extension [START_REF] Bury | Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)[END_REF] handles linear arithmetic formulas, and relies on the simplex algorithm to compute solutions for systems over rationals, as well as on the branch and bound method to deal with integer systems [START_REF]Linear Programming[END_REF]. As can be observed, the more extensions we plug, the more POs we prove. The most significant gain is provided by the type extension, where we get an increase of about 1755% compared to Zenon. Plugging deduction modulo gives an additional increase of 65%. Finally, connecting arithmetic on top allows us to prove 20% more POs, and to improve by 10 percentage points on mp.

In the second table, we observe that Zenon with types and deduction modulo (but without arithmetic) obtains better results than the first order ATPs Vampire and E w.r.t. the number of proved POs. Vampire remains close to Zenon (10,154 proofs compared to 10,340 proofs for Zenon), but Zenon appears to be about 4 times faster than Vampire over all the proved POs (with a cumulative time of 31,665 s compared to 118,541 s for Vampire). Similarly, Zenon with all the extensions proves more POs than the SMT solvers CVC4 and Z3, except Alt-Ergo. However, it should be noted that CVC4 is close to Zenon (12, The low results of iProver Modulo can be explained by the encoding of polymorphism, which hampers the analysis of the theory and the generation of a rewrite system similar to the one of Sec. 3. As described in [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF], Zenon Modulo enjoys a backend that outputs certificates for Dedukti [START_REF] Boespflug | The λΠ-Calculus Modulo as a Universal Proof Language[END_REF], a universal proof checker for the λΠ-calculus modulo. Since it also relies on deduction modulo, Dedukti natively deals with rewriting and is well-suited to verify the proofs of Zenon Modulo.

In particular, we do not record the rewriting steps in the proofs (these steps are implicitly done by Dedukti), which are therefore quite compact. The logic of Dedukti is constructive, and calls for a translation initially based on an optimized double-negation translation (see [START_REF] Delahaye | Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo[END_REF]). This translation has been replaced by a more syntactical one using excluded middle explicitly (see [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF]), which is more efficient in practice. This backend deals with all the proofs not involving arithmetic, and all the 10,340 relevant proofs of Tab. 1 have been approved by Dedukti.

Conclusion

In this paper, we have observed the benefits of typing and rewriting for automated deduction, implemented in the Zenon Modulo tool, and applied to the B set theory. We have assessed this claim on thousands of POs of the BWare project. Our tool competes with state-of-the-art first order ATPs (without arithmetic) and SMT solvers (with arithmetic), and obtains better results than a large part of them. This tends to show that our tool scales up, and is ready to be applied in any industrial project using the B method. More generally, this work could also be adapted to any framework of formal method based on set theory modeling, as the B set theory includes few specificities compared to Zermelo-Fraenkel set theory for example.

As future work, we aim to integrate conditional rewrite rules to Zenon Modulo along the lines of [START_REF] Burel | Cut Admissibility by Saturation[END_REF], so as to turn more axioms of the B set theory into rewrite rules (currently, some axioms remain, for instance function application). We also plan to study theoretical properties, in particular cut-free completeness. As there is no general way to ensure this in deduction modulo [START_REF] Burel | Regaining Cut Admissibility in Deduction Modulo using Abstract Completion[END_REF], we will probably use specific techniques to our case. We also plan to enhance the Dedukti backend of Zenon Modulo with arithmetic, and make Dedukti understand these computations. We foresee an extension of the conversion rule of Dedukti, shifting from rewriting to reasoning modulo a decision procedure. This would allow us to produce yet more compact certificates. Finally, within the BWare project, we will increase the variety of available domains and applications of the benchmark, by integrating a new large project. The final benchmark will contain more than 80,000 proof obligations, which will be one of the largest academic benchmarks in the domain of program verification. Still in the objectives of BWare, we intend to make this work usable in industry. A first step has been done in this direction in the latest version of Atelier B, which now proposes a Why3 output. To obtain a similar integration of Zenon Modulo, we need to certify it, which should be eased by its ability to produce certificates checkable by Dedukti.

B Cumulative Time Graphs of the Experimental Results

Figure 1 :

 1 Figure 1: Types, Type Schemes, and Expressions

Figure 2 :

 2 Figure 2: Typing Rules

¬

  ¬Rr(τ1, . . . , τm; a, a) r ¬ Rs(τ1, . . . , τm; a, b), ¬Rs(τ1, . . . , τm; b, a) s Analytic Rules

Figure 3 :

 3 Figure 3: Proof Search Rules (Part 1)

  τ n bn f (τ1, . . . , τm; a1, . . . , an) = f (τ1, . . . , τm; b1, . . . , bn) fun ai, bi : τ i , i = 1 . . . n a1 = τ 1 b1 | . . . | an = τ n bn Rs(τ1, . . . , τm; a, b), ¬Rs(τ1, . . . , τm; c, d) sym a, b, c, d : τ a =τ d | b =τ c ¬Rr(τ1, . . . , τm; a, b) ¬refl a, b : τ a =τ b Rt(τ1, . . . , τm; a, b), ¬Rt(τ1, . . . , τm; c, d) trans a, b, c, d : τ c =τ a, ¬Rt(τ1, . . . , τm; c, a) | b =τ d, ¬Rt(τ1, . . . , τm; b, d) Rts(τ1, . . . , τm; a, b), ¬Rts(τ1, . . . , τm; c, d) transsym a, b, c, d : τ d =τ a, ¬Rt(τ1, . . . , τm; d, a) | b =τ c, ¬Rts(τ1, . . . , τm; b, c) a =τ b, ¬Rt(τ1, . . . , τm; c, d) transeq a, b, c, d : τ c =τ a, ¬Rt(τ1, . . . , τm; c, a) | ¬Rt(τ1, . . . , τm; c, a), ¬Rt(τ1, . . . , τm; b, d) | b =τ d, ¬Rt(τ1, . . . , τm; b, d) a =τ b, ¬Rts(τ1, . . . , τm; c, d) transeqsym a, b, c, d : τ d =τ a, ¬Rts(τ1, . . . , τm; d, a) | ¬Rts(τ1, . . . , τm; a, d), ¬Rts(τ1, . . . , τm; b, c) | b =τ c, ¬Rts(τ1, . . . , τm; b, c)

Figure 4 :

 4 Figure 4: Proof Search Rules (Part 2)

Figure 5 :

 5 Figure 5: Proof Search Example with Metavariables

Figure 6 :

 6 Figure 6: Rules of the B Set Theory Modulo (Part 1)

Figure 7 :

 7 Figure 7: Rules of the B Set Theory Modulo (Part 2)

Figure 9 :

 9 Figure 9: Cumulative Times According to the Numbers of Proved POs

  Type . . . αm : Type.τ1 → . . . → τn → τ (polymorphic terms) | Πα1 : Type . . . αm : Type.τ1 → . . . → τn → o

	Term-level Types
		τ ::= α	(type variable)
		|	AType	(type metavariable)
		|	(α : Type).e(α)	(type -term)
		|	f (τ1, . . . , τm)	(type constructor application)
	Type Schemes
	σ ::= Πα1 : (polymorphic formulas)
	|	Πα1 : Type . . . αm : Type.Type	(polymorphic types)
	Expressions
	e ::= x		(variable)
	|	Xτ		(metavariable)
	|	(x : τ ).e(x)	( -term)
	|	e1 =τ e2		(equality)
	|	f (τ1, . . . , τm; e1, . . . , en)	(application)
	|	| ⊥		(true and false)
	|	¬e | e1 ∧ e2 | e1 ∨ e2 | e1 ⇒ e2 | e1 ⇔ e2	(logical connectives)
	|	∀x : τ .e(x) | ∃x : τ .e(x)	(quantifiers over terms)
	|	∀α : Type.e(α) | ∃α : Type.e(α)	(quantifiers over types)

  Type, . . . , αm : Type τi : Type, i = 1 . . . n ΓG; α1 : Type, . . . , αm : Type κo : Kind (or κo = o) Sym ΓG; ∅ f : Πα1 : Type . . . αm : Type.τ1 → . . . → τn → κo

	Well-Formedness Rules
	(∅; ∅) wf	WF0	ΓG; ΓL κ : Kind (ΓG; ΓL, x : κ) wf	WF1	ΓG; ∅ f : σ (ΓG, f : σ; ∅) wf	WF2
	ΓG; α1 : Typing Rules
						Γ P : o Γ P ⇔ Q : o Γ Q : o ⇔
	Γ κ : Kind Γ ∀x : κ.P (x) : o Γ, x : κ P (x) : o	∀	Γ κ : Kind Γ ∃x : κ.P (x) : o Γ, x : κ P (x) : o	∃

Table 1 :

 1 173 proofs compared to 12,281 proofs for Zenon), Experimental Results over the BWare Benchmark and has a significant lower cumulative time (8,378 s compared to 31,689 s for Zenon).

	All Tools (12,738/98.9%)

Γ, x : κ wf Var Γ, x : κ x : κΓG; ∅ κ : Kind Meta ΓG; ΓL Xκ : κ Γ wf Type Γ Type : Kind Γ τ : Type Sub Γ τ : Kind Γ κ : Kind Γ, x : κ P (x) : o Γ (x : κ).P (x) : κ Γ τ : Type Γ a : τ Γ b : τ = Γ a =τ b : o (f : Πα1 : Type . . . αm : Type.τ1 → . . . → τn → κo) ∈ Γ Γ τ i : Type, i = 1 . . . m Γ ei : τi[α1/τ 1 , . . . , αm/τ m ], i = 1 . . . n App Γ f (τ 1 , . . . , τ m ; e1, . . . , en) : κo[α1/τ 1 , . . . , αm/τ m ] Γ wf Γ : o Γ wf ⊥ Γ ⊥ : o Γ P : o ¬ Γ ¬P : o Γ P : o Γ Q : o ∧ Γ P ∧ Q : o Γ P : o Γ Q : o ∨ Γ P ∨ Q : o Γ P : o Γ Q : o ⇒ Γ P ⇒ Q : o

This benchmark is publicly available at: http://bware.lri.fr/.

Available at: https://www.rocq.inria.fr/deducteam/ZenonModulo/.

CeCILL is a French free software license, compatible with the GNU GPL. For more information, see: http://www.cecill.info/licences.en.html.

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

: Πα1, α2 : Type.α1 → α2 → tup(α1, α2) -× -: Πα1, α2 : Type.set(α1) → set(α2) → set(tup(α1, α2)) P(-)

: Πα :

: Πα1, α2 : Type.set(tup(α1, α2)) → set(tup(α2, α1)) dom(-) : Πα1, α2 : Type.set(tup(α1, α2)) → set(α1) ran(-) : Πα1, α2 : Type.set(tup(α1, α2)) → set(α2) -; -: Πα1, α2, α3 : Type.set(tup(α1, α2)) → set(tup(α2, α3)) → set(tup(α1, α3)) -• -: Πα1, α2, α3 : Type.set(tup(α2, α3)) → set(tup(α1, α2)) → set(tup(α1, α3)) id(-)

: Πα :

C Detailed Information regarding the Experiment

The experiment results presented in Sec. 4 were performed over a benchmark of 12,876 POs, which has been provided by two industrial partners of the BWare project. The benchmark is publicly available (under the CeCILL-B license 3 ) at: http://bware.lri.fr/. Several formats are proposed and divided into several archives. The considered formats are the following:

• TPTP FOF (regular TPTP format for mono-sorted first order logic);

• TPTP TFF1 (TPTP format for first order logic with polymorphic types);

• SMT-LIB v2 (regular SMT format for many-sorted first order logic);

• Alt-Ergo (input native format of Alt-Ergo).

The experiment was run on an Intel Xeon E5-2660 v2 2.20 GHz computer, with a timeout of 120 s and a memory limit of 1 GiB. For each tool (except mp, which was tested directly over the native format of POs coming from Atelier B), the following input formats and command lines (where %t is the timeout, %m the memory and %f the file name) were used:

• Zenon Modulo 0.4.1 (Zenon with types, deduction modulo, and arithmetic):

Input format: TPTP TFF1; Command line: "zenon_modulo -p0 -itptp -b-rwrt -rwrt -x arith -max-size %mM -max-time %ts %f".

• iProver Modulo v0.7+0.2: Input format: TPTP FOF; Command line: "iprover_modulo_launcher.sh %f %t --strategies 'Id;Equiv(ClausalAll)' --normalization_type dtree --omit_eq false --dedukti_out_proof false".

• Alt-Ergo 0.99.1: Input format: Alt-Ergo; Command line: "alt-ergo -timelimit %t %f".

• Vampire 2.6: Input format: TPTP FOF; Command line: "vampire --proof tptp --mode casc -t %t %f".

• E 1.8: Input format: TPTP FOF; Command line: "eprover --auto --tptp3-format %f".

• CVC4 1.4: Input format: SMT-LIB v2; Command line: "cvc4 --lang=smt2 --rlimit %t000 %f".

• Z3 4.3.2: Input format: SMT-LIB v2; Command line: "z3 -smt2 -rs:42 %f".