Tableaux for Regular Grammar Logics of Agents Using Automaton-Modal Formulae

A grammar logic is a multimodal logic extending Kn with inclusion axioms of the form [t1]...[th]j (r) [s1]...[sk]j where t1, ..., th, s1, ..., sk are modal indices. Such an axiom can be seen as the grammar rule t1...th (r) s1...sk where the corresponding side stands for the empty word if k = 0 or h = 0. Thus the inclusion axioms of a grammar logic L capture a grammar G(L). This grammar is context-free if its rules are of the form t (r) s1...sk and is regular if it is context-free and for every modal index t there exists a finite automaton At that recognises the words derivable from t using G(L). A regular grammar logic L is a grammar logic whose inclusion axioms correspond to grammar rules that collectively capture a regular grammar G(L). We present sound and complete tableau calculi for the class of regular grammar logics and a class eRG of extended regular grammar logics which contains useful epistemic logics for reasoning about beliefs of agents. Our tableau rules use a special feature called automaton-modal formulae which are similar to formulae of automaton propositional dynamic logic. Our calculi are cut-free and have the analytic superformula property so they give decision procedures. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also prove that the general satisfiability problem of eRG logics is EXPTIME-complete.