Terminating tableau systems for hybrid logic with difference and converse (Q1047795): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Revision as of 03:01, 5 March 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
