Original Articles |
Termination for Hybrid Tableaus
Informatics and Mathematical Modelling, Richard Petersens Plads, Building 322, Technical University of Denmark, DK-2800 Lyngby, Denmark. E-mail: tb{at}imm.dtu.dk
Inria Lorraine, 615, Rue du Jardin Botanique, 54602 Villers Lès Nancy Cedex, France. E-mail: patrick.blackburn{at}loria.fr
Received 9 October 2006.
 |
Abstract |
|---|
This article extends and improves work on tableau-based decision methods for hybrid logic by Bolander and Braüner. 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 internalized 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 internalized tableaus. At first sight, such systems seem to be more complex. However, we define a internalized system which terminates without loop-checks. It is simpler than previously known internalized 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; Decision procedures; Loop-checks