A fixpoint semantics for disjunctive logic programs

AbstractWe present a fixpoint semantics for disjunctive logic programs. We extend the concept of the Herbrand base of a logic program to consist of all positive clauses that may be formed using the atoms in the Herbrand base. A monotonic closure operator is defined, operating on the lattice formed by the power set of the extended Herbrand base. The closure operator is shown to achieve a least fixpoint which captures the intended meaning of derivability of disjunctive programs. The equivalence of the fixpoint semantics with the minimal model semantics is also shown. We provide a characterization for Minker's generalized closed-world assumption using the fixpoint operator. We introduce the concept of support for negation and develop a proof procedure for handling negation based on this concept. We describe a proof procedure based on SLINF derivation, a modification of SLI derivation (LUST resolution). We show that the proof procedure reduces to SLDNF resolution when applied to Horn programs