Sciweavers

Share
TABLEAUX
2005
Springer

A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics

10 years 8 days ago
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 lemma for regular grammar logics using our calculus.
Rajeev Goré, Linh Anh Nguyen
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TABLEAUX
Authors Rajeev Goré, Linh Anh Nguyen
Comments (0)
books