Simplification with Renaming: A general proof technique for tableau and

sequent-based provers

Fabio Massacci^{1} Computer Laboratory,

University of Cambridge (UK)

and

Dipartimento di Informatica e Sistemistica, University of Roma “La Sapienza” (I)

May 19, 1997

1Current address: Dipartimento di Informatica e Sistemistica, via Salaria 113, I-

00198 Roma, Italy, e-mail: massacci@dis.uniroma1.it

Abstract

Tableau and sequent calculi are the basis for most popular interactive theorem provers for hardware and software verification.

Yet, when it comes to decision procedures or automatic proof search, tableaux are orders of magnitude slower than Davis-Putnam, SAT based procedures or other techniques based on resolution.

To meet this challenge, this paper proposes a theoretical innovation: the rule of simplification, which plays for tableaux the same role of subsumption for resolution and unit for Davis-Putnam.

This technique gives an unifying view of a number of tableaux-like calculi such as DPLL, KE, HARP, hyper-tableaux etc. For instance, the stand-alone nature of the first-order Davis-Putnam-Longeman-Loveland procedure can be explained away as a case of Smullyan tableau with propositional simplification.

Beside its computational effectiveness, the simplicity and generality of simplification make possible its extension in a uniform way. We define it for propositional and first order logic and a wide range of modal logics. For a full-fledged first order simplification we combine it with another technique, renaming, which subsumes the use of free universal variables in sequent and tableau calculi.

New experimental results are given for random SAT and the IFIP benchmarks for hardware verification.

Contents

1 Introduction 1 1.1 Plan of the paper . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Principles and Intuitions 3 2.1 Simplification as “Top-Down Subsumption” . . . . . . . . . . . . 3 2.2 Renaming for First Order Formulae . . . . . . . . . . . . . . . . 4 2.3 A General Definition . . . . . . . . . . . . . . . . . . . . . . . . . 4

3 Notation and Terminology 5

4 Propositional Logic 7 4.1 Examples and Comparison . . . . . . . . . . . . . . . . . . . . . . 8 4.2 Subsuming other approaches . . . . . . . . . . . . . . . . . . . . 9 4.3 Further Forms of Simplification . . . . . . . . . . . . . . . . . . . 11

5 Modal Logics from K to S5 13

6 Renaming and First Order Logic 15 6.1 Ground Sequents and first order DPLL . . . . . . . . . . . . . . . 15 6.2 Free Variables Sequents with Renaming . . . . . . . . . . . . . . 15 6.3 Examples and Properties . . . . . . . . . . . . . . . . . . . . . . 17 6.4 Proving Soundness and Completeness . . . . . . . . . . . . . . . 19

7 Experimental Analysis 20 7.1 Random 3-CNF . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.2 IFIP benchmarks for Hardware verification . . . . . . . . . . . . 20

8 Conclusion 22 ii CONTENTS

1 Introduction

It is a widespread belief that methods based on the sequent calculus (such as tableaux) are hopeless for “real life” satisfiability and validity search. Even for decidable problems with a natural appeal for tableaux, such as modal or propositional logics, experimental results have shown that other algorithms outperform them by orders of magnitude [9, 18, 24, 34, 42].

Such a huge gap leads to think that this is not a matter of efficient implementations^{1} but rather of theoretical nature. The key question is whether such a gap is inherent to tableaux methods or something is simply missing.

This answer is not only of theoretical relevance but has an extreme importance for the future development of hardware and software verification tools.

Indeed, variants of the sequent calculus are the main techniques used by interactive theorem provers, such as Isabelle [29], PVS [33] or HOL [1, 19]. Those provers have successfully tackled hardware and software verification and often require to prove some properties in decidable sub-theories such as propositional logic (e.g. a N-bits binary adder) or fragments of arithmetics [1, 33]. If tableauxlike methods are “hopeless by nature”, then using ad-hoc tactics (in the general calculus) for decidable sub-theories would be impractical for hw/sw verification. Rather, non sequent-based systems (outside the prover) should be consulted as oracles. For instance the use of particularly efficient algorithms for propositional logics as one-off “derived rules” for HOL has been proposed in [22, 23]. Yet the risk is that the concept of proof (and verification) would then be shaded by many black-box steps.

To fill the computational gap, a number of works have improved the effectiveness of tableaux method by switching from ground calculi to free variables versions [31, 16] with smart skolemisation techniques [2], adding ad-hoc rules for modus ponens and tollens [10, 24, 28], imposing regularity conditions [10, 25], using controlled form of cut [25, 10], or factoring and merging [27, 41], exploiting universal variables [7, 4], incorporating features of hyper-resolution [3]. They have improved the efficiency of the calculus but sometimes at the expenses of the generality and simplicity of the rules (its main appeal for interactive prover and proof presentation). In some cases [9] the quest for an efficient implementation has lead from an original sequent calculus to a (seemingly different) Davis-Putnam procedure.

We propose a general (and hopefully simpler) technique, which subsumes a number of these approaches, and whose intuition is due to an interesting comparison between tableaux and their “historical competitors”.

Since the very beginning, Davis-Putnam procedure [13] or its enhanced variant [12] in cooperation with Longeman and Loveland (DPLLfor short), and resolution [32] included rules for the simplification of the formulae to be proved unsatisfiable (e.g. unit or subsumption) without changing the basic inference mechanism.

In a nutshell, techniques for “eliminating the irrelevant from mechanical proofs” [11] were immediately considered and embedded in the proof procedure. The implementation of this simplification procedures is almost a research field in itself [40, 42] and difficult problems could hardly (if at all) be solved by either resolution or DPLL without using them. On the contrary, even in the modern texts on tableaux [16] everything is proved by “first principles”.

1Although this helps: the connection tableaux based prover SETHEO has won the CADE-96 automatic provers competition.

We advocate that this lack of “rules for simplification” is the main cause for the computational gap^{2}. Hence we need a simple theoretical innovation: an operation plays for the sequent calculus the same role of unit for DPLL and subsumption for resolution. We call it simplification and discuss its application to propositional, modal and first order logics.

While propositional and modal logics can be uniformly treated without much changes, the effective use of simplification for first order logic requires a new concept. In the same way that variables are “implicitly quantified” in a clause (and in the corresponding subsumption procedure), we modify the sequent calculus to make explicit the notion of universal and rigid variables. We call this technique renaming. It generalizes the use of universal variables introduced by [6] and enhance the possibilities of simplification.

The simplicity and flexibility of simplification makes it possible its application to a wide range of logics and logical formalism, as soon as there is sequent calculus. The only difficult feature is the enhancement of simplification as we “upgrade” the logic. Its effectiveness can enhance the computational power of interactive and automatic tableaux based provers.

The introduction of simplification for the sequent calculus provide also an unifying perspective of many (tableaux based) deduction techniques and, notably, “explains away” the stand-alone characteristic of the DPLL procedure (or KSATprocedures of [17] which are based on DPLL). For instance the first order version in [12] can be “re-interpreted” as a tableau á la Smullyan “plus” propositional simplification. Such an interpretation can also explain the comparative inefficiency of first-order DPLL versus propositional DPLL.

We also show the practical impact of the operation of simplification on the performance of tableau methods: a simple Prolog implementation shows essentially the same easy-hard-easy computation pattern for random 3-SAT shown by DPLL [9] even with a a simpler notion of simplification than the full fledged used by DPLL. We also show some results on the IFIP benchmarks for hardware verification which are highly non clausal.

1.1 Plan of the paper

In what follows, we present the intuitions and the principles behind simplification and renaming (§2). After the introduction of some preliminary notation and terminology (§3), we show the uniform application of these techniques to propositional (§4), modal (§5) and first order logics (§6). In each section we show how this methods provide a general framework which explains away a number of related works presented in the literature. Next we report briefly on a number of benchmarks (§7) and conclude (§8).

2This has also been confirmed for modal logics by recent experimental studies [24] which clarified the gap between KSAT and tableaux based procedures.

2 Principles and Intuitions

We assume a basic knowledge of the sequent calculus (see [35] for an introduction). In the sequel formulae are denoted by A, B, C, sets of formulae by Γ, Δ and sequents by Γ ⟹ Δ. The (usual) interpretation is that if all formulae of Γ are true then at least one formula of Δ is true.

2.1 Simplification as “Top-Down Subsumption”

The intuition behind simplification is rather simple and can be better explained by comparing it with subsumption, to show the duality between top-down (tableaux) and bottom-up (resolution) methods

Intuition 1 : Bottom-up methods explore the search space by generating new information and to simplify the search they retain information to discard (newly generated) irrelevant facts. On the contrary, top-down methods work by breaking existing information and therefore the best way to delete irrelevant information should be anticipating the outcome of the search.

