Terminating tableau systems for hybrid logic with difference and converse (Q1047795): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s10849-009-9087-8 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1981904119 / rank | |||
Normal rank |
Revision as of 22:28, 19 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