A Proof System for Temporal Reasoning with Sequential Information
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.
KeywordsInduction Hypothesis Proof System Sequence Model Linear Temporal Logic Propositional Variable
Unable to display preview. Download preview PDF.
- 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
- 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