Terminating tableau systems for hybrid logic with difference and converse (Q1047795)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Terminating tableau systems for hybrid logic with difference and converse |
scientific article; zbMATH DE number 5653949
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Terminating tableau systems for hybrid logic with difference and converse |
scientific article; zbMATH DE number 5653949 |
Statements
Terminating tableau systems for hybrid logic with difference and converse (English)
0 references
6 January 2010
0 references
The paper presents a tableau-based decision procedure for hybrid logic with global, difference, and converse modalities, considering also reflexive and transitive relations. The main contributions are a new model existence theorem, a terminating control that does not rely on the usual chain-based blocking scheme, a new treatment of the equational constraints that come with nominals and difference, and a terminating tableau for difference modalities.
0 references
modal logic
0 references
hybrid logic
0 references
difference modality
0 references
tableau systems
0 references
tableau-based decision procedure
0 references
0.96932214
0 references
0 references
0.9105329
0 references
0 references
0.8967644
0 references
0 references
0.88663584
0 references
0.8784274
0 references
