We present an ongoing work on a proof-search procedure for Propositional Linear Temporal Logic (PLTL) based on a one-pass tableau calculus with a multiple-conclusion rule. The procedure exploits logical optimization rules to reduce the proof-search space. We also discuss the performances of a Prolog prototype of our procedure.
Introduction
In recent years, we have introduced new tableau calculi and logical optimization
rules for propositional Intuitionistic Logic [
As for related work, our tableau calculus lies in the line of the one-pass calculi
based on sequents and tableaux calculi [
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 de ne A as :(>U:A). Given a set of formulas S, we denote with S the set f A j A 2 Sg.
PLTL is semantically characterized by rooted linearly ordered Kripke models; formally, a PLTL-model is a structure K = hP; ; ; V i where P is the set of S; :(AUB)
S; :B j S; :A; :B j S; A; :B; :(AUB) S; :(A _ B) S; :A; :B :_
S; ::A
S; A
T ; A; B A; B+; B j A; H1 j : : : j A; Hm :: Lin
S; :> S; ? :>
S; :? S; > :U :?
S; AUB S; B j S; A; :B; (AUB) S; : A S; :A :
S; A _ B S; A j S; B T V [ f:p j p 2 Vg [ f>; ?g, A is a possibly empty set, B = fU1; : : : ; Umg is a possibly empty set, with Ui = AiUBi or Ui = :(AiUBi) B+ = fUi+jUi 2 Bg, where Hi = f U1; U1+; : : : ; Ui 1; Ui+ 1g [ fUi g [ fUi+1; : : : ; Umg (i = 1; : : : ; m) worlds, is a linear well-order with minimum and no maximum element, V is a function associating with every world 2 P the set of propositional variables satis ed in . Given 2 P , the immediate successor of , denoted by 0, is the minimum of the <-successors of . The satis ability of a formula A in a world of K, written K; A (or simply A), is de ned as follows: { for p 2 V, { :A i { A i 0 { AUB i 9
p i p 2 V ( ); 1 A; A _ B i
A;
B and 8 : >;
1 ?; A or
B; < ,
A.
The following properties can be easily proved. The latter one follows by the fact
that is a well-order, hence, if B is satis able in some , there exists the
minimum satisfying B.
:
1 A and 8 :
;
A set of formulas S is satis able in (K; S) if every formula of S is satis able
in ; S is satis able if it is satis able 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 Godel-Dummett Logic DUM
presented in [
The rules of T are sound is the sense that, if the premise of a rule is satis able then one of its conclusions is satis able. We brie y discuss, by means
S S[>=p]
S S[?=p] + if p + S if p
S
S; A S[>=A]; A
S; A Sf>=Ag; A R-cl
S; :A S[?=A]; :A
S; :A Sf?=Ag; :A
R- :
R-cl: For for l 2 f+; g, p l S i p l H for every H 2 S where, p l H is de ned as follows: { p + p and p :p and p l H, if H 2 (V n fpg) [ f>; ?g; { p l (A _ B) i p l A and p l B; { p l (AUB) i p l A and p does not occur in B; { p l :(AUB) i p l B and p does not occur in A; { if A 6= BUC, then p + :A i p A and p :A i p + A; { p l A i p l A; of an example, the soundness of rule Lin. The application of rule Lin to f (A1UB1); :(A2UB2)g generates as conclusions the sets: B = C = fA1; :B2g [ B ; H1 = fB1; :(A2UB2)g ; H2 = f (A1UB1); A1; :A2; :B2g:
satis able. We have 0
B; we show that at least one of the conclusions is A1UB1 and 0 :(A2UB2). Note that: { { 0 0
A1UB1 ) 9 1 :(A2UB2) )
0 : 1 ( (i) 8
(ii) 9 2
suppose that (ii) holds; then: { if 0 < 1 and 0 < 2, then 0 { if 0 = 1, then 0 H1; { if 0 < 1 and 0 = 2, then 0
C; H2.
B1 and 8 : 0 0; 1 B2 or < 1;
A1. 0 : 2 1 A2 and 8 : 0 2; The notions of proof-table and branch are de ned as usual. A set S of formulas is closed if it either contains ? or it contains a formula A and its negation. Branches of a proof-table are generated alternating saturation phases, where rules di erent from Lin are applied as long as possible, and applications of rule Lin. We remark that, at the end of a saturation phase, we get a set of formulas which only contains literals, >, ? and formulas pre xed with . If during the saturation phase a closed set is generated the construction of the branch is aborted. During branch construction loops can be generated, hence a loop-checking mechanism is needed to assure termination. A loop is a sequence of consecutive sets of formulas S1; : : : ; Sn in a branch such that S1 = Sn and Si 6= Si+1 for every 1 i < n. Whenever, during a branch construction, a loop is detected the branch construction is aborted. A loop is closed if there exist i 2 f1; : : : ; n 1g and AUB 2 Si (:(AUB) 2 Si, respectively) such that B 62 Sj (f:A; :Bg 6 Sj , respectively) for every 1 j < n. A loop is open if it is not closed. A branch is closed if it contains a closed set of formulas or a closed loop and open otherwise. The proof of the completeness theorem for T is based on a procedure extracting a PLTL-model satisfying S from an open branch starting with S.
Although multi-conclusion rules as Lin can generate a huge number of branches,
as discussed in [
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 [
All the rules of Fig. 2 have the property that the premise is satis able i the
conclusion is. In the proof search procedure we apply the optimization rules and
the usual boolean simpli cation rules [
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
e ective 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 gures
related to PLTL, an OCaml prover based on the one-pass tableau calculus of [
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 [
Status Family lift sat. anzu-amba sat. acacia-demo-v3 sat. anzu-genbuf sat. rozier counters sat.