Skip navigation
Skip navigation

A tableau calculus with automaton-labelled formulae for regular grammar logics

Gore, Rajeev; Nguyen, Linh Anh


We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation...[Show more]

CollectionsANU Research Publications
Date published: 2005
Type: Conference paper
Source: Proceedings of TABLEAUX 2005


There are no files associated with this item.

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator