ExpTime tableau decision procedures for regular grammar logics with converse (Q763333)

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.