Logic Journal of IGPL Advance Access originally published online on October 29, 2007
Logic Journal of IGPL 2008 16(2):175-193; doi:10.1093/jigpal/jzm059
| ||||||||||||||||||||||||||||||||||||||||||||||||
Constructing Finite Least Kripke Models for Positive Logic Programs in Serial Regular Grammar Logics
Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland. E-mail: nguyen{at}mimuw.edu.pl
| 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 model M is less than or equal to model M' if for every positive formula
, if M
then M'
.) 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(n3). 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
(n). 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.
Key Words: modal logic Horn logic model construction
Received for publication 25 November 2006.
![]()
CiteULike
Connotea
Del.icio.us What's this?