A tableau calculus with automaton-labelled formulae for regular grammar logics
Gore, Rajeev; Nguyen, Linh Anh
Description
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]
Collections | ANU Research Publications |
---|---|
Date published: | 2005 |
Type: | Conference paper |
URI: | http://hdl.handle.net/1885/83126 |
Source: | Proceedings of TABLEAUX 2005 |
Download
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