de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Tableau Calculi for Hybrid Logics

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45645

Tzakova,  Miroslava
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Tzakova, M. (1999). Tableau Calculi for Hybrid Logics. In N. V. Murray (Ed.), Proceedings of the International Conference TABLEAUX'99 - Automated Reasoning with Analytic Tableaux and Related Methods (pp. 278-292). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-369E-4
Abstract
Hybrid logics were proposed as a way of boosting the expressivity of modal logics via a novel mechanism: adding labels for states in Kripke models and viewing these labels as formulae. In addition, hybrid logics may contain quantifiers to bind the labels. Thus, hybrid logics have both Kripke semantics and a first-order binding apparatus. We present prefixed tableau calculi for weak hybrid logics (proper fragments of classical logic) as well as for hybrid logics having full first-order expressive power, and give a general method for proving completeness. For the weak quantifier-free logics we present a tableau-based decision procedure.