A tableau calculus with automaton-labelled formulae for regular grammar logics
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|
|Source:||Proceedings of TABLEAUX 2005|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.