Propositional temporal logics: decidability and completeness

&
Logic Journal of the IGPL 8 (1):55-85 (2000)
  Copy   BIBTEX

Abstract

A sound and complete axiomatic system and a tableau-based decision procedure are presented for propositional temporal logic over linear and discrete time models. The axiomatic system and decision procedure are presented for the full logic, including the past operators, but contain a clear identification of the parts whose omission yields axiomatization and a decision procedure for the future fragment. The paper summarizes work of over 20 years and is intended to provide a definitive reference to the version of propositional temporal logic used for the specification and verification of reactive systems

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/8.1.55

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,438

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Cut-free sequent and tableau systems for propositional diodorean modal logics.Rajeev Goré - 1994 - Studia Logica 53 (3):433 - 457.
Calendar Logic.Hans Jürgen Ohlbach & Dov Gabbay - 1998 - Journal of Applied Non-Classical Logics 8 (4):291-323.
Adding a temporal dimension to a logic system.Marcelo Finger & Dov M. Gabbay - 1992 - Journal of Logic, Language and Information 1 (3):203-233.
Decidability of an Xstit Logic.Gillman Payette - 2014 - Studia Logica 102 (3):577-607.
The Unrestricted Combination of Temporal Logic Systems.Marcelo Finger & M. Weiss - 2002 - Logic Journal of the IGPL 10 (2):165-189.
An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
Completeness and decidability results for some propositional modal logics containing “actually” operators.Dominic Gregory - 2001 - Journal of Philosophical Logic 30 (1):57-78.
Temporal non-commutative logic: Expressing time, resource, order and hierarchy.Norihiro Kamide - 2009 - Logic and Logical Philosophy 18 (2):97-126.
Completeness and decidability of tense logics closely related to logics above K.Frank Wolter - 1997 - Journal of Symbolic Logic 62 (1):131-158.
A new algebraic semantic approach and some adequate connectives for computation with temporal logic over discrete time.Alfredo Burrieza & Inma P. De Guzmán - 1992 - Journal of Applied Non-Classical Logics 2 (2):181-200.
Reasoning about sequences of memory states.Rémi Brochenin, Stéphane Demri & Etienne Lozes - 2010 - Annals of Pure and Applied Logic 161 (3):305-323.
A loop-free decision procedure for modal propositional logics k4, s4 and S.Dorota Leszczyńska-Jasion - 2009 - Journal of Philosophical Logic 38 (2):151 - 177.
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief.Michael Wooldridge, Clare Dixon & Michael Fisher - 1998 - Journal of Applied Non-Classical Logics 8 (3):225-258.
Decidability Results for Metric and Layered Temporal Logics.Angelo Montanari & Alberto Policriti - 1996 - Notre Dame Journal of Formal Logic 37 (2):260-282.
Decidable fragments of first-order temporal logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.

Analytics

Added to PP
2015-02-04

Downloads
13 (#1,020,434)

6 months
2 (#1,221,975)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

View all 14 citations / Add more citations

References found in this work

No references found.

Add more references