LiU Electronic Press
Full-text not available in DiVA
Author:
Nguyen, Linh Anh (University of Warsaw)
Szalas, Andrzej (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab) (Linköping University, The Institute of Technology)
Title:
A tableau calculus 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:
Conference paper (Refereed)
Language:
English
In:
Proceedings of the 22nd International Conference on Automated Deduction (CADE)
Conference:
22nd International Conference on Automated Deduction
Publisher: Springer
Series:
Lecture Notes in Artificial Intelligence, ISSN 0302-9743; 5663
Volume:
5663 LNAI
Pages:
421-436
Year of publ.:
2009
URI:
urn:nbn:se:liu:diva-21208
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-21208
ISBN:
978-364202958-5
Subject category:
Engineering and Technology
SVEP category:
TECHNOLOGY
Abstract(en) :

We give a sound and complete tableau calculus for deciding the general satisfiability problem of regular grammar logics with converse (REG c logics). Tableaux of our calculus are defined as "and-or" graphs with global caching. Our calculus extends the tableau calculus for regular grammar logics given by Goré and Nguyen [11] by using a cut rule and existential automaton-modal operators to deal with converse. We use it to develop an ExpTime (optimal) tableau decision procedure for the general satisfiability problem of REG c logics. We also briefly discuss optimizations for the procedure.

Available from:
2009-09-30
Created:
2009-09-30
Last updated:
2011-04-13
Statistics:
35 hits