Constructing Finite Least Kripke Models for Positive Logic Programs in Serial Regular Grammar Logics

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