Temporal Tableaux

R. KontchakovR. Kontchakov, Carsten LutzCarsten Lutz, Frank WolterFrank Wolter, M. ZakharyaschevM. Zakharyaschev

Datei:KoLuWoZa.ps.gz

Download

R. Kontchakov, Carsten Lutz, Frank Wolter, M. Zakharyaschev
Temporal Tableaux
Studia Logica, 76(1):91-134, 2004

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ KoLuWoZa-04,
  author = {R. {Kontchakov} and C. {Lutz} and F. {Wolter} and M. {Zakharyaschev}},
  journal = {Studia Logica},
  number = {1},
  pages = {91--134},
  title = {Temporal Tableaux},
  volume = {76},
  year = {2004},
}