Model Generation and State Generation for Disjunctive Logic Programs
Model Generation and State Generation for Disjunctive Logic Programs
Files
Publication or External Link
Date
1998-10-15
Authors
Seipel, Dietmar
Minker, Jack
Ruiz, Carolina
Advisor
Citation
DRUM DOI
Abstract
This paper investigates two fixpoint approaches for minimal model
reasoning with disjunctive logic programs DB. The first one, called
model generation [4], is based on an operator TI defined on sets of
Herbrand interpretations, whose least fixpoint is logically equivalent
to the set of minimal Herbrand models of the program. The second
approach, called state generation [12], uses a fixpoint operator TS
based on hyperresolution. It operates on disjunctive Herbrand states
and its least fixpoint is the set of logical consequences of DB, the
so--called minimal model state of the program.
We establish a useful relationship between hyperresolution by TS and
model generation by TI. Then we investigate the problem of continuity
of the two operators TS and TI. It is known that the operator TS is
continuous [12], and so it reaches its least fixpoint in at most omega
steps. On the other hand, the question of whether TI is continuous has
been open. We show by a counterexample that TI is not continuous.
Nevertheless, we prove that it converges towards its least fixpoint in
at most omega steps too, as follows from the relationship that we show
exists between hyperresolution and model generation.
We define an iterative version of TI that computes the perfect model
semantics of stratified disjunctive logic programs. On each stratum of
the program, this operator converges in at most omega steps. Model
generations for the stable semantics and the partial stable (and so the
well--founded semantics) are respectively achieved by using this
iterative operator together with the evidential transformation [3] and
the 3-S transformation [16].
(Also cross-referenced as UMIACS-TR-95-99)