Tableau Calculi for Hybrid Logics

Tzakova, Miroslava

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Tableau Calculi for Hybrid Logics

MPS-Authors

/persons/resource/persons45645

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

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: https://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.