A Proof System for Temporal Reasoning with Sequential Information

  • Norihiro Kamide
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6404)


A new logic, sequence-indexed linear-time temporal logic (SLTL), is obtained semantically from the standard linear-time temporal logic LTL by adding a sequence modal operator which represents a sequence of symbols. By the sequence modal operator of SLTL, we can appropriately express “sequential information” in temporal reasoning. A Gentzen-type sequent calculus for SLTL is introduced, and the completeness and cut-elimination theorems for this calculus are proved. SLTL is also shown to be PSPACE-complete and embeddable into LTL.


Induction Hypothesis Proof System Sequence Model Linear Temporal Logic Propositional Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Formal Models and Semantics (B), pp. 995–1072. Elsevier, MIT Press (1990)Google Scholar
  2. 2.
    Kamide, N., Kaneiwa, K.: Extended full computation-tree logic with sequence modal operator: representing hierarchical tree structures. In: Nicholson, A., Li, X. (eds.) AI 2009. LNCS (LNAI), vol. 5866, pp. 485–494. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  3. 3.
    Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33, 423–432 (1987)CrossRefzbMATHGoogle Scholar
  4. 4.
    A. Pnueli, The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)Google Scholar
  5. 5.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3), 733–749 (1985)CrossRefzbMATHGoogle Scholar
  6. 6.
    Wansing, H.: The Logic of Information Structures. LNCS, vol. 681, 163 pages. Springer, Heidelberg (1993)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Norihiro Kamide
    • 1
  1. 1.Waseda Institute for Advanced StudyWaseda UniversityTokyoJapan

Personalised recommendations