Termination for Hybrid Tableaus

9 years 11 months ago
Termination for Hybrid Tableaus
Abstract. This article extends and improves work on tableau-based decision methods for hybrid logic by Bolander and Bra¨uner [5]. 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 whic...
Thomas Bolander, Patrick Blackburn
Added 16 Dec 2010
Updated 16 Dec 2010
Type Journal
Year 2007
Authors Thomas Bolander, Patrick Blackburn
Comments (0)