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)
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
URI:
urn:nbn:se:liu:diva-21208
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-21208
Subject category:
Engineering and 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
Statistics:
31 hits