Tableau System and Theorem Prover for Temporal Logic K_{t}

Akio MARUYAMA and Toshimasa MATSUMOTO

                    {maruyama, tmatsumo}@jaist.ac.jp

Japan Advanced Institute of Science and Technology

1 Introduction

Sequent systems and tableau systems for temporal logics have been discussed in papers [1, 3, 4, 7]. Nishimura [7] and Kashima [3] introduced sequent systems, and Gore [1] studied a tableau system.

In this paper, we introduce sequent systems and tableau ones for the minimal temporal logic K_{t}. Our aim is to implement a decision algorithm of K_{t} based on tableau systems as a theorem prover, since tableau systems are well-suited for proof search by computers. To get an efficient algorithm, we propose a restricted tableau system for K_{t}. Main difficulty in implementation is that rules of a restricted tableau system for K_{t} cause two kinds of loops. Heuerding [2] and Mouri [6] have introduced histories into sequent systems for KT and S4 for loop-checking. Matsumoto [5] has applied a special modal operator by Mouri [6] to the tableau system for KT to eliminate loops. Therefore, we expect that histories will be useful for loop-checking in the tableau system for K_{t}.

2 Temporal Logic K_{t}

In temporal logic K_{t}, [F] and [P] are used as temporal operators. Formulas A, B, ⋯ are defined in usual way, and [F]A and [P]A are read as “at all future times A” and “at all past times A”, respectively. Both ⟨F ⟩A and ⟨P ⟩A are abbreviations of ¬[F]¬A and ¬[P]¬A, respectively. The temporal logic K_{t} has classical tautologies and the following as axioms, and has modus ponens and the rule of necessitation for temporal operators [F] and [P] as rules of inference.

\begin{aligned}KF & : & [F](A ⊃ B) ⊃ ([F]A ⊃ [F]B), & KP & : & [P](A ⊃ B) ⊃ ([P]A ⊃ [P]B), \\ 4F & : & [F]A ⊃ [F][F]A, & 4P & : & [P]A ⊃ [P][P]A, \\ CF & : & A ⊃ [F]⟨P ⟩A, & CP & : & A ⊃ [P]⟨F ⟩A. \end{aligned}

Let W be a non-empty set of possible worlds, and let R_{T} be a binary relation on W. A Kripke frame for temporal logic is defined to be a pair (W, R_{T}). Kripke semantics are given in the usual way, and valuations ⊧ for [F]A and [P]A are defined as follows:

u ⊧ [F]A iff for all v ∈ W (uR_{T} v implies v ⊧ A), u ⊧ [P]A iff for all v ∈ W (vR_{T} u implies v ⊧ A).

Proposition 2.1 Let (W, R_{T}) be any Kripke frame. Then, 4F and 4P are valid on (W, R_{T}) iff R_{T} is transitive.

A Kripke frame (W, R_{T}) satisfying a condition that R_{T} is transitive is called K_{t}-frame. It can be easily to show that the completeness theorem holds for K_{t}, i.e K_{t} ⊬ A iff there exists K_{t}-model M such that M |̸= A.

Greek capital letters Γ, Δ ⋯ denote finite sets of formulas. The set of all subformulas of A and the set of all subformulas of formulas in Γ are denoted by Sub(A) and Sub(Γ), respectively. The notation ¬Sub(Γ) is abbreviation of {¬A|A ∈ Sub(Γ)}. The set of all propositional variables in A is denoted by V ar(A).

3 Sequent System for K_{t}

In this section, we introduce three sequent systems for temporal logic K_{t}. All of them lack the cutelimination property. Using Takano’s method, however, we can derive some important logical properties for K_{t} using these systems.

The sequent system S(K_{t}) is obtained from the propositional fragment of the sequent system LK for the classical logic by adding the following two temporal rules:

{[F]Γ, Γ → [P]Δ, [P]Π, A \atop [F]Γ → [P]Δ, Π, [F]A} (T 1)  {[P]Γ, Γ → [F]Δ, [F]Π, A \atop [P]Γ → [F]Δ, Π, [P]A} (T 2)

The cut rule whose cut formula is restricted to a subformula of formulas in the lower sequent is called the acceptable cut. The sequent system obtained from S(K_{t}) by replacing cut rule by acceptable cut rule is denoted by S(K_{t})^{∗}. Furthermore, a restricted sequent system S(K_{t})^{∗∗} is defined as the system S(K_{t})^{∗} with conditions [P]Π ⊆ Sub(Γ ∪ Δ ∪ {A}) in applying the rule (T 1) and [F]Π ⊆ Sub(Γ ∪ Δ ∪ {A}) in applying the rule (T 2). Then we can prove that all of sequent systems S(K_{t}), S(K_{t})^{∗} and S(K_{t})^{∗∗} are equivalent. The following interpolation theorem for Kt is shown by using Maehara’s method in S(K_{t})^{∗}.

Theorem 3.1 (interpolation theorem) If A ⊃ B is provable in K_{t}, then there exists a formula C such that (i) A ⊃ C and C ⊃ B are both provable in K_{t} and (ii) V ar(C) ⊆ V ar(A) ∩ V ar(B).

The sequent system S(K_{t})^{∗∗} has the subformula property, i.e. every formula A provable in S(K_{t})^{∗∗} has such a proof P that every formula appearing in P is a subformula of A. Therefore, we can get a decision procedure for S(K_{t})^{∗∗} by using Gentzen’s method. However the procedure is not always efficient. In order to obtain a more efficient decision procedure, we propose the procedure with tableau system in the next section.

4 Tableau System for K_{t}

