@inproceedings{bb543b1f69784cfc8ab2351b67725c71,
title = "A tableau calculus with automaton-labelled formulae for regular grammar logics",
abstract = "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.",
author = "Rajeev Gor{\'e} and Nguyen, {Linh Anh}",
year = "2005",
doi = "10.1007/11554554_12",
language = "English",
isbn = "3540289313",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "138--152",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 14th International Conference, TABLEAUX 2005, Proceedings",
address = "Germany",
note = "14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2005 ; Conference date: 14-09-2005 Through 17-09-2005",
}