Terminating tableau systems for hybrid logic with difference and converse (Q1047795): Difference between revisions
From MaRDI portal
Latest revision as of 08:48, 2 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Terminating tableau systems for hybrid logic with difference and converse |
scientific article |
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