Temporalising tableaux

Studia Logica 76 (1):91 - 134 (2004)
  Copy   BIBTEX

Abstract

As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 89,718

External links

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

Through your library

Analytics

Added to PP
2009-01-28

Downloads
129 (#128,910)

6 months
3 (#435,525)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Semantical Considerations on Modal Logic.Saul Kripke - 1963 - Acta Philosophica Fennica 16:83-94.
Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
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.
The tableau method for temporal logic: An overview.Pierre Wolper - 1985 - Logique Et Analyse 28 (110-111):119-136.
Decidable fragments of first-order modal logics.Frank Wolter & Michael Zakharyaschev - 2001 - Journal of Symbolic Logic 66 (3):1415-1438.

View all 11 references / Add more references