Lightweight hybrid tableaux

12 years 11 months ago
Lightweight hybrid tableaux
We present a decision procedure for hybrid logic equipped with nominals, the satisfaction operator and existential, difference, converse, reflexive, symmetric and transitive modalities. This decision procedure is a prefixed tableau method based on the one introduced by Bolander and Blackburn in [2]. It enhances its predecessor in terms of computational efficiency and handles more expressive logics. Its way of ensuring termination enables addition of rules for the difference modality, inspired by Kaminski and Smolka in [5].
Guillaume Hoffmann
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Authors Guillaume Hoffmann
Comments (0)