liu.seSearch for publications in DiVA
ReferencesLink to record
Permanent link

Direct link
A tableau calculus for regular grammar logics with converse
2009 (English)In: Proceedings of the 22nd International Conference on Automated Deduction (CADE), Springer, 2009, Vol. 5663 LNAI, 421-436Konferensbidrag (Refereed)
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.

Series
Lecture Notes in Artificial Intelligence, ISSN 0302-9743 ; 5663
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-21208 (URN)10.1007/978-3-642-02959-2_31 (DOI)978-364202958-5 (ISBN)oai:DiVA.org:liu-21208 (OAI)
Conference
22nd International Conference on Automated Deduction
Available from2009-09-30 Created:2009-09-30 Last updated:2011-04-13

Open Access in DiVA

No fulltext

Other links

Publisher's fulltext

Search in DiVA

By author/editor
Nguyen, Linh AnhSzalas, Andrzej
By organisation
University of WarsawKPLAB - Knowledge Processing LabThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Citations

Web of Science®:

Altmetric score

Totalt: 36 hits
ReferencesLink to record
Permanent link

Direct link