The family of stable models

AbstractThe family of all stable models for a logic program has a surprisingly simple overall structure, once two naturally occuring orderings are made explicit. In a so-called knowledge ordering based on degree of definedless, every logic program P has a smallest stable model skP—it is the well-founded model. There is also a dual largest stable model SkP, which has not been considered before. There is another ordering based on degree of truth. Taking the meet and the join, in the truth ordering, of the two extreme stable models skP and SkP just mentioned yields the alternating fixed points of Van Gelder, denoted stP and StP here. From stP and StP in turn, skP and SkP can be produced again, using the meet and joint of the knowledge ordering. All stable models are bounded by these four valuations. Further, the methods of proof apply not just to logic programs considered classically, but to logic programs over any bilattice meeting certain conditions, and thus apply in a vast range of settings. The methods of proof are largely algebraic