Lightweight hybrid tableaux (Q631086): Difference between revisions
From MaRDI portal
Changed an Item |
Changed an Item |
||
Property / describes a project that uses | |||
Property / describes a project that uses: KL-ONE / rank | |||
Normal rank |
Revision as of 03:53, 28 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Lightweight hybrid tableaux |
scientific article |
Statements
Lightweight hybrid tableaux (English)
0 references
22 March 2011
0 references
The paper presents a decision procedure for some fragments of the hybrid logic. The main difference between hybrid logic and modal logic is the presence of nominals, which are propositional symbols true at exactly one world in a model. The decision procedure is based on a prefixed tableau calculus. The general idea of the termination proof of this system is that, on the one hand, the quasi-subformula property guarantees that a given prefix can only make true finitely many formulas and, on the other hand, there can only be finitely many prefixes in a branch of the tableau.
0 references
hybrid logic
0 references
modal logic
0 references
tableau calculus
0 references
decision procedure
0 references
loop-check
0 references
difference modality
0 references
converse modality
0 references
nominals
0 references