Termination for Hybrid Tableaus |
Thomas Bolander, Patrick Blackburn
|
| Abstract | This article extends and improves work on tableau-based decision
methods for hybrid logic by Bolander and Bra\"uner [2006]. Their paper gives tableau-based decision
procedures for basic hybrid logic (with unary modalities) and the
basic logic extended with the global modality. All their proof
procedures make use of loop-checks to ensure termination.
Here we take a closer look at termination for hybrid tableaus. We
cover both types of system used in hybrid logic: prefixed tableaus and
internalised tableaus. We first treat prefixed tableaus. We prove a
termination result for the basic language (with n-ary operators)
that does not involve loop-checks. We then successively add the global
modality and n-ary inverse modalities, show why various different
types of loop-check are required in these cases, and then re-prove
termination. Following this we consider internalised tableaus. At
first sight, such systems seem to be more complex. However we define
a internalised system which terminates without loop-checks. It is
simpler than previously known internalised systems (all of which
require loop-checks to terminate) and simpler than our prefix systems
(no non-local side conditions on rules are required). |
| Keywords | Hybrid logic, modal logic, tableau systems, decisionprocedures, loop-checks. |
| Type | Journal paper [With referee] |
| Journal | Journal of Logic and Computation |
| Year | 2007 Vol. 17 No. 3 pp. 517-554 |
| Publisher | Oxford University Press |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |