Skip navigation
Skip navigation

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]

CollectionsANU Research Publications
Date published: 2005
Type: Conference paper
URI: http://hdl.handle.net/1885/83126
Source: Proceedings of TABLEAUX 2005

Download

There are no files associated with this item.


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

Updated:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator