On the Computation of the Disjunctive Well-Founded Semantics

A characterization of the disjunctive well-founded semantics (DWFS) is given in terms of the Gelfond–Lifschitz transformation. This characterization is used to develop a top-down method of testing DWFS membership, employing a hyperresolution-like operator and quasi-cyclic trees to handle minimal model processing. A flexible bottom-up method of computing the DWFS is also given that admits the use of a powerful reduction operator. For finite propositional databases, all of our methods run in polynomial space.