ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse

被引：7
|
作者：
Linh Anh Nguyen [1 ]
Szalas, Andrzej [1 ,2 ]
机构：
[1] Warsaw Univ, Inst Informat, Warsaw, Poland
[2] Linkoping Univ, Dept Comp & Informat Sci, S-58183 Linkoping, Sweden
来源：
STUDIA LOGICA | 2011年 / 98卷 / 03期
关键词：
Modal logic; regular grammar logics with converse; automated reasoning; tableaux; global caching; CALCULUS; CHECKING;
D O I：
10.1007/s11225-011-9341-3
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
Grammar logics were introduced by Farinas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse (REG(c) logics) and present sound and complete tableau calculi for the general satisfiability problem of REG(c) logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG(c) logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various optimization techniques can be applied. We also prove a new result that the data complexity of the instance checking problem in REG(c) logics is coNP-complete.
引用
收藏
页码：387 / 428
页数：42
相关论文
共 44 条
12345