Temporal Tableaux

Aus International Center for Computational Logic
Version vom 19. März 2015, 18:44 Uhr von Marcel Lippmann (Diskussion | Beiträge)
(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)
Wechseln zu:Navigation, Suche

Toggle side column

Temporal Tableaux

R. KontchakovR. Kontchakov,  C. LutzC. Lutz,  F. WolterF. Wolter,  M. ZakharyaschevM. Zakharyaschev
R. Kontchakov, C. Lutz, F. 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},
}