Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse ( REG c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various (...) optimization techniques can be applied. We also prove a new result that the data complexity of the instance checking problem in REG c logics is coNP-complete. (shrink)

A serial context-free grammar logic is a normal multimodal logic L characterized by the seriality axioms and a set of inclusion axioms of the form □tφ→□s1…□skφ. Such an inclusion axiom corresponds to the grammar rule t → s1… sk. Thus the inclusion axioms of L capture a context-free grammar . If for every modal index t, the set of words derivable from t using is a regular language, then L is a serial regular grammar logic. In this paper, we present (...) an algorithm that, given a positive multimodal logic program P and a set of finite automata specifying a serial regular grammar logic L, constructs a finite least L-model of P. A least L-model M of P has the property that for every positive formula φ, P ⊧ φ iff M ⊧ φ. The algorithm runs in exponential time and returns a model with size 2O. We give examples of P and L, for both of the case when L is fixed or P is fixed, such that every finite least L-model of P must have size 2Ω. We also prove that if G is a context-free grammar and L is the serial grammar logic corresponding to G then there exists a finite least L-model of □s p iff the set of words derivable from s using G is a regular language. (shrink)

(2012). Modal logics for reasoning about infinite unions and intersections of binary relations. Journal of Applied Non-Classical Logics: Vol. 22, No. 4, pp. 275-294. doi: 10.1080/11663081.2012.705960.