Model Generation and State Generation for Disjunctive Logic Programs

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)