Introduction

In recent years, we have introduced new tableau calculi and logical optimization rules for propositional Intuitionistic Logic [4] and propositional Gödel-Dummett Logic [7]. As an application of these results, we have implemented theorem provers for these logics [3,7] which outperform their competitors. The above quoted calculi and optimizations are the result of a deep analysis of the Kripke semantics of the logic at hand. In this paper, we apply such a semantical analysis to PLTL. In particular, we present a refutation tableau calculus and some logical optimizations for PLTL and we briefly discuss a prototype Prolog implementation of the resulting proof-search procedure.

As for related work, our tableau calculus lies in the line of the one-pass calculi based on sequents and tableaux calculi [14,2,10], whose features are suitable for automated deduction. We also cite as related the approaches based on sequent calculi discussed in [12,13] and the natural deduction based proof-search techniques discussed in [1]. The results in [8,15] are based on resolution, thus they are related less to our approach.

Tableau calculus and replacement rules

We consider the language based on a denumerable set of propositional variables V, the logical constants (true), ⊥ (false), ¬ and ∨ and the modal operators • (next) and U (until). We define A as ¬( U¬A). Given a set of formulas S, we denote with

•S the set {•A | A ∈ S}.

PLTL is semantically characterized by rooted linearly ordered Kripke models; formally, a PLTL-model is a structure K = P, ≤, ρ, V where P is the set of

(AUB) + = A ( ¬(AUB) ) + = ¬B (AUB) − = B ( ¬(AUB) ) − = ¬A, ¬B Hi = {•U1, U + 1 , . . . , •Ui−1, U + i−1 } ∪ {U − i } ∪ {Ui+1, . . . , Um} (i = 1, . . . , m)

Fig. 1. The tableau calculus for PLTL worlds, ≤ is a linear well-order with minimum ρ and no maximum element, V is a function associating with every world α ∈ P the set of propositional variables satisfied in α. Given α ∈ P , the immediate successor of α, denoted by α , is the minimum of the <-successors of α. The satisfiability of a formula A in a world α of K, written K, α A (or simply α A), is defined as follows:

-

for p ∈ V, α p iff p ∈ V (α); α ; α ⊥; -α ¬A iff α A; α A ∨ B iff α A or α B; -α •A iff α A; -α AUB iff ∃β ≥ α : β B and ∀γ : α ≤ γ < β, γ A.

The following properties can be easily proved. The latter one follows by the fact that ≤ is a well-order, hence, if B is satisfiable in some γ ≥ α, there exists the minimum γ * ≥ α satisfying B.

-α A iff ∀β ≥ α, β A; -α AUB iff (∀γ ≥ α, γ B) or (∃β ≥ α : β A and ∀γ : α ≤ γ ≤ β, γ B). A set of formulas S is satisfiable in α (K, α S) if every formula of S is satisfiable in α; S is satisfiable if it is

satisfiable in some world of a PLTL-model. The rules of the tableau calculus T for PLTL are given in Fig. 1. The peculiar rule of T is the rule Lin inspired by the multiple-conclusion rule for Gödel-Dummett Logic DUM presented in [6,7]. DUM is semantically characterized by intuitionistic linearly ordered Kripke models; the multi-conclusion rule for DUM simultaneously treats a set of implicative formulas while Lin simultaneously treats a set of modal formulas. We remark, that the number of conclusions of rule Lin depends on the number of formulas in B; if B is empty, Lin has A as only conclusion.

The rules of T are sound is the sense that, if the premise of a rule is satisfiable then one of its conclusions is satisfiable. We briefly discuss, by means

S, A S[ /A], A R- S, ¬A S[⊥/A], ¬A R-¬ S, A S{ /A}, A R-cl S, ¬A S{⊥/A}, ¬A R-cl¬ S S[ /p] + if p + S S S[⊥/p] − if p − S

For for l ∈ {+, −}, p l S iff p l H for every H ∈ S where, p l H is defined as follows:

