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].

• Type: Journal
• Year: 2010
• Where: JAPLL
• Authors: Guillaume Hoffmann
• Keywords: JAPLL 2010, Prefixed Tableau Method, Satisfaction Operator, Transitive Modalities