Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4663033 | Journal of Applied Logic | 2010 | 12 Pages |
Abstract
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 (2007) [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 (2009) [6].
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Guillaume Hoffmann,