Tableau-Based Decision Procedures for Hybrid Logic



AbstractHybrid 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.
KeywordsHybrid logic, modal logic, universal modality, tableau systems, decision procedures.
TypeJournal paper [With referee]
JournalJournal of Logic and Computation
Year2006    Month December    Vol. 16    pp. 737-763
PublisherOxford University Press
ISBN / ISSN0955-792X
Publication linkhttp://logcom.oxfordjournals.org/
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering