Tableau-Based Decision Procedures for Hybrid Logic |
|
| Abstract | Hybrid logics are a principled generalization of both modal logics
and description logics. It is well-known that various hybrid logics
without binders
are decidable, but decision procedures are usually not
based on tableau systems,
a kind of formal proof procedure that lends itself towards computer
implementation.
In this paper we give four different tableau-based
decision procedures for a very expressive hybrid
logic including the universal modality; three of the procedures are
based on different tableau systems, and one procedure is based on a
Gentzen system.
The decision procedures make use of
so-called loop-checks which is a technique standardly used in connection
with tableau systems for other logics,
namely prefixed tableau systems for transitive modal logics, as well
as prefixed tableau systems for certain description logics. The
loop-checks used in our four decision procedures are similar, but
the four proof systems on which the procedures are based constitute a
spectrum of different systems: prefixed and internalized systems,
tableau and Gentzen systems. |
| Keywords | Hybrid logic, modal logic, universal modality,
tableau systems, decision procedures. |
| Type | Journal paper [With referee] |
| Journal | Journal of Logic and Computation |
| Year | 2006 Month December Vol. 16 pp. 737-763 |
| Publisher | Oxford University Press |
| ISBN / ISSN | 0955-792X |
| Publication link | http://logcom.oxfordjournals.org/ |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |