=Paper=
{{Paper
|id=Vol-1459/paper13
|storemode=property
|title=Towards a tableau-based procedure for PLTL based on a
multi-conclusion rule and logical optimizations
|pdfUrl=https://ceur-ws.org/Vol-1459/paper13.pdf
|volume=Vol-1459
|dblpUrl=https://dblp.org/rec/conf/cilc/FerrariFF15
}}
==Towards a tableau-based procedure for PLTL based on a
multi-conclusion rule and logical optimizations==
https://ceur-ws.org/Vol-1459/paper13.pdf
Towards a tableau-based procedure for PLTL
based on a multi-conclusion rule and logical
optimizations
Mauro Ferrari1 , Camillo Fiorentini2 , Guido Fiorino3
1
DiSTA, Univ. degli Studi dell’Insubria, Via Mazzini, 5, 21100, Varese, Italy
2
DI, Univ. degli Studi di Milano, Via Comelico, 39, 20135 Milano, Italy
3
DISCO, Univ. degli Studi di Milano-Bicocca, Viale Sarca, 336, 20126, Milano, Italy
Abstract. 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 dis-
cuss the performances of a Prolog prototype of our procedure.
1 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 implementa-
tion 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 tech-
niques discussed in [1]. The results in [8, 15] are based on resolution, thus they
are related less to our approach.
2 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 = hP, ≤, ρ, V i where P is the set of
S, AUB S, ¬(AUB)
U ¬U
S, B | S, A, ¬B, ◦(AUB) S, ¬B | S, ¬A, ¬B | S, A, ¬B, ◦¬(AUB)
S, ¬ ◦ A S, A ∨ B S, ¬(A ∨ B) S, ¬¬A S, ¬> S, ¬⊥
¬◦ ∨ ¬∨ ¬¬ ¬> ¬⊥
S, ◦¬A S, A | S, B S, ¬A, ¬B S, A S, ⊥ S, >
T , ◦A, ◦B
Lin
+
A, B , ◦B | A, H1 | . . . | A, Hm
T ⊆ V ∪ {¬p | p ∈ V} ∪ {>, ⊥}, A is a possibly empty set,
B = {U1 , . . . , Um } is a possibly empty set, with Ui = Ai UBi or Ui = ¬(Ai UBi )
B+ = {Ui+ |Ui ∈ B}, where
(AUB)+ = A (AUB)− = B
( ¬(AUB) )+ = ¬B ( ¬(AUB) )− = ¬A, ¬B
Hi = {◦U1 , U1+ , . . . , ◦Ui−1 , Ui−1
+
} ∪ {Ui− } ∪ {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 α0 , 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 (α); α >; α 1 ⊥;
– α ¬A iff α 1 A; α A ∨ B iff α A or α B;
– α ◦A iff α0 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;
– α 1 AUB iff (∀γ ≥ α, γ 1 B) or (∃β ≥ α : β 1 A and ∀γ : α ≤ γ ≤ β, γ 1 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 sat-
isfiable then one of its conclusions is satisfiable. We briefly discuss, by means
S, A S, ¬A
R- R-¬
S[>/A], A S[⊥/A], ¬A
S, A S, ¬A
R-cl R-cl¬
S{>/A}, A S{⊥/A}, ¬A
For for l ∈ {+, −}, pl S iff pl H for every H ∈ S where,
pl H is defined as follows:
S
+ if p+ S
S[>/p] – p+ p and p− ¬p and pl H, if H ∈ (V \ {p}) ∪ {>, ⊥};
– pl (A ∨ B) iff pl A and pl B;
S – pl (AUB) iff pl A and p does not occur in B;
− if p− S – pl ¬(AUB) iff pl B and p does not occur in A;
S[⊥/p]
– if A 6= BUC, then p+ ¬A iff p− A and p− ¬A iff p+ A;
– pl ◦ A iff pl A;
Fig. 2. Optimization rules for PLTL
of an example, the soundness of rule Lin. The application of rule Lin to ◦B =
{◦(A1 UB1 ), ◦¬(A2 UB2 )} generates as conclusions the sets:
C = {A1 , ¬B2 } ∪ ◦B , H1 = {B1 , ¬(A2 UB2 )} , H2 = {◦(A1 UB1 ), A1 , ¬A2 , ¬B2 }.
Let us assume that α ◦B; we show that at least one of the conclusions is
satisfiable. We have α0 A1 UB1 and α0 ¬(A2 UB2 ). Note that:
– α0 A1 UB1 ⇒ ∃β1(≥ α0 : β1 B1 and ∀γ : α0 ≤ γ < β1 , γ A1 .
(i) ∀γ ≥ α0 , γ 1 B2 or
– α0 ¬(A2 UB2 ) ⇒
(ii) ∃β2 ≥ α0 : β2 1 A2 and ∀γ : α0 ≤ γ ≤ β2 , γ 1 B2
If (i) holds either α0 < β1 and α0 C, or α0 = β1 and α0 H1 . Now, let us
suppose that (ii) holds; then:
– if α0 < β1 and α0 < β2 , then α0 C;
– if α0 = β1 , then α0 H1 ;
– if α0 < β1 and α0 = β2 , then α0 H2 .
The notions of proof-table and branch are defined 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 different
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 prefixed 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 ∈ {1, . . . , n − 1}
and AUB ∈ Si (¬(AUB) ∈ Si , respectively) such that B 6∈ Sj ({¬A, ¬B} 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 [7], theorem provers using these kind of rules can be effective.
To improve the performances of the above procedure we exploit the optimiza-
tion 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 (pl 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.
3 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 sim-
ple 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 optimiza-
tions, 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].
4
Available at http://www2.disco.unimib.it/fiorino/beta.tgz
Family Status β PLTL Family Status β PLTL
lift sat. 76 42 lift unsat. 0 8
anzu-amba sat. 18 38 schuppan-O1 unsat. 27 10
acacia-demo-v3 sat. 12 12 schuppan-O2 unsat. 7 10
anzu-genbuf sat. 28 26 schuppan-phltl unsat. 5 3
rozier counters sat. 35 65
Fig. 3. Comparison between β and PLTL
References
1. A. Bolotov, O. Grigoriev, and V. Shangin. Automated natural deduction for propo-
sitional linear-time temporal logic. In TIME (2007), pages 47–58. IEEE Computer
Society, 2007.
2. K. Brünnler and M. Lange. Cut-free sequent systems for temporal logic. Journal
of Logic and Algebraic Programming, 76(2):216–225, 2008.
3. M. Ferrari, C. Fiorentini, and G. Fiorino. fCube: An efficient prover for intuition-
istic propositional logic. In C. G. Fermüller et al., editor, LPAR-17, volume 6397
of LNCS, pages 294–301. Springer, 2010.
4. M. Ferrari, C. Fiorentini, and G. Fiorino. Simplification rules for intuitionis-
tic propositional tableaux. ACM Transactions on Computational Logic (TOCL),
13(2):14:1–14:23, 2012.
5. M. Ferrari, C. Fiorentini, and G. Fiorino. An evaluation-driven decision procedure
for G3i. ACM Transactions on Computational Logic (TOCL), 6(1):8:1–8:37, 2015.
6. G. Fiorino. Tableau calculus based on a multiple premise rule. Information Sci-
ences, 180(19):371–399, 2010.
7. G. Fiorino. Refutation in Dummett logic using a sign to express the truth at the
next possible world. In T. Walsh, editor, IJCAI 2011, pages 869–874. IJCAI/AAAI,
2011.
8. M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions
on Computational Logic (TOCL), 2(1):12–56, 2001.
9. J. Gaintzarain, M. Hermo, P. Lucio, and M. Navarro. Systematic semantic tableaux
for PLTL. Electronic Notes in Theoretical Computer Science, 206:59–73, 2008.
10. J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas. Dual systems of
tableaux and sequents for PLTL. Journal of Logic and Algebraic Programming,
78(8):701–722, 2009.
11. F. Massacci. Simplification: A general constraint propagation technique for propo-
sitional and modal tableaux. In Harrie de Swart, editor, TABLEAUX’98, volume
1397 of LNCS, pages 217–232. Springer-Verlag, 1998.
12. B. Paech. Gentzen-systems for propositional temporal logics. In E. Börger et al.,
editor, CSL’88, volume 385 of LNCS, pages 240–253. Springer, 1988.
13. R. Pliuskevicius. Investigation of finitary calculus for a discrete linear time logic by
means of infinitary calculus. In J. Barzdins et al., editor, Baltic Computer Science,
volume 502 of LNCS, pages 504–528. Springer, 1991.
14. S. Schwendimann. A new one-pass tableau calculus for PLTL. In H. C. M. de Swart,
editor, TABLEAUX’98, volume 1397 of LNCS, pages 277–291. Springer, 1998.
15. M. Suda and C. Weidenbach. Labelled superposition for PLTL. In N. Bjørner
et al., editor, LPAR-18, volume 7180 of LNCS, pages 391–405. Springer, 2012.