We propose and extension of the tableau-based rst-order automated theorem prover Zenon Modulo to polarized rewriting. We introduce the framework and explain the potential bene ts. The rst target is an industrial benchmark composed of B Set Theory problems. The B Method set theory [1] has been extensively used for 20 years by the railway industry in France to develop certi ed correct-by-construction software. Recently, the BWare [18] project has tackled the issue of automatically proving the thousands of proof obligations generated by the development process. Zenon Modulo [11] is one of the tools developed to this aim. Originally a tableau-based prover, Zenon [4] is used for instance by TLA+ [10] and FoCaLiZe [14]. To help manage the axioms of set theory, but also the uncountable derived constructs de nitions (e.g. inclusion, union, functions), we deemed useful to not let nonlogical axioms wander as formulas: a prover would easily get lost by decomposing one or another axiom in an unorganized fashion. We replaced them with rewrite rules, turning Zenon into an implementation of Deduction Modulo Theory [3,5,13], which allows rewriting on terms and formulas. Additionally, we equipped it with ML polymorphic types and arithmetic [8]. On the BWare benchmark, the success rate was raised from 2.5% to 95%. We propose to extend Zenon Modulo with polarized rewriting, a more permissive rewrite relation. We rst introduce the framework, then we discuss examples and the pros and cons of the approach. There is currently no implementation, essentially because this is a perfect match for an intern or a PhD student.
We assume familiarity with rst-order logic and at least one deduction system.
Tableaux calculus is a refutational calculus, thus, to show F under the
assumptions , we refute ; :F . The rst-order tableaux rules are recalled in Figure 1,
see textbooks [
F; :F :(F _ G) :F; :G
:_ :(F ^ G) :F j :G :^ :>
:> :(F ) G)
F; :G F ) G :F j G )
:) :8x F (x)
:F (c) :9x F (x) :F (t) :8 :9 ::F
F
? :: F _ G F j G ? F ^ G F; G _ 9x F (x)
F (c) 8x F (x)
F (t) 9 8
^
F G , if F (a) General Case
(b) Con uent Case De nition 1 (Polarity of an Occurrence). The occurrence of a formula F in a formula G is positive (resp. negative) i { G is F , { G is G1 ^ G2, G1 _ G2, 8xG1, 8xG1 or H ) G1 and the occurence of F in
G1 or G2 is positive (resp. negative), { G is :G1 or G1 ) H and the occurrence of F in G1 is negative (resp.
positive).
Now, we consider two (proposition) rewrite systems R+ [ R .
De nition 2 (Polarized Rewrite Relation). Let F and G be two formulas. F !+ G i F ! G with a term rewrite rule or there exists a positive (resp. negative) occurrence H in F , a substitution , and a rule l ! r 2 R+ (resp. R ), such that H = l and G is F where H has been replaced with r .
F ! G i :F !+ :G, that is to say we exchange R+ and R above.
We denote by + and the re exive-transitive closures of !+ and ! , respectively. De ning + and is more delicate and unlikely to be useful practice. Polarized Tableaux combine the rules of Figure 1 and Figure 3.
F G + , if F + G Zenon Modulo rewrites only literals, in a forward fashion. This is a further restriction of Figure 2b and it relies on termination of term rewriting and on con uence of the whole rewriting. Otherwise, completeness of the proof search fails. The heuristic is, each time we meet a literal, to: 1. normalize the terms it contains; 2. rewrite the literal itself (if there is an applicable rewrite rule) on one step; 3. if the formula is in normal form or compound, stop, otherwise repeat.
To get polarized rewriting it su ces to modify the second step into \rewrite
positively if the literal is positive, negatively otherwise". The expected gain does
not lie here, but in an optimized preprocessing for rules. Indeed [
Axioms of the form 8x(P ) A) and 8x(A ) P ), with P atomic, become rules of R+ and R , respectively. In classical logic, when P is a negated atom, we also get rewrite rules in R and R+, respectively. { We can Skolemize rewrite rules. This has two bene ts: rst, less inference rules are necessary in the tableaux, and second, the Skolem term is uniform, while multiple applications of 9 or :8 introduce di erent fresh symbols at each time. This also holds in the presence of meta-variables.
Skolemizing the rules is impossible in vanilla Deduction Modulo Theory, as rewriting applies at positive and negative occurrences. Therefore, we do not know in advance which quanti ers are positive and negative. To illustrate the di erence, consider axioms of the type 8x(P ) A) and 8x(A ) P ). { In 8x(P ) A), we can replace all the positive existential and negative universal quanti ers of A by a Skolem function symbol. { Similarly, in 8x(A ) P ), we can replace all the positive universal and negative existential quanti ers of A by a Skolem function symbol.
The very same principle applies to polarized rewrite rules. We leave the
study and the choice of the strategies for Skolemization [
Let us consider the classical example of proving a a with the standard axiom of inclusion 8x8y x y , (8z z 2 x ) z 2 y). A usual tableau proof involves the succession of rules 8 (twice), ^, ), :8 and :) on the axiom. Deduction Modulo Theory turns it into the rewrite rule x y ! (8z z 2 x ) z 2 y), and yields the 3-rules axiomless proof of Figure 4a.
If we switch to Polarized Deduction Modulo Theory, we get the pair R+ = fx y ! (8zz 2 x ) z 2 y)g and R = fx y ! (f (x; y) 2 x ) f (x; y) 2 y)g. The proof of a a is one more step smaller, as shown in Figure 4b. :8 :) :(a
a) :(8z z 2 a ) z 2 a) :(c 2 a ) c 2 a) :(c 2 a); c 2 a :(a
a) :(f (a; a) 2 a ) f (a; a) 2 a) :(f (a; a) 2 a); f (a; a) 2 a :) (a) Pristine Tableaux
(b) Polarized Tableaux We expect the polarized approach to give at least as e cient as Zenon Modulo itself. The proof-search algorithm needs only few changes, mostly in the rule pre-processing. The obtained rules contain less quanti ers, allowing for fewer rules in proof-search and potential earlier uni cation and branch closure, since using a rewrite rule several times now involves the same Skolem symbol.
On the risk side, implicational axioms can now be turned into rewrite rules. This might be a threat to termination or con uence. A study of the theoretical framework, including models, is required.
Automated theorem provers are aggressively optimized tools, naturally
lending themselves to bugs. This is why independent double checking facilities are
important. Zenon Modulo is able to produce proof-terms or proof certi cates,
though it provides no rewrite steps explicitly, following Poincare's Principle:
computations (rewriting) in proofs give no insight, they can be quickly
reconstructed (by the checker) at will and are to be left implicit. Such a clerk/expert
distinction has for instance been studied in the Foundational Proof Certi cate
project [
On the BWare benchmark, all statements proved by Zenon Modulo [
The challenge is to keep this skeptical double-checking approach viable. We
may need a depolarization of the proofs, perhaps following [