208 III. PROLOG ? Negation and Nonmonotonic Logic 209 p(l,2). <|C1) :- p(l,l),-*?(l). 9(1) :p(l,2),~^(2). d(2) :- p(2,l),-ng(l). f(2) :- p(2,2),-«(2). We now consider the subset M ~ {«(1)} of the Herbrand universe. Pm is then p(l,2). «(D :P(l,2). «(2) :p(2,2). The minimal Herbrand model of PM is {p(l,2),g(l)} ^ Af. Thus, M is not a stable model of P. Indeed, any set M not containing p(L 2) is not a model of P and so by Theorem 7.9 not a stable model of P. Next, we consider the two minimal Herbrand models Mi and M% of the original program Q, We claim that M, is stable but not My,. First. pMt is p(l,2). 9(1) P(l,2). 9(2) :p(2,2). The minimal model of this program is clearly Mi which is therefore stable. On the other hand, Pm2 is p(l,2). «(1) :P(l,l)-g(2) p(2,l). Its minimal model is {p(l,2)} yi M2. Thus M2 is not stable. In fact, Mi is the only stable model of P (Exercise 7) and so the stable mode! is the "right" one from the viewpoint of negation as failure. A direct and precise connection of stable mo * * terns is provided by the Theorem 7.12. We co above and begin with a lemma. Lemma 7.11: If M' is a model ofPM, then M' \ Proof; Suppose that M' is a model of PM. We \ M-deductions that every member of t7M(i M-deduction spi,(pu,p (bom 0) and sup; of this deduction to conclude p is ir(C) for we may assume that • • •. -Jk is one of the Theorem 7,12: A subset M ofU is a stable model oftr(P). Proo required. □ Gelfond and Lifschitz show that certain classes of programs with properties such as those considered in §4 have unique stable models arid propose the term stable model semantics for such programs. The special ease of a unique stable model is certainly of particular interest. Rrom the viewpoint of nonmonotonic logic, however, all the extensions of tr(P) are equally good candidates for models of the system. Exercises 1, Let S'i D ,5*2 D ... be a nested sequence of deductively closed sets for a 2. A version of Zona's lemma (see Theorem VI.10.2 and Exercise ¥1.10.21 3. Prove that the operation Cs(l) is monotonic in I and antimonotonic in S, that is if I C J, then CS{I) C CS(J) and if S C T, then CS(I) 2 CT(I). 4. Prove that, if S is an extension of I, then S is a minimal deductively closed superset of I and for every J such that I C J C S we have Cs(J) — S.