ExpTime tableau decision procedures for regular grammar logics with converse (Q763333): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 02:10, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | ExpTime tableau decision procedures for regular grammar logics with converse |
scientific article |
Statements
ExpTime tableau decision procedures for regular grammar logics with converse (English)
0 references
9 March 2012
0 references
The paper presents sound and complete tableau calculi for the general satisfiability problem of regular grammar logics with converse and the problem of checking consistency of an ABox w.r.t. a TBox in such a logic. The authors use a direct approach instead of a translation to another logic, which seems to be something new for grammar logics with converse. In particular, they give an optimal decision procedure for the general satisfiability problem of REGc logics with the corresponding complexity proofs. They prove the new result that the data complexity of the instance checking problem in regular grammar logics is coNP-complete.
0 references
modal logic
0 references
regular grammar logics with converse
0 references
automated reasoning
0 references
tableaux
0 references
global caching
0 references
satisfiability
0 references