Constructing Finite Least Kripke Models for Positive Logic Programs in Serial Regular Grammar Logics |
| |
Authors: | Nguyen Linh Anh |
| |
Institution: | 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 logicL characterized by the seriality axioms and a set of inclusionaxioms of the form t![{varphi}](http://jigpal.oxfordjournals.org/math/phiv.gif) ![->](http://jigpal.oxfordjournals.org/math/rarr.gif) s1... sk . Such an inclusion axiom correspondsto the grammar rule t s1... sk. Thus the inclusion axioms ofL capture a context-free grammar . If for every modal index t, the set of words derivable fromt using is a regular language, then L is a serial regular grammar logic. In this paper, we present an algorithm that, given a positivemultimodal logic program P and a set of finite automata specifyinga serial regular grammar logic L, constructs a finite leastL-model of P. (A model M is less than or equal to model M' iffor every positive formula , if M then M' .) A least L-modelM of P has the property that for every positive formula , P iff M . The algorithm runs in exponential time and returnsa model with size 2O(n3). We give examples of P and L, for bothof the case when L is fixed or P is fixed, such that every finiteleast L-model of P must have size 2 (n). We also prove that ifG is a context-free grammar and L is the serial grammar logiccorresponding to G then there exists a finite least L-modelof s p iff the set of words derivable from s using G is a regularlanguage. |
| |
Keywords: | modal logic Horn logic model construction |
本文献已被 Oxford 等数据库收录! |
|