For example, consider the following α-rule:

{Γ, A, B ⟹ Δ \atop Γ, A ∧ B ⟹ Δ} (α)

After this rule a tableau will continue to break down connectives until a branch closure rule can be applied. It is looking for something like Γ, C ⟹ Δ, C.

Yet, after the α-step, there is some information that the calculus does not use to anticipate the outcome of its search: when all formulae in of Γ ∪ {A, B} are true then A must be true, no matter what A is (equally for B). We can use this information about A to simplify Γ and Δ before reducing other connectives.

The simplest way is a syntactic search: look for all exact^{3} occurrences of A in Γ and replace it with the propositional constant ⊤; next perform some boolean operations to eliminate ⊤ and ⊥ from the formula; only afterwards continue with further rules.

The computational pay-off may seem doubtful: some time must be spent for scanning the formula replacing the occurrences with ⊤; eliminate boolean constant and so on. So what could be the gain?

Intuition 2 : The sequent proof of Γ ⟹ Δ is potentially of size O(2|Γ ∪ Δ|) [39]. If can reduce Γ ⟹ Δ to Γ^{∗} ⟹ Δ^{∗} so that its size decreases, if only by 1, we would reduce the potential search space at least by half.

We trade off some polynomial processing for an exponential gain: scanning the formula and looking for “exact” copies can be done in polynomial time; the boolean reduction is guaranteed by the following property.

Proposition 1 Let φ be a formula in a logic containing the propositional calculus, then reducing ⊤ and ⊥ from φ through boolean operations only require O(|φ|). The size of the reduced formula φ^{∗} is such that |φ^{∗} | ≤ |φ|.

3With modal connectives or variables it is not so simple but this is an intuitive explanation.

For propositional logic the inequality is always strict if there is at least one occurrence of ⊤ or ⊥ in φ and so is for first order logic. In case of modal logic it is almost always strict with just two particular exceptions^{4}.

Hence, if there is at least another occurrence of A (or B) in Γ, it always pays off to replace this occurrence with ⊤: the resulting sequent will be smaller and thus the proof tree below will also be (exponentially) smaller.

2.2 Renaming for First Order Formulae

As soon as we admit free variables in our picture there is a new difficulty: how do we know whether p(x, a) “equals” the subformula p(y, a) in ∀y.p(y, a)?

Of course we could limit the operation of simplification to closed sentences and therefore fall back on propositional simplification. We should only worry of identity up to renaming of bound (mute) variables. However this is a very limited choice (as we shall see this is exactly what first order DPLL does).

To obtain an enhanced version we must give an answer to the above question. From a syntactic perspective, the simplest way would be to rename x to y so

to make the above formulae exactly identical. The problem is that this operation cannot always safely done unless x is “implicitly” universally quantified.

Again looking to resolution may be useful: variables in a clause are implicitly universally quantified. We combine this idea with the technique of universal variables of [6, 4]. Thus, rather than explicitly indicating the universal variables as in [7] we take the dual view: indicate in the sequent explicitly the rigid variables, assuming all the others as implicitly universal. Then a new rule (renaming) can be used to rename variables for further and enhanced steps of simplification.

2.3 A General Definition

We must be careful in the definition of simplification rules, otherwise we could (i) shift the cost of the proof search in the simplification step and (ii) obtain exactly the kind of black box operation we want to avoid. So we propose the following general definition:

Definition 1 Let C be a sequent calculus for a logic including the propositional calculus, a simplification rule for C is a rule of the form:

{Γ^{∗} ⟹ Δ^{∗} \atop Γ ⟹ Δ} simp

where the following properties hold:

1. the end-sequent is logically equivalent to the upper sequent;

2. Γ^{∗} (resp. Δ^{∗}) is obtained by Γ (resp. Δ) by replacing suitable subformulae of either Γ or Δ with ⊤ or ⊥ and by subsequentely reducing those constants; 3. the time complexity of this replacement is bounded by O(poly(|Γ ∪ Δ|))

4Namely □⊥ and ¬◇⊤ cannot be reduced to ⊥ in a non deontic logic [15, 21].

where poly is a polynomial;

4. the size of the end-sequent is not increased i.e. |Γ^{∗} | ≤ |Γ| and |Δ^{∗} | ≤ |Δ| (in general smaller).

The first condition is to retain soundness and completeness w.r.t. C, if we give to simplification a strict precedence over other rules. Otherwise we could waive the completeness requirement (we will do so for a particular form of simplification) and obtain an “unsafe” rule, i.e. a rule was application may prevent the finding of a proof in the terminology of interactive theorem proving [29].

Intuition 3 : Our objective is to obtain Γ^{∗} ⟹ Δ^{∗} by simple syntactic checking and rewriting since:

1. it does not change the simple nature of the sequent calculus;

2. it is simple and effective to implement;

3. interactive provers have fairly developed and effective tactics to incorporate such operations.

In the sequel we simplify only w.r.t. one formula (not necessarily atomic). Positive simplification of Γ by A, denoted by Γ[t.A], is the operation where A (or some suitable subformula) is replaced by ⊤. In a dual way we have direct negative simplification, denoted by Γ[f.A] when A is replaced by ⊥.

Simplification rules will then have a form like

{Γ[t.A], A ⟹ Δ[t.A] \atop Γ, A ⟹ Δ} pos

{Γ[f.A] ⟹ Δ[f.A], A \atop Γ ⟹ Δ, A} neg

The key advantage of this definition and the rules we have proposed is that when we “upgrade” the logic we do not have (in general) to change the rules but only specify the behavior of the operation B[t.A] and B[f.A] w.r.t. the new connectives we have introduced. The flexibility and modularity makes it easy also to upgrade current implementations with these techniques.

3 Notation and Terminology

We assume some basic familiarity with the standard syntax and semantics of propositional, modal and first order logic. For an introduction see [16, 35] for propositional and first order logic and [15, 21] for propositional modal logics.

For propositional logic we construct formulae A, B, C from a set of propositional atoms p, q ∈ P and the boolean constant ⊤ and ⊥ with the logical connectives ∧, ∨, ¬, ⊃ etc. Propositional modal logics are obtained by adding the unary operators □ (necessity) and ◇ (possibility).

α  α_{1} α_{2}
t.A ∧ B t.A t.B
f.A ∨ B f.A f.B
f.A ⊃ B t.A f.B

\begin{matrix}α & α_{1} = α_{2} \\ t.¬A & f.A \\ f.¬A & t.A \end{matrix} β  β_{1} β_{2}

f.A ∧ B f.A f.B
t.A ∨ B t.A t.B
t.A ⊃ B f.A t.B
\begin{matrix}ν & ν_{0} \\ t.□A & t.A \\ f.◇A & f.A \end{matrix} \begin{matrix}π & π_{0} \\ f.□A & f.A \\ t.◇A & t.A \end{matrix} \begin{matrix}γ & γ_{0}(t) \\ t.∀x.A(x) & t.A(t) \\ f.∃x.A(x) & f.A(t) \end{matrix} \begin{matrix}δ & δ_{0}(t) \\ f.∀x.A(x) & f.A(t) \\ t.∃x.A(x) & t.A(t) \end{matrix}

Table 1: Uniform notation

For first order logics we denote constants by a, b, c ∈ Const and functions by f, g ∈ Fun while variables are denoted by x, y, z, … ∈ Var and terms by t. The usual definition for ground terms is also adopted [16, 35]. The symbol p(…), q(…) represents predicates. The operator for universal and existential quantification are standard: ∀x.A and ∃x.A. By F V (A) we denote the set of free variables occurring in the formula A, and with A(x) we mean that the variable x may occur free in the formula A and A(t) denotes the uniform substitution of t for x in A (see [16, 35]). F V is extended to set of formulae in the obvious way.

For first order logic we will need the concept of substitution, denoted by σ, ρ, where σ = {t_{1}/x_{1}, …, t_{n}/x_{n}} [16, 32]. If R ⊂ Var is a set of variables we denote by σ_{/R} the substitution {t_{1}/x_{1}, …, t_{n}/x_{n}} where each x_{i} ∉ R. A particular form of substitution, called renaming, is denoted by η = {v_{1}/x_{1}, …, v_{n}/x_{n}} where each v_{i} is a fresh variable distinct from all other v_{j}. By Aσ we denote the application of the substitution σ to the formula A. We also employ the usual concept of substitution free for a formula (the variables of t_{i} do not get bound after the substitution for t_{i} for x_{i}).

Sets of formulae are represented by Γ and Δ and a sequent, written using Gentzen notation, is the pair Γ ⟹ Δ. The usual semantic interpretation is that if all formulae of Γ are true then at least one formula of Δ is true. For first order logic we will introduce a new form of sequent, namely a triple: Γ ⟹^{R} Δ where R is a set of variables such that R ⊆ F V (Γ) ∪ F V (Δ)

For sake of modularity and compactness we use signed formulae and the α, β, γ, δ notation introduced by Smullyan [36] and extended to modal logic by Fitting [15]. Thus a signed formula, denoted by φ and ψ, is a pair t.A or f.A. The intuitive interpretation is that A is assumed to be respectively true and false. The conjugate of a signed formula φ, denoted by \overline{φ}, is obtained by switching t. with f. and viceversa.

The uniform classification of formulae is given in Table 1. For sake of simplicity negation has been classified as a formula of type α (see [15] for a different classification for intuitionistic logic). With signed formula a sequent Γ ⟹ Δ is represented as set S of signed formulae as follows [36]:

S = {t.A | A ∈ Γ} ∪ {f.A | A ∈ Δ}  (1)

S, f.⊤ (⊤)  S, t.⊥ (⊥)  S, φ, \overline{φ} (Ax)

{S, α_{1}, α_{2} \atop S, α} (α) \begin{matrix}S, β_{1} & S, β_{2} \\ S, β \end{matrix} (β) {S, ψ[φ], φ \atop S, ψ, φ} (simp)

{S \atop S, φ} (thin)  \begin{aligned}S, φ & & S, \overline{φ} \\ & S \end{aligned} (cut)

Figure 1: Propositional Sequent Rules with Simplification

We also abbreviate S ∪ {φ} as S, φ. In this set-oriented framework the usual structural rules such as weakening and contraction [37] become redundant. The “triple” version of a sequent Γ ⟹^{R} Δ will be denoted by S : R.

4 Propositional Logic

The rules and axioms of the calculus are given in Fig. 1 the only new rule (simp), which we call local simplification. The use of signed formulae makes the definition of rule (simp) extremely compact. Without signs we would have had the derivation rules of §2 if we repeatedly applied (simp) wrt φ to all formulae ψ in S.

Rule (thin) is not necessary and (cut) can be eliminated [37, 35, 16]. We introduce them to show that some particular forms of simplification are derived by them with (simp).

We refer to formulae (rules) as positive or negative according their sign (the sign of the main formula). In the examples we use the Γ ⟹ Δ notation without signed formulae in the obvious way.

The definition of search tree and proof tree are standard [16, 35]: a sequent search tree is a dyadic tree where each node is labelled by a sequent, the root is labelled with the sequent we are trying to prove and, for each node, its children are labelled with the corresponding consequents of a rule of the calculus. A proof is a search tree where each leaf is labelled with an axiom. In the sequel we will also use the notion of a frontier of a sequent search tree T : it is the collection of all leaves of the tree and is denoted by S_{1} | … | S_{n}. If we view the proof tree as a (reversed) tableau the frontier is simply the collection of the current branches of the tableau [7, 14, 16].

The next step to complete our machinery, is the definition of the proper operation of simplification ψ[φ]. Clearly signs will be left unchanged and we have just to specify the progression over formulae. In the following definition ♯ is any binary (propositional) connective.

