2002 | OriginalPaper | Buchkapitel
HyLoRes 1.0: Direct Resolution for Hybrid Logics
verfasst von : Carlos Areces, Juan Heguiabehere
Erschienen in: Automated Deduction—CADE-18
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Hybrid languages are modal languages that allow direct reference to the elements of a model. Even the basic hybrid language $$ {\text{(}}\mathcal{H}{\text{(@))}} $$, which only extends the basic modal language with the addition of nominals (i,j, k,...) and satisfiability operators (@ i , @ j , @ k ,...), increases the expressive power: it can explicitly check whether the point of evaluation is a specific, named point in the model (w ⊩ i), and whether a named point satisfies a given formula (w ⊩ @ iϕ ). The extended expressivity allows one to define elegant decision algorithms, where nominals and @ play the role of labels, or prefixes, which are usually needed during the construction of proofs in the modal setup [5,3]. Note that they do so inside the object language. All these features we get with no increase in complexity: the complexity of the satisfiability problem for $$ \mathcal{H}{\text{(@)}} $$ is the same as for the basic modal language, PSPACE [2]. When we move to very expressive hybrid languages containing binders, we obtain an impressive boost in expressivity, but usually we also move beyond the boundaries of decidability. Classical binders like ∀ and ∃ (together with @) make the logic as expressive as first-order logic (FOL) while adding the more “modal” binder ↓ gives a logic weaker than FOL [1]. We refer to the Hybrid Logic site at http://www.hylo.net for a broad on-line bibliography.