@ARTICLE\{IMM2007-05013,
    author       = "T. Bolander and P. Blackburn",
    title        = "Termination for Hybrid Tableaus",
    year         = "2007",
    keywords     = "Hybrid logic, modal logic, tableau systems, decisionprocedures, loop-checks.",
    pages        = "517-554",
    journal      = "Journal of Logic and Computation",
    volume       = "17",
    editor       = "",
    number       = "3",
    publisher    = "Oxford University Press",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5013-full.html",
    abstract     = "This article extends and improves work on tableau-based decision
methods for hybrid logic by Bolander and Bra\$\backslash\$''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)."
}