A[φ] ↦ \{ \begin{matrix}⊤ & if φ = t.A \\ ⊥ & elseif φ = f.A \\ ¬(B[φ]) & elseif A = ¬B \\ B[φ] ♯ C[φ] & elseif A = B♯C \\ A & otherwise \end{matrix}  (2)

By A = B we mean, at this preliminary stage, syntactic identity. So A ∧ B is different from B ∧ A. Further extensions, where the commutative properties of the connectives are considered are described in the following subsections.

There is a number of observations worth making:

1. we do not only reduce branching, we get smaller and simpler formulae

2. the operation of simplification is parametric wrt the connectives used;

3. the simplifying formula φ needs not be a literal nor have any special normal form;

4. without restriction, simplification can procede recursively down any level of nesting of propositional connectives.

The last step is one of the key differences with modus ponens and tollens applied in HARP [28], the KE β^{c}-rules [10] and the ∨−simp_{0,1}-rule used in [24]. Indeed we will show that they are particular forms of simplification where the recursion is stopped at the main connective of ψ.

Intuition 4 : Since we are not restricted to clausal normal form nor local simplification needs to be restricted to the main connective, the full fledged application of simplification leads to faster proof.

It is rather easy to prove the following theorem:

Theorem 1 Local simplification (simp) satisfies Def. 1 for the propositional calculus, including completeness.

4.1 Examples and Comparison

General simplification has further gains wrt HARP or KE or similar rules such as factoring. Proof which would be optimal for the above mentioned calculi, can still be (considerably) shortened.

The difference between traditional derivation and simplification is shown in Fig. 2. The branching factor is greatly reduced. If we carry the same proof using modus ponens as in HARP or β^{c} as in KE we get the same branching structure of the simplified proof but the size of the simplified formulae is larger.

Simplification is definitely superior to modus ponens or β^{c} when there are formuale which are logically equivalent (but not identical) to the ppaernt used by MP or β^{c}-rules and, above all, when there are many occurences of the

\begin{matrix}A, B ⊃ C ⟹ A, C & \begin{matrix}A, B ⟹ B, C & A, B, C ⟹ C \\ A, B, B ⊃ C ⟹ C \end{matrix} β_{⊃} \\ A, A ⊃ B, B ⊃ C ⟹ C \end{matrix} ; β_{⊃} ; A, A ⊃ B ⟹ (B ⊃ C) ⊃ C ; α_{⊃} ; A ⟹ (A ⊃ B) ⊃ ((B ⊃ C) ⊃ C) ; α_{⊃} ; ⟹ A ⊃ ((A ⊃ B) ⊃ ((B ⊃ C) ⊃ C)) ; α_{⊃}  \begin{matrix}\begin{matrix}{A, B, C ⟹ C \atop A, B ⟹ C ⊃ C} & α_{⊃} \\ A, B ⟹ (B ⊃ C) ⊃ C \end{matrix} & simp_{t.B} \\ A ⟹ B ⊃ ((B ⊃ C) ⊃ C) \end{matrix} ; α_{⊃} ; A ⟹ (A ⊃ B) ⊃ ((B ⊃ C) ⊃ C) ; simp_{t.A} ; ⟹ A ⊃ ((A ⊃ B) ⊃ ((B ⊃ C) ⊃ C)) ; α_{⊃}

Figure 2: Classical sequents versus simplification

\begin{matrix}{A, (A ⊃ B) ∨ (A ⊃ C), D ⟹ A \atop A, (A ⊃ B) ∨ (A ⊃ C) ⟹ D ⊃ A} α_{⊃} & \begin{matrix}{A, B ⟹ B, C \atop A, A ⊃ B ⟹ B, C} MP & {A, C ⟹ B, C \atop A, A ⊃ C ⟹ B, C} MP \\ A, (A ⊃ B) ∨ (A ⊃ C) ⟹ B, C \end{matrix} ; β_{∨} ; A, (A ⊃ B) ∨ (A ⊃ C) ⟹ B ∨ C ; α_{∨} \\ A, (A ⊃ B) ∨ (A ⊃ C) ⟹ (D ⊃ A) ∧ (B ∨ C) \end{matrix} ; β_{∧} ; A ⟹ (A ⊃ B) ∨ (A ⊃ C) ⊃ (D ⊃ A) ∧ (B ∨ C) ; α_{⊃} ; ⟹ A ⊃ ((A ⊃ B) ∨ (A ⊃ C) ⊃ (D ⊃ A) ∧ (B ∨ C)) ; α_{⊃} ; \begin{matrix}\begin{matrix}{A, B ∨ C ⟹ B ∨ C \atop A ⟹ B ∨ C ⊃ B ∨ C} & α_{⊃} \\ A ⟹ ((A ⊃ B) ∨ (A ⊃ C) ⊃ (D ⊃ A) ∧ (B ∨ C)) \end{matrix} & simp_{t.A} \\ ⟹ A ⊃ ((A ⊃ B) ∨ (A ⊃ C) ⊃ (D ⊃ A) ∧ (B ∨ C)) \end{matrix} ; α_{⊃}

Figure 3: HARP modus ponens versus simplification

simplifying formula, possibly deeply nested within the main formulae of the sequent. An example is shown in Fig 3. To simplify the notation we assume the usual associativity precedence of ∧ over ∨ and of those two connectives over ⊃.

Of course one may argue that the pattern A and (A ⊃ B) ∨ (A ⊃ C) could be easily recognised but it is also easy to change it substantially; for instance as (A ⊃ B) ∨ ((A ∧ ¬B) ∨ D ⊃ C). This formula can still be proved with local simplification without any branching whereas HARP’s proof is harder than the one shown in Fig. 3. Moreover this is exactly the point of simplification: we do not want to remember a lot of particular patterns.

4.2 Subsuming other approaches

A wide variety of rules used by tableaux provers turn out to be restricted and shallow forms of local simplification. Here we consider the case for the unit of DP [13], the β^{c}-rules of KE [10],the Modus ponens and tollens of HARP [28], hyper-tableaux expansions [3].

First consider DPLL unit: “let l be a unit clause, delete every clause which contains l and delete any occurrence of \overline{l} from the remaining clauses” [12].

Suppose we have Γ, l ⟹ ∅ where Γ is set of clauses and we apply direct simplification to Γ[t.l]. By applying the boolean reductions ⊥ ∨ l_{1} ∨ … l_{n} ↦ l_{1} ∨ … ∨ l_{n} and ⊤ ∨ l_{1} ∨ … l_{n} ↦ ⊤, and finally ⊤ ∧ C_{1} ∧ … ∧ C_{n} ↦ C_{1} ∧ … ∧ C_{n} we obtain the same result of the unit rule.

Fact 1 The DPLLunit rule is an instance of the local simplification rule (simp) where S is a set of clauses labelled with t. and φ is equal to t..p or f.p.

Equally, the β^{c}-rule of KE from [10] is a generalization to signed formulae of the Modus ponenes and modus tollens of HARP [28] and the ∨−simp_{0,1} in [24]. Reversed bottom-up from their original tableau-notation they are as follows:

{S, β_{2}, \overline{β_{1}} \atop S, β, \overline{β_{1}}} β_{1}^{c}  {S, β_{1}, \overline{β_{2}} \atop S, β, \overline{β_{2}}} β_{2}^{c}

It can be easily shown, by cases, that they are extremely restricted form of local simplification. For instance consider the following instance of β_{1}^{c}:

{Γ, B ⟹ Δ, A \atop Γ, A ∨ B ⟹ Δ, A} t.A^{c}  {Γ, (A ∨ B)[f.A] ⟹ Δ, A \atop Γ, A ∨ B ⟹ Δ, A} simp_{f.A}

If we applied the full-fledge version of simplification we would have had:

(A ∨ B)[f.A] ↦ A[f.A] ∨ B[f.A] ↦ ⊥ ∨ B[f.A] ↦ B[f.A]

Thus, while KE only yields B, the full fledged use of simplifcation would have given us B[f.A]. If A occurred somewhere in B local simplification would have reduced B and, in general, shortened the proof further.

Fact 2 The β_{i}^{c} rules for KE are instances of the local simplification rule (simp), when recursion stops at the main connective of Γ and Δ formulae and it is only applied to β-formulae.

As a simpler corollary we get:

Fact 3 Modus ponens, tollens etc. of HARP and the ∨ − simp_{0,1} rules in [24] are instances of the local simplification rule (simp), when recursion stops at the main connective of Γ and Δ formulae and it is only applied to formulae of particular shape.

The next restriction that is imposed on clausal tableau proofs or model elimination techniques is regularity [3, 10, 25, 41, 39]: a literal should never appear twice on a branch. In the setting of propositional logic and clausal theorem proving (such as [3, 25]) this is equivalent to say that a clause is never selected for the extension of a branch in the tableau if the extension step (an n-ary β-rule) will yield a literal to appear twice. It is a system to constrain the search space and in particular the non-determinism in the selection of clauses for reduction.

Since we use sequents as sets, and are not restricted to clausal normal form we rephrase it in more general terms: a proof is super-regular iff all subformulae introduced by α, β rules (i.e. β_{1}, β_{2}, α_{,}α_{2}) do not occur already in the sequent S before the application of the rule.

This requirement is always satisfied (and hence made redundant) by calculi with simplification:

Fact 4 If simplification is given precedence over other rules then all propositional tableaux proofs are super-regular.

The extension step of hyper-tableaux [3] can also be subsumed:

Fact 5 Propositional hyper tableaux [3] are an instance of the sequent calculus with (simp) where Γ is a set of clauses, Δ is empty, and β-formulae are expanded only if they do not contains negated atoms.

This gives a non-clausal “hyper-tableaux” if we wave the restriction for Γ and impose simply that β do not contain negative occurrences of atoms.

Proof condensation [28] is also made redundant in most cases. The only exception is when we have two (or more) disjunctive formulae β^{a} and β^{b} on the branch and only the second (more properly β_{1}^{b} and β_{2}^{b}) is necessary for the closure of the tableaux.

4.3 Further Forms of Simplification

We can devise more powerful forms if we replace ∧ and ∨, which are commutative, associative and idempotent, with set-oriented versions ∧ ∧ and ∨ ∨. For instance (A_{1} ∨ A_{2} ∨ B_{1}) ∧ B_{2} ∧ B_{2} ∧ C ↦ ∧∧ {B_{2}, C, ∨∨ {A_{1}, A_{2}, B_{1}}}. This is already a simplification since we eliminate duplicates.

Set-oriented simplification is characterized as follows:

\begin{matrix}‡‡ \{A_{i} | i ∈ I\} [t. ‡‡ \{A_{j} | j ∈ J\}] ↦ ‡‡ \{A_{i} | i ∈ I − J\} ‡‡⊤ \\ ‡‡ \{A_{i} | i ∈ I\} [f. ‡‡ \{A_{j} | j ∈ J\}] ↦ ‡‡ \{A_{i} | i ∈ I − J\} ‡‡⊥ \end{matrix}

where ‡‡ is a set oriented connective and J ⊂ I. If I = J we can just replace the initial formula by ⊤ or ⊥ as with traditional syntactic simplification. We can also recursively simplify the remaining part.

For instance ∧ ∧{A, B, ∨∨ {C, ¬D} , ∨∨ {E, F }} simplified by t.∧ ∧ {B, ∨∨ {E, F }} yields ∧∧ {A, ∨∨ {C, ¬D}} ∧ ⊤ where ⊤ can then be eliminated.

Set containment can be verified in polynomial time and this operation can be applied a number of times at most equal to the number of subformulae of Γ and Δ.

Theorem 2 Set oriented simplification satisfies Def. 1 if ‡‡ is associative, commutative and idempotent.

This is the case for ∧ and ∨. If we want to relate this to Davis-Putnam…

Fact 6 DP-subsumption is an instance of set-oriented simplification where Γ is a set of clauses and Δ = ∅.

It seems that we have obtained every form of syntactic simplification but it is not yet the case. Consider the rule for branching in sequent or tableau:

\begin{matrix}A, Γ ⟹ Δ & B, Γ ⟹ Δ \\ A ∨ B, Γ ⟹ Δ \end{matrix} β

If we have been able to close the tableau on the left-hand side this means that we have proved that A, Γ ⟹ Δ or, in equivalent form Γ ⟹ Δ, ¬A. However, as we have already noted beforehand B, Γ ⟹ Δ means that all models that satisfy this sequent must be such that B and Γ are true. If they are true, then A ought to be false.

However we do not add A as a lemma on the right hand side. This would violate Def. 1: the resulting sequent is, in general, larger and therefore potentially increases the search space. Using full fledged lemmas may yield to some slow down, as it is shown by the comparison between KE and leanTAP in [30]. Where the application of lemmas is restricted to unit clauses as in [25] the performance is always improved.

The solution here is to introduce Tree Simplification which replaces the previous branching rule

\begin{aligned}S, β_{1} & S[\overline{β_{1}}], β_{2}[\overline{β_{1}}] \\ & S, β \end{aligned} T ree − β

The idea is very close to unit lemmas [25], and the split rule of DPLL or the principle of bivalence employed by KE. Indeed we can represent this technique as a derived rule in presence of (cut) and (thin):

\begin{aligned}S, β_{1} & \begin{matrix}{S, β_{1} \atop S, β_{2}, β_{1}} thin & \begin{matrix}{S[\overline{β_{1}}], β_{2}[\overline{β_{1}}] \atop S[\overline{β_{1}}], β_{2}[\overline{β_{1}}], \overline{β_{1}}} & thin \\ S, β_{2}, \overline{β_{1}} \end{matrix} ; simp\overline{β_{1}} \\ S, β_{2} \end{matrix} ; cut \\ & S, β \end{aligned} ; β

The last thinning step at the right-hand branches hinder completeness so we can only state a weaker property for tree simplification:

Theorem 3 Tree simplification satisfies Def. 1 except for completeness. Completeness is satisfied if β_{1} is a atom (literal for non signed version).

The reason for the successes of the split-rule of DPLL or the folding operation with unit lemmata [25] is indeed their combination with (hidden) unit simplification: we add a unit literal (the negation of the left-hand side) and afterwards we proceed with unit simplification. The size of the right subtree is never larger.

Tree simplification “compiles” these ideas into a direct and uniform rule without a restriction to unit lemmas:

Fact 7 The DPLL procedure is an instance of a sequent calculus with local and tree simplification (restricted to literals) where Γ is a set of clauses and Δ is empty.

It has been sometimes argued that the use of the name TABLEAU in [9] was somehow misleading since it was an efficient implementation of DPLL. In the light of the results of this paper the choice of the name was indeed correct.

{S, ν_{0} \atop S, ν} ν {S^{∗}, π_{0} \atop S, π} π

Figure 4: Modal Sequent Rules

Logic Composition of S^{∗} ν − rule
K {ν_{0} | ν ∈ S} NO
K4  {ν_{0}, ν | ν ∈ S} NO
K45 {ν_{0}, ν, π | ν, π ∈ S} NO

Logic Composition of S^{∗} ν − rule
T  {ν_{0} | ν ∈ S}  YES
S4  {ν | ν ∈ S}  YES
S5  {ν, π | ν, π ∈ S} YES

Table 2: Conditions for different modal logics

5 Modal Logics from K to S5

A wide range of tableau and sequent calculi have been proposed for modal logics and surveys can be found in [15, 20].

For sake of simplicity, we stick to the Gentzen-like formulation here without adding extra-logical symbols, although these techniques can be easily adapted to prefixed systems such as those of [15, 26, 5].

The corresponding sequent rule are shown in Fig. 4 where different logics can be obtained by changing the operation S^{∗}. Table 2 lists the major modal logics of knowledge and belief^{5} [21] and other logics can be found in [15, 20]. To obtain deontic versions of those logics one simply need to waive the requirement to have a π-formula (and the corresponding π_{0}) in the π-rule.

Notice that we do not need to change our general framework nor to impose clausal normal form, as done in KSAT [17] to apply propositional DPLL, and that we inherit all propositional rules including simplification. The only things we need to specify is how A[φ] will behave in presence of □ and ◇.

The simplest way is to consider □B or ◇B as atoms (“modal atoms”) and apply boolean simplification. This is already sufficient for a speed-up [18, 24].

Fact 8 Basic KSAT is an instance of the modal sequent calculus for logic K with propositional simplification, Γ contains only formulae in modal-CNF with only the □ operator and Δ is empty.

This restriction is such that KSAT may not even simplify directly □p ∧ ◇¬p without reduction to normal form.

To enhance simplification we look inside modal atoms. The uniform notation we are using provides us with extremely elegant rules. In the sequel we skip boolean rules as they remain unchanged. Moreover the only cases for simplification of A[φ] are those where the simplifying formula is a modal formula i.e. where φ is either a ν formula or a π-formula.

5We recall that, with this sequent calculus á la Fitch, cut is not eliminable for strong completeness of the logic S5, although we may use an analytic cut whose application is heavily restricted [20]. One has to resort to prefixed systems to avoid it.

Modal-K simplification is the simplest:

A[ν] ↦ \{ \begin{matrix}□(B[ν_{0}]) & if A = □B \\ ◇(B[ν_{0}]) & if A = ◇B \\ … & as for propositional logic \end{matrix}

The idea is that if we want to simplify □A with [t.□C] (a ν-formula) then we can exploit the properties of the modal operators and transform this operation in the simplifcation of A with [t.C] (the corresponding ν_{0}-formula). See again §3 and Table 1 for the ν-formulae.

Intuition 5 In a nutshell, while propositional connectives leave the simplifying formula unchanged in the recursive steps (see §4 and reduction (2)), the semantics of the modal operators is such that we must do the recursion on the subformulae of both the simplied and the simplifying formula.

For instance suppose we have ◇(□p ⊃ □(p ⊃ r)∨◇¬r) and want to simplify it with the ν-formula t.□□p. Then we get the following computation:

(◇(□p ⊃ □(p ⊃ r) ∨ ◇¬r))[t.□□p]
↦_{K} ◇((□p ⊃ □(p ⊃ r) ∨ ◇¬r)[t.□p])
↦_{bool} ◇((□p)[t.□p] ⊃ (□(p ⊃ r))[t.□p] ∨ (◇¬r)[t.□p])
↦_{K} ◇(⊤ ⊃ □((p ⊃ r)[t.p] ∨ ◇(¬r[t.p])
↦_{bool} ◇(□r ∨ ◇¬r)

Modal-K4 simplification exploits directly the properties of transitivity (represented by the axiom □φ ⊃ □□φ):

A[ν] ↦ \{ \begin{matrix}□(B[ν][ν_{0}]) & if A = □B \\ ◇(B[ν][ν_{0}]) & if A = ◇B \\ … & as for propositional logic \end{matrix}

This means that for any logic containing the transitivity axiom we can first simplify B with ν and then simplify the result with ν_{0}. The presence of the transitivity adds a further level of simplification with respect to simple modal logic K.

Notice that the recursive call to simplification always terminates since there is a decrease in the nesting of modal operators of the simplified formula. For instance one may try the previous example with t.□p as the simplifying formula.

Modal-K5 simplification is the following

A[ν] ↦ □(B[ν_{0}]) if A = □B
A[ν] ↦ ◇(B[ν_{0}]) if A = ◇B
A[π] ↦ □(B[π]) if A = □B
A[π] ↦ ◇(B[π]) if A = ◇B

The rule can be understood by considering the corresponding axiom, ◇A ⊃ □◇A: it tells that possibility-like formulae can propagate inside modalities.

When we combine properties we can also combine simplifications. For instance K45:

A[φ] ↦ \{ \begin{matrix}□(B[ν][ν_{0}]) & if A = □B and φ = ν \\ ◇(B[ν][ν_{0}]) & if A = ◇B and φ = ν \\ □(B[π]) & if A = □B and φ = π \\ ◇(B[π]) & if A = ◇B and φ = π \\ … & as for propositional logic \end{matrix}

Theorem 4 L-Modal simplification (either direct or tree like) satisfies Def. 1 for modal logic L where L is one of K,T, K4,S4,K45,S5 and their deontic variants.

6 Renaming and First Order Logic

For sake of simplicity we assume that formulae have been already skolemised. So that we will not have to deal with existential-like (δ) formulae on-line.

If this is not the case, on-line reduction of existential formulae can be done in a number of ways: from the ground version of Smullyan [35] to the free variable one [31, 16]. A comprehensive study of different rules for δ-formulae can be found in [2] where their impact on the proof size has also been analyzed. Since this issue is orthogonal to the one pursued here we refer to the above works.

6.1 Ground Sequents and first order DPLL

The simplest way to lift the propositional framework (§4) to first order logic is to use the ground version of the sequent calculus as in [35]. We simply require a new rule:

{S, γ_{0}(t) \atop S, γ} where t is a ground term

This unifying calculus answers an interesting question: why first order DPLL is rather inefficient in comparison with its propositional version?

Fact 9 The first oder DPLL procedure is a sequent calculus with propositional simplification, off-line skolemisation and the ground γ-rule.

Unfortunately, using γ-rule á la Smullyan rather than those with unification in [7, 31, 16] leads to a non-elementary slow down [2]. Even a propositional exponential speed-up cannot compensate it (especially if there is little propositional reasoning).

6.2 Free Variables Sequents with Renaming

As we already mentioned, the presence of free variables makes the extension of simplification non trivial, especially if we want to use the (more efficient) free variables version of the sequent calculus.

S, f.⊤ : R (⊤)  S, t.⊥ : R (⊥)  S, φ, \overline{φ} : R (Ax)

{S, α_{1}, α_{2} : R \atop S, α : R} (α)  {S, γ_{0}(x) : R \atop S, γ : R} (γ)  \begin{matrix}S, β_{1} : R_{D} & S, β_{2} : R_{D} \\ S, β : R \end{matrix} (β)

{S, ψ[φ|R], φ : R \atop S, ψ, φ : R} (simp) {S, φη_{/R} : R \atop S, φ : R} (ren)

Where R_{D} ⊇ R ∪ (F V (β_{1}) ∩ F V (β_{2})), x is a new variable for S in the

γ-rule,i.e. x ∉ F V (S), and η_{/R} is a renaming.

Figure 5: First order calculus with Simplification and Renaming

A comparison with resolution may therefore help in clarifying the major intuition. When we apply clause subsumption [32, 40] we implicitly assume that all variables are universally quantified, therefore we must find a substitution that binds only the (universal) variables of the subsuming clause so that it is contained in the subsumed clause.

To apply this analogy, we need to identify the (implicitly quantified) universal variables in a sequent (or at least some of them since the general problem is undecidable).

This need leads to a redefinition of the free variables sequent calculus [31, 16]: we take the idea of universal variables [4, 6] and use the dual notion of rigid variables. Thus our sequents will be triples in the unsigned notation Γ ⟹^{R} Δ and pairs in the signed one S : R, where R ⊆ F V (S) is the set of rigid variables in S. The intuition is that all other variables in S can be implicitly assumed to be universally quantified.

The global calculus is shown in Fig.5: simplification is now conditional wrt the set of rigid variables R and there is a new rule (ren) for renaming non rigid and hence universal variables. For the notation see again §3: we recall that η_{/R} is a substitution which renames with fresh variables some variables not in R.

Remark 1 It is important to notice that the renaming η_{/R} is local to the formula φ: it is not applied to the whole sequent S nor, a fortiori, to the whole proof tree.

The definition of the proof search tree T and the frontier of the tree S_{1} : R_{1} | … | S_{n} : R_{n} (S_{i} : R_{i} are the leaves of T ) are unchanged w.r.t. propositional logic (§4). The notion of proof needs a slight repharsing.

Definition 2 A pair ⟨T , σ_{T} ⟩, where T is a search tree and σ_{T} a substitution, is a proof for the sequent S iff

• S : ∅ labels the root of the tree T ;

• F V (S) = ∅, i.e. S constains only sentences; • for each S_{i} : R_{i} in the frontier of T , S_{i}σ_{T} is an axiom^{6};

• For each S_{i} : R_{i} and S_{j} : R_{j} in the frontier of T , we have F V (S_{i}) ∩ F V (S_{j}) ⊆ R_{i} ∩ R_{j};

We refer to σ_{T} as a closing substitution for T . Notice that we can always obtain a proof tree satisfying the last condition by a suitable application of renaming for each leaf. In this way we can apply the substitution σ_{T} also to the whole tableau and obtain still a result close to a standard proof search tree of the ground version. If we choose to represent only the frontier of the tree, as done in [7, 14], we could have used also the sequent elimination rule (abc). The only substitution which is applied globally is σ_{T}.

The next step is the upgrade of the operation of simplification A[φ|R]. We only need to change the basic step here:

A[φ|R] ↦ \{ \begin{matrix}⊤ & if φσ = t.A \\ ⊥ & elseif φσ = f.A \\ ∀x.(B[φ|R]) & elseif A = ∀x.B \\ & as for propositional logic \end{matrix}  (3)

The substitution σ can be any substitution of the form ρ_{/R∪F V (A)}, that is it must not binf variables in A nor rogid variables in R. Notice that σ is not applied to the tableau nor the simplified formula. This is in common to many techniques used by clausal tableaux such as [3, 25].

In this case we define A = B as syntactic equivalence up to the obvious renaming of bound variables. For instance we have ∀x∀yp(x, y) = ∀z∀w.p(z, w) while ∀y.p(x, y) ≠ ∀w.p(z, w).

Further extensions, as in §4, are also possible with set-oriented connectives.

6.3 Examples and Properties

Two examples of derivation are shown in Fig. 6,7 without using simplification but only renaming (irrelevant formulae have been omitted for readability). The second example cannot be simulated by leanTAP with universal variables [7] which requires more β and γ rules.

Indeed this calculus subsumes leanTAP with universal variables:

Fact 10 leanTAP with universal variables is an instance of the calculus with renaming but without simplification where (i) in the β rule R_{D} ≐ R∪F V (β_{1})∪ F V (β_{2}) and (ii) renaming is applied to all literals in S before any β-rule.

This general technique also subsumes the use of conjunctive super-formulae used in [14]. A comparison with the first order hyper-tableaux expansion step in [3] is also interesting: the idea of a purifying (grounding) substitution corresponds, in this framework, to say that all variables from ⋃_{i} R_{i} must be grounded by σ, where R_{i} are those created by branching rules where β has only positive literals.

6If the formulae φ and \overline{φ′} of the axioms are non-atomic then σ_{T} must also be free for φ and φ′.

\begin{matrix}{p(y) ⟹^{\{\}} p(a) \atop p(x) ⟹^{\{\}} p(a)} ren_{p(x)} & {p(z) ⟹^{\{\}} p(b) \atop p(x) ⟹^{\{\}} p(b)} ren_{p(x)} \\ ∀x.p(x), p(x) ⟹^{\{\}} p(a) ∧ p(b) \end{matrix} ; β_{∧} ; ∀x.p(x) ⟹^{\{\}} p(a) ∧ p(b) ; γ

The closing substitution is σ_{T} = {a/y, b/z}

Figure 6: A Simple Derivation with Renaming

\begin{matrix}p(x) ⟹^{\{x\}} p(a) & \begin{matrix}r(y) ⟹^{\{x,y\}} r(b), s(b) & s(y) ⟹^{\{x,y\}} r(b), s(b) \\ q(x), r(y) ∨ s(y) ⟹^{\{x\}} p(a), r(b), s(b) \end{matrix} β_{∨} \\ p(x) ∨ q(x), r(y) ∨ s(y) ⟹^{\{\}} p(a), r(b), s(b) \end{matrix} ; β_{∨} ; p(x) ∨ q(x), r(x) ∨ s(x) ⟹^{\{\}} p(a), r(b), s(b) ; ren_{r(x)∨s(x)} ; (p(x) ∨ q(x)) ∧ (r(x) ∨ s(x)) ⟹^{\{\}} p(a), r(b), s(b) ; α_{∧} ; ∀x.(p(x) ∨ q(x)) ∧ (r(x) ∨ s(x)) ⟹^{\{\}} p(a), r(b), s(b) ; γ

The closing substitution is σ_{T} = {a/x, b/y}

Figure 7: Another Derivation with Renaming

What is more significant is the level of simplification in the proof search which is performed by first-order simplification. An example is shown in Fig. 8 where an effect similar to hyper-resolution with subsumption is obtained. A proof of the same formula in the calculus without renaming requires more branchings and applications of the γ-rule.

Some care must be taken to avoid excessive simplification of γ formulae to keep completeness. Indeed if we reduce γ to γ_{0}(x) and then simplify γ[γ_{0}(x)] this reduces to ⊤ and we have lost the possibility of generating fresh instances from γ.

This problem is not present if we “copy” a formula before renaming it,i.e. we assume to have, in the antecedent of rule (ren), S, φ = S ∪ {φ} = S ∪ {φ, φ} = S ∪ {φ}, φ and then apply renaming. With this solution the γ rule may become a destructive rule (i.e. gamma is deleted after reduction). In a nutshell we are shifting the application of contraction from γ formulae to renamed ones.

This idea leads to a more effective calculus, since the particular form of the β-rule makes it possible to maintain (some) universal variables also after a branching. Thus renaming requires less application of contraction than γ formulae. An example is shown in Fig. 9, also this example cannot be simulated by universal variables as defined in [7].

It is possible to further optimize this calculus if we assume a depth first search for closing substitutions selecting the branch one by one and then even-

\begin{matrix}{p(x), r(z, y) ⟹^{\{\}} ⊤ \atop p(x), r(z, y) ⟹^{\{\}} r(a, b) ∧ r(c, d)} & simp_{r(z,y)} \\ p(x), ∀y∀z.r(z, y) ⟹^{\{\}} r(a, b) ∧ r(c, d) \end{matrix} ; γ ; p(x), ∀y∀z.p(y) ⊃ r(z, y) ⟹^{\{\}} r(b, c) ∧ r(d, e) ; simp_{p(x)|} ; ∀x.p(x), ∀y∀z.p(y) ⊃ r(z, y) ⟹^{\{\}} r(a, b) ∧ r(c, d) ; γ

Figure 8: A Proof with first order simplification

\begin{matrix}p(a) ⟹^{\{x\}} p(x), q(b, a) ∧ q(c, a) & \begin{matrix}{q(z, x) ⟹^{\{x\}} q(b, a) \atop q(y, x) ⟹^{\{x\}} q(b, a)} ren & {q(w, x) ⟹^{\{x\}} q(c, a) \atop q(y, x) ⟹^{\{x\}} q(c, a)} ren \\ q(y, x), p(a) ⟹^{\{x\}} q(b, a) ∧ q(c, a) \end{matrix} ; β_{∧} \\ p(x) ⊃ q(y, x), p(a) ⟹^{\{\}} q(b, a) ∧ q(c, a) \end{matrix} ; β_{⊃} ; ∀x∀y.p(x) ⊃ q(y, x), p(a) ⟹^{\{\}} q(b, a) ∧ q(c, a) ; γ ; ∀x∀y.p(x) ⊃ q(y, x) ⟹^{\{\}} p(a) ⊃ q(b, a) ∧ q(c, a) ; α_{⊃}

Closing substitution is σ_{T} = {a/x, b/z, c/w}.

Figure 9: Renaming below a branching point

tually backtracking in case of failure. This is the techniques used by leanTAP, see e.g. [7]. In this case a further improvement is obtained by revising the β rule and putting S, β_{2} : R (rather than R_{D}) on the right branch, applying to it the closing substitution of the left branch and then proceeding in the search.

6.4 Proving Soundness and Completeness

The completeness of the calculus is derived directly by the completeness of free variables sequents and tableaux calculi [16], since we have more rules.

Soundness is the tricky part. To this extent we cannot use the standard techniques, with a rigid assignment to all variables in a proof tree: renaming and the β-rule would then be unsound. For the soundness proof to carry forward we must associate the frontier of a proof tree to a first order formula as follows:

fml(S_{1} : R_{1} | … | S_{n} : R_{n}) = fml(S_{1} : R_{1}) ∨ … ∨ fml(S_{n} : R_{n}) (4)
fml(S : R) = ∀x_{1} … x_{n}. ⋀_{i} A_{i} ∧ ⋀_{j} ¬B_{j}  (5)
where x_{k} ∈ F V (S) − R
and t.A_{i} ∈ S and f.B_{j} ∈ S

Then the key point of the proof is to prove that, given the frontier of a proof tree S_{1} : R_{1} | … | S_{n} : R_{n} and the new frontier due to some rule application S′_{1} : R′_{1} | … | S′_{n′} : R′_{n′}, for all interpretation I and all assignment A if I, A ⊧ fml(S_{1} : R_{1} | … S_{n} : R_{n}) then for all assignment A′ extending A it is I, A′ ⊧ fml(S′_{1} : R′_{1} | … S′_{n′} : R′_{n′}).

The case for the renaming rule is then trivial and the case for β-rule stems from the observation that ∀x.(A ∨ B) is logically equivalent to (∀x.A) ∨ B if x ∉ F V (B).

In this way we can prove that is the root is satisfiable the frontier would also be satisfiable and of course the frontier of a closed tableau cannot be satisfiable.

7 Experimental Analysis

We performed some experiments on random 3-SAT instances and the IFIP benchmarks with a tableaux prover (Beatrix^{7}) implemented in sicstus prolog.

Beatrix has been designed in the spirit of lean tableaux theorem proving [7] modified only for using set oriented connectives and the trivial heuristic of reducing small formulae before large ones^{8}. A simple implementation is sufficient for interesting conclusions wrt the relative gains of local and tree simplification. Formula are reduced off-line in negation normal form (and skolemised) in the same fashion of leanTAP.

7.1 Random 3-CNF

Table 3 shows the result for the standard random distribution of 3-SAT^{9}: 3 − sat(V, C) means that samples had C clauses, with 3 literals selected uniformly among V variables and each literal negated with probability 0.5.

A number of experimental studies [9, 17] have shown that DPLL (and indeed most complete satisfiability checking procedures) exibits an easy-hard-easy computation pattern as the ratio between the number of clauses and variables increases, with the hardest formulae around C/V = 4.2 − 4.3. This phenoment has been sometimes attributed to the “semantical” branching described by the splitting rule of DPLL. On the contrary we have found out the following:

Fact 11 For random 3-CNF local simplification produces already the easy-hard-easy pattern. Only in the transition region tree simplification (the analogous of DPLL split) performs better.

7.2 IFIP benchmarks for Hardware verification

Beside CNF benchmark we have tested our implementation on the IFIP benchmarks for hardware verification [8]. These benchmarks are hard for (clausal)

7In the 13th century masterpiece Divina Commedia by Dante Alighieri, Beatrix is the angel who oversees the poet from hell to heaven.

8We use neither cut nor thinning except for the particular combination described as tree simplification in §4.3.

9After C = 10 × V a linear relation between C and running time is due to inefficient list management by prolog.

Table 3: Benchmark on Random 3-SAT

Problem  Local Tree  Problem  Local Tree
3-sat(32,96)  .3  .2  3-sat(64,192)  1.4 1.0
3-sat(32,128)  3.9 1.2  3-sat(64,256)  334.6 38.4
3-sat(32,136)  6.1 1.8  3-sat(64,272)  554.3 56.4
3-sat(32,144)  6.9 2.1  3-sat(64,288) 1,050.9 72.0
3-sat(32,160)  8.2 2.4  3-sat(64,320)  568.6 60.0
3-sat(32,192)  7.7 2.6  3-sat(64,384)  240.3 39.4
3-sat(32,224)  6.0 2.2  3-sat(64,448)  139.3 30.6
3-sat(32,256)  5.3 2.3  3-sat(64,512)  74.3 23.5
3-sat(32,288)  4.9 2.3  3-sat(64,576)  69.6 21.8
3-sat(32,320)  4.8 2.4  3-sat(64,640)  59.6 20.4
3-sat(32,640)  5.9 3.7  3-sat(64,1280)  38.2 19.8
3-sat(32,1280) 10.5 6.5  3-sat(64,2560)  52.3 24.9

car_{1} ≡ (a_{1} ∧ b_{1}),
som_{1}(1) ≡ (a_{1} ⊕ b_{1}),
som_{2}(1) ≡ (a_{2} ⊕ b_{2} ⊕ car_{1}),
cout(1) ≡ (((a_{2} ∨ b_{2}) ∧ car_{1}) ∨ (a_{2} ∧ b_{2})),
cout_{1} ≡ (b_{1} ∧ a_{1})),
som_{1}(2) ≡ ¬((¬a_{1} ∧ ¬b_{1}) ∨ (a_{1} ∧ b_{1})),

som_{2}(2) ≡ ¬((((¬a_{2} ∧ ¬b_{2}) ∨ (a_{2} ∧ b_{2})) ∧ ¬cout_{1}) ∨ (cout_{1} ∧ ¬((¬a_{2} ∧ ¬b_{2}) ∨ (a_{2} ∧ b_{2})))),

cout(2) ≡ ((a_{2} ∧ cout_{1}) ∨ (b_{2} ∧ cout_{1}) ∨ (a_{2} ∧ b_{2}))

⟹ (som_{1}(1) ≡ som_{1}(2)) ∧ (som_{2}(1) ≡ som_{2}(2)) ∧ (cout(1) ≡ cout(2))

Figure 10: A two bits ripple adder rip02.be

tableaux methods [38] and are typically formulated in non clausal form, with an extensive use of equivalences (≡) and exclusive or (⊕). The typical problem is to show that a two circuit descriptions are equivalent (i.e. a specification matches an implementation). One of the easiest formula is shown in Fig. 10.

In practice all have been solved except large multipliers, known to be hard also for BDDs, timed out after 10 minutes (for a comparison between DPLL and OBDDs see [38]). Satisfiable formulae (marked by *) are solved within few milliseconds. What is more interesting here is the comparison with a standard interactive prover such as Isabelle [29]. This is shown in Table 4, where fast tac is the standard automatic tactic used in Isabelle, and ifip tac applies fast tac after a preprocessing step which exploit the format of the benchmark.

The scaling factor for problems such as rip0x.be is more interesting than the absolute values. Absolute values simply tell us about the relative efficiency of lean proving in prolog vs big provers in ML, somehow strengthening the argument of [7]. On the contrary the gap in the scaling factor (a factor of 1000 for Isabelle in the passage from rip0n to rip0n + 2 is matched by a factor of 10) tells that the use of simplification can substantialy increase the tractability

Table 4: Simplification versus Isabelle

Problem fast tac ifip tac  Problem Local Tree
ex2  13.1  1.3  ex2  0.0 0.0
transp  43.8  0.2  transp  0.0 0.0
risc  -  9.8  risc  0.4 0.6
counter  -  68.8  counter  0.1 0.1
hostint1  -  96.5  hostint1  0.3 0.2
mul  -  130.9  mul  0.4 0.2
rip02  2848.2  1.6  rip02  0.0 0.0
rip04  -  994.5  rip04  0.5 0.6
rip06  -  -  rip06  3.0 3.0
rip08  -  -  rip08  18.2 18.4

Table 5: Run times on IFIP Benchmarks

Problem  Local Tree
counter  0.1 0.2
d3(*)  0.1 0.1
dk27  2.2 2.3
ex2  0.0 0.0
hostint1  0.2 0.2
misg  0.7 1.0
mul  0.2 0.2
risc  0.4 0.5
transp  0.0 0.0
werner (*)  0.1 0.0

Problem  Local Tree
ztwaalf1  0.8 0.8
ztwaalf2  0.8 0.4
mjcg no (*)  0.0 0.0
mjcg yes  1.8 1.1
mp2d  3.7 1.1
rip02  0.0 0.0
rip04  0.4 0.5
rip06  2.9 2.9
rip08  18.2 18.4

threshold for tableaux calculi. Further benchmarks are shown in Table 5 and in Table 6.

For first-order logic the effect on universal variables is also documented in [7] and the use of simplification improves further the performance.

Intuition 6 : If we are mainly interested in theorem-hood, local simplification (with renaming) may be enough without cut or tree-simplification.

8 Conclusion

In this paper we have show how the introduction of a simple technique called simplification may boost the deduction capabilities of tableaux methods. It plays (mutatis mutandis) the same role of unit for DPLL and subsumption for resolution and provides an uniform framework which subsumes a number of techniques for the improvement of tableau-based methods.

It can be used for a wide range of logic ranging from proposition to modal to higher order logic.

Table 6: More IFIP Benchmarks

Problem Local Tree
add1  24.4 12.2
alu  21.3 7.1
dk17  19.8 3.0
f51m  21.4 5.7
table  13.9 2.8
vg2  12.8 7.0
x1dn  13.4 7.2
z4  2.9 2.3
z5xpl  11.5 4.1

Problem Local Tree
alupla20 784.0 618.1
dc2  149.7 12.5
sqn  297.7 11.2
z9sym 166.8 9.8
mul03  - 20.1
pitch - 5.7
rd73  - 30.4
rom2 - 2.5
root  - 33.7

Its flexibility and its simplicity make it possible its incorporation into sequent based interactive theorem provers used for hardware and software verification. Moreover there is no need of black-boxes since the computational effectiveness of DPLL and KSAT can now be compiled into standard sequentbased tactics.

Yet, there is a possible criticism we may have to face: after adding all these simplifications to sequent calculi are not we abandoning the calculus itself?

The best answer is probably a question: is resolution with subsumption no longer resolution?

Acknowledgments

I would like to acknowledge many fruitful discussions with F. Donini, L. Carlucci Aiello, F. Giunchiglia, R. Goré, J. Harrison, L. Paulson, F. Pirri and R. Sebastiani and the members of the AI group in Rome and the Automatic Reasoning group in Cambridge. A special thank to L. Paulson and the Computer Laboratory for their hospitality in Cambridge and for making this technical report possible.

References

[1] C. M. Angelo, D. Verkest, L. Claesen, and H. De Man. On the comparison of HOL and Boyer-Moore for formal hardware verification. Formal Methods in System Design, 2(1):45–72, 1993.

[2] M. Baaz and C. G. Fermüller. Non-elementary speedups between different versions of tableaux. In P. Baumgartner, R. Hähnle, and J. Possega, editors, Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, volume 918 of Lecture Notes in Artificial Intelligence, pages 217–230. Springer-Verlag, 1995.

[3] P. Baumgartner, U. Furbach, and I. Niemelä. Hyper tableaux. In J. Alferes, L. Pereira, and E. Orlowska, editors, Proceedings of the 6th European Workshop on Logics in Artificial Intelligence (JELIA-96), volume 1126 of Lecture Notes in Artificial Intelligence, pages 1–17. Springer-Verlag, 1996.

[4] B. Beckert. Semantic tableaux with equality. Journal of Logic and Computation, 7(1):38–58, 1997. To appear.

[5] B. Beckert and R. Goré. Free variable tableaux for propositional modal logics. In D. Galmiche, editor, Proceedings of the International Conference on Analytic Tableaux and Related Methods (TABLEAUX-97), Lecture Notes in Artificial Intelligence. Springer-Verlag, 1997.

[6] B. Beckert and R. Hänle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction (CADE-90), volume 607 of Lecture Notes in Artificial Intelligence, pages 507–521. Springer-Verlag, 1992.

[7] B. Beckert and J. Possega. leanTAP: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.

[8] L. J. Claesen, editor. Formal VLSI Correctness Verification: VLSI Design Methods, volume II. Elsevier Science Publishers (North-Holland), Amsterdam, 1990.

[9] J. Crawford and L. Auton. Experimental results on the crossover point in satisfiability problems. In Proceedings of the 11th National Conference on Artificial Intelligence (AAAI-93), pages 21–27. AAAI Press/The MIT Press, 1993.

[10] M. D’Agostino and M. Mondadori. The taming of the cut. Journal of Logic and Computation, 4(3):285–319, 1994.

[11] M. Davis. Eliminating the irrelevant from mechanical proofs. In N. Metropolis, A. H. Taub, J. Todd, and C. Tompkins, editors, Proceedings of the 15th Symposium in Applied Mathematics, pages 15–30. American Mathematical Society, 1963.

[12] M. Davis, G. Longemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962.

[13] M. Davis and H. Putnam. A computing procedure for quantificational theory. Journal of the ACM, 7(3):201–215, 1960.

[14] A. Degtyarev and A. Voronkov. Equality elimination for the tableau method. In J. Calmet and C. Limongelli, editors, Proceedings of the International Symposium on the Design and Implementation of Symbolic Computation Systems (DISCO-96), volume 1128 of Lecture Notes in Computer Science, pages 46–60. Springer-Verlag, 1996.

[15] M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983.

[16] M. Fitting. First Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.

[17] F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures - the case study of modal k. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction (CADE-96), volume 1104 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1996.

[18] F. Giunchiglia and R. Sebastiani. A SAT-based decsion procedures for ALC. In Proceedings of the 5th International Conference on the Principles of Knowledge Representation and Reasoning (KR-96), 1996.

[19] M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, 1993.

[20] R. Goré. Tableaux method for modal and temporal logics. Technical Report TR-ARP-15-5, Australian National University, 1995. To appear as chapter on the ”Handbook of Tableau Methods”.

[21] J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence Journal, 54:319–379, 1992.

[22] J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162–170, 1995.

[23] J. Harrison. Stalmarck’s algorithm as a HOL derived rule. In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’96), volume 1125 of Lecture Notes in Computer Science, pages 221–234. Springer-Verlag, 1996.

[24] U. Hustadt and R. A. Schmidt. On evaluating decision procedure for modal logic. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), 1997. To appear.

[25] R. Letz, K. Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13(3):297– 337, 1994.

[26] F. Massacci. Strongly analytic tableaux for normal modal logics. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction (CADE-94), volume 814 of Lecture Notes in Artificial Intelligence, pages 723–737. Springer-Verlag, 1994.

[27] N. V. Murray and E. Rosenthal. On the computational intractability of analytic tableau methods. Bulletin of the Interest Group in Pure and Applied Logic, 2(2):205–228, 1994.

[28] F. Oppacher and E. Suen. HARP: a tableau-based theorem prover. Journal of Automated Reasoning, 4:69–100, 1988.

[29] L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[30] J. Pitt and J. Cunningham. Theorem proving and model building with the calculus KE. Bulletin of the Interest Group in Pure and Applied Logic, 4(3):129–150, 1996.

[31] D. Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960.

[32] J. A. Robinson. A machine oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.

[33] J. Rushby. Automated deduction and formal methods. In R. Alur and T. A. Henzinger, editors, Proceedings of the International Conference on Computer-Aided Verification (CAV-96), volume 1102 of Lecture Notes in Computer Science, pages 169–183. Springer-Verlag, 1996.

[34] B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92), 1992.

[35] R. M. Smullyan. First Order Logic. Springer-Verlag, 1968. Republished by Dover, New York, in 1995.

[36] R. M. Smullyan. Uniform gentzen systems. Journal of Symbolic Logic, 33(4):549–559, 1968.

[37] M. Szabo, editor. The collected papers of G. Gentzen. North-Holland Publ. Co., Amsterdam, Amsterdam, 1969.

[38] T. Uribe and M. E. Stickel. Ordered binary decision diagrams and the davis-putnam procedure. In J. P. Jouannaud, editor, Proocedings of the 1st International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[39] A. Urquhart. The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1(4):425–467, Dec 1995.

[40] A. Voronkov. The anatomy of vampire (implementing bottom-up procedures with code trees). Journal of Automated Reasoning, 15(2):237–265, 1995.

[41] K. Wallace and G. Wrightson. Regressive merging in model elimination tableau-based theorem provers. Bulletin of the Interest Group in Pure and Applied Logic, 3(6):921–937, 1995.

[42] H. Zhang and M. E. Stickel. An efficient algorithm for unit-propagation. In Proc. of the 4th International Symposium on Artificial Intelligence and Mathematics, 1996.