Author:
Nguyen, Linh Anh (Institute of Informatics, Warsaw University)
Szalas, Andrzej (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab) (Linköping University, The Institute of Technology)
Title:
ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse
Department:
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Publication type:
Article in journal (Refereed)
Place of publ.:
Berlin/Heidelberg
Publisher:
Springer Berlin/Heidelberg
In:
Studia Logica: An International Journal for Symbolic Logic(ISSN 0039-3215)(EISSN 1572-8730)
URI:
urn:nbn:se:liu:diva-72694
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-72694
Keywords(en)
:
Modal logic, regular grammar logics with converse, automated reasoning, tableaux, global caching
Abstract(en)
:
Grammar logics were introduced by Fariñas 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 clogics is coNP-complete.
Available from:
2011-12-05
Statistics:
13 hits