In this section, we propose a tableau system for K_{t}. A tableau system consist of a set of tableau rules. A tableau for Γ is a finite tree with the root Γ, each of whose nodes carries a finite set of formulas. To check whether A is provable in a tableau system or not, we give ¬A to the tableau procedure as an input. A tableau is closed if all of leaves of the tableau end with {f}. Otherwise, it is open. A tableau system for K_{t}, denoted by T (K_{t}), is obtained by adding the following tableau rules to the standard tableau system for classical logic, and the right tableau is an example of a closed tableau for CF:

{Γ \atop Γ, A | Γ, ¬A} (cut)

{Δ, [F]Γ, ¬[F]A \atop Γ, [F]Γ, ¬A} (K4F)  {Δ, [P]Γ, ¬[P]A \atop Γ, [P]Γ, ¬A} (K4P)

{Γ, ¬[F]A \atop ¬[P]¬Γ, ¬A} (CF)  {Γ, ¬[P]A \atop ¬[F]¬Γ, ¬A} (CP)

\begin{matrix}{¬(A ⊃ [F]¬[P]¬A) \atop A, ¬[F]¬[P]¬A} ; ¬[P]¬A, ¬¬[P]¬A & (CF) \\ ¬[P]¬A, [P]¬A \end{matrix} ; ¬¬A, ¬A, [P]¬A ; (K4P) ; A, ¬A, [P]¬A ; f

A closed tableau for CF

Here, we face with a problem: it is hard to search a tableau of T (K_{t}) for a given formula A, because the cut-formula of (cut) is arbitrary. Therefore, we give conditions for applying some rules of T (K_{t}) as Takano [8]. A restricted tableau system T (K_{t})^{∗} is obtained by replacing (cut), (CF) and (CP) of T (K_{t}) with the following restricted rules, respectively:

{Γ \atop Γ, A | Γ, ¬A} (cut)^{∗}  {Γ, ¬[F]A \atop ¬[P]¬Γ, ¬A} (CF)^{∗}  {Γ, ¬[P]A \atop ¬[F]¬Γ, ¬A} (CP)^{∗}
where A ∈ Sub(Γ)  where ¬[P]¬Γ ⊆ Sub(A)  where ¬[F]¬Γ ⊆ Sub(A)

¿From these conditions, we can say that any tableau of T (K_{t})^{∗} for Γ is constructed by formulas in Sub(Γ) ∪ ¬Sub(Γ) ∪ {f}. This property is very useful for searching tableaus.

Theorem 4.1 The tableau system T (K_{t})^{∗} is sound with respect to K_{t}-frames.

In order to show completeness of T (K_{t})^{∗} we need some technical machinery (see [1] for the details).

Conjecture 4.2 The tableau system T (K_{t})^{∗} is complete with respect to K_{t}-frames.

If we check all nodes of each tableau and find loops, then we stop constructing tableau any more. Hence, we can show the decidability of T (K_{t})^{∗}. But the loop-checking causes inefficiency.

5 Implementing Theorem Prover for K_{t}

In implementing theorem prover for K_{t}, we have to avoid two kinds of loops caused by applications of tableau rules. One is caused by applications of (K4F) or (K4P), the other is caused by alternating applications of (CF) and (CP) as follows:

{[F]¬[F]¬A, ¬[F]A, ¬A \atop [F]¬[F]¬A, ¬[F]A, ¬A} (K4F) ; ⋮ ; (K4F)  \begin{matrix}{A, ¬[F]¬[P]¬A \atop ¬[P]¬A, ¬¬[P]¬A} & (CF) \\ ¬[P]¬A, [P]¬A \end{matrix} ; ¬¬A, ¬[F]¬[P]¬A ; (CP) ; A, ¬[F]¬[P]¬A ; ⋮ ; (CF)

To avoid these loops, we will need to introduce “histories” as Heuerding [2] and Mouri [6] did. This will be left for further work.

References

[1] R. Goré, Tableau Methods for Modal and Temporal Logics, in Handbook of Tableau Methods, eds. by M. D’Agostino, D. M.Gabby, R. Hähnle and J. Posegga, Kluwer Academic Publishers, 1999.

[2] A. Heuerding, M. Seyfried and H. Zimmermann, Efficient Loop-Check for Backward Proof Search in Some Non-Classical Propositional Logics, eds. by P. Miglioli, U. Moscato, D. Mundici and M. Ornaghi, Tableaux 96, LNCS 1071, pp. 201-225, 1996.

[3] R. Kashima, Cut-Free Sequent Calculi for Some Tence Logics, Studia Logica 53, pp. 199-135, 1994.

[4] A. Maruyama, S. Tojo and H. Ono, Decidability of Temporal Epistemic Logics for Multi-Agent Models, Proceedings of the ICLP’01 Workshop on Computational Logic in Multi-Agent Systems (CLIMA-01), pp. 31-40, 2001.

[5] T. Matsumoto and H. Ono, Theorem Prover for Modal Logics with Tableau Method, Proceedings of International Workshop RPC’01, pp. 42-59, 2001.

[6] M. Mouri, An Efficient Construction of Counter-Models for Modal Logic S4, Proceedings of International Workshop RPC’01, pp. 247-256, 2001.

[7] H. Nishimura, A Study of Some Tense Logics by Gentzen’s Sequential Method, Publications of the Research Institute for Mathematical Sciences, Kyoto University 16, pp. 343-353, 1980.

[8] M. Takano, Subformula Property as a Substitute for Cut-Elimination in Modal Propositional Logics, Mathematica Japonica 37, pp. 1129-1145, 1992.