p + p and p − ¬p and p l H, if H ∈ (V \ {p}) ∪ { , ⊥}; p l (A ∨ B) iff p l A and p l B; p l (AUB) iff p l A and p does not occur in B; p l ¬(AUB) iff p l B and p does not occur in A;

-if A = BUC, then p + ¬A iff p − A and p − ¬A iff p + A; -p l • A iff p l A;

Fig. 2. Optimization rules for PLTL of an example, the soundness of rule Lin. The application of rule Lin to

•B = {•(A 1 UB 1 ), •¬(A 2 UB 2 )

} generates as conclusions the sets:

C = {A1, ¬B2} ∪ •B , H1 = {B1, ¬(A2UB2)} , H2 = {•(A1UB1), A1, ¬A2, ¬B2}.

Let us assume that α •B; we show that at least one of the conclusions is satisfiable. We have α A 1 UB 1 and α ¬(A 2 UB 2 ). Note that:

-α A 1 UB 1 ⇒ ∃β 1 ≥ α : β 1 B 1 and ∀γ : α ≤ γ < β 1 , γ A 1 . -α ¬(A 2 UB 2 ) ⇒ (i) ∀γ ≥ α , γ B 2 or (ii) ∃β 2 ≥ α : β 2 A 2 and ∀γ : α ≤ γ ≤ β 2 , γ B 2

If (i) holds either α < β 1 and α C, or α = β 1 and α H 1 . Now, let us suppose that (ii) holds; then:

-if α < β 1 and α < β 2 , then α C; -if α = β 1 , then α H 1 ; -if α < β 1 and α = β 2 , then α H 2 .

The notions of proof- Although multi-conclusion rules as Lin can generate a huge number of branches, as discussed in [7], theorem provers using these kind of rules can be effective.

To improve the performances of the above procedure we exploit the optimization rules depicted in Fig. 2 which are inspired by the rules presented in [11,4]. In rules R-and R-¬ (R stands for Replacement), S[B/A] denotes formula substitution, that is the set of formulas obtained by replacing every occurrence of A in S with B. In rules R-cl and R-cl¬, S{B/A} denotes partial formula substitution, that is the set of formulas obtained by replacing every occurrence of A in S which is not under the scope of a modal connective with B. As for rules + and − , they can be applied if the propositional variable p has constant polarity in S (p l S). We remark that rules + and − are the PLTL version of the rules T-permanence and T¬-permanence of [4].

All the rules of Fig. 2 have the property that the premise is satisfiable iff the conclusion is. In the proof search procedure we apply the optimization rules and the usual boolean simplification rules [11,4] at every step of a saturation phase.

Implementations and performances

To perform some experiments on the benchmark formulas for PLTL, we have implemented β, a theorem prover written in Prolog4 . At present β is a very simple prototype that implements T and the rules in Fig. 2. On the third column of the table in Fig. 4 we report the performances of β. For every family of formulas in the benchmark we indicate the number of formulas of the family solved within one minute. All tests were conducted on a machine with a 2.7GHz Intel Core i7 CPU with 8GB memory. All the optimizations rules we have described are effective in speeding-up the deduction. Indeed, without the described optimizations, timings of β are some order of magnitude greater and almost no formula is decided within one minute. In the fourth column of Fig. 4 we report the figures related to PLTL, an OCaml prover based on the one-pass tableau calculus of [14]. Although in general PLTL outperforms β, there are families where our prototype is more efficient than PLTL and this is encouraging for further research.

To conclude, we have presented our ongoing research on automated deduction for PLTL. In this note we have discussed a new proof-theoretical characterization of PLTL based on a multiple-conclusion rule and some optimization rules useful to cut the size of the proofs. As regards the future work, we aim to apply to the case of PLTL other optimizations introduced in the context of Intuitionistic logic as the permanence rules of [4] and the optimizations exploiting the notions of local formula [3] and evaluation [5].