LiU Electronic Press
Full-text not available in DiVA
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)
Language:
English
Place of publ.: Berlin/Heidelberg Publisher: Springer Berlin/Heidelberg
Status:
Published
In:
Studia Logica: An International Journal for Symbolic Logic(ISSN 0039-3215)(EISSN 1572-8730)
Volume:
98
Issue:
3
Pages:
387-428
Year of publ.:
2011
URI:
urn:nbn:se:liu:diva-72694
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-72694
Subject category:
Computer Science
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
Created:
2011-12-05
Last updated:
2011-12-12
Statistics:
18 hits