A new fixpoint semantics for general logic programs compared with the well-founded and the stable model semantics

We study a new fixpoint semantics for logic programs with negation. Our construction is intermediate between Van Gelder's well-founded model and Gelfond and Lifschitz's stable model semantics. We show first that the stable models of a logic program P are exactly the well-supported models of P, i.e. the supported models with loop-free finite justifications. Then we associate to any logic program P a non-monotonic operator over the semilattice of justified interpretations, and we define in an abstract form its ordinal powers. We show that the fixpoints of this operator are the stable models of P, and that its ordinal powers after some ordinal a are extensions of the well-founded partial model of P. In particular if P has a well-founded model then that canonical model is also an ordinal power and the unique fixpoint of our operator. We show with examples of logic programs which have a unique stable model but no well-founded model that the converse is false. We relate also our work to Doyle's truth maintenance system and some implementations of rule-based expert systems.