Abstract

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