Quite recently Brass/Dix have introduced the semantics D-WFS for general disjunctive logic programs. The interesting feature of this approach is that it is both semantically and proof-theoretically founded. Any program Φ is associated a normal form res(Φ), called the residual program, by a non-trivial bottom-up construction using least fixpoints of two monotonic operators.
We show in this paper, that the original calculus, consisting of some simple transformations, has a very strong and appealing property: it is confluent. This means that all the transformations can be applied in any order: if we arrive at an irreducible program (no more transformation is applicable) then this is already the unique normal form. No proper subset of the calculus has this property.
We also give an equivalent characterization of D-WPS in terms of iterated minimal model reasoning. This construction is a generalization of a description of the wellfounded semantics: we introduce a very simple and neat construction of a sequence D i that eventually stops and represents the set of derivable disjunctions.
Both characterizations open the way for efficient implementations. The first because the ordering of the transformations does not matter, the second because special methods from Circumscription might be useful.