Temporal Tableaux

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

Temporal Tableaux

R. KontchakovR. Kontchakov,  Carsten LutzCarsten Lutz,  Frank WolterFrank Wolter,  M. ZakharyaschevM. Zakharyaschev
R. Kontchakov, Carsten Lutz, Frank Wolter, M. Zakharyaschev
Temporal Tableaux
Studia Logica, 76(1):91-134, 2004
  • 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},
}