Negation 

Example: true cousin defined as follows:

  cousin(X,Y) :- parent(X,Xp), parent(Y,Yp), sibling(Xp,Yp).
  cousin(X,Y) :- parent(X,Xp), parent(Y,Yp), cousin(Xp,Yp).

  firstCousin(X,Y) :- parent(X,Xp), parent(Y,Yp), sibling(Xp,Yp).

  farCousin(X,Y) :- cousin(X,Y), not firstCousin(X,Y).

  FARCOUSIN = (select * from COUSIN) minus (select * from FIRSTCOUSIN)
 
Introducing Negation in rule bodies causes several problems:

(1) Rules that are not safe! i.e. variables appear only in negated goals.

    bachelor(X) :- male(X), not married(X,Y).

    Seems like a correct rule. Not so. Semantic problems! RHS describes males
    who are not married to EVERYBODY in the universe.

    Solution: Make the rule safe.

    husband(X) :- married(X,Y).
    bachelor(X) :- male(X), not husband(X).

    HUSBAND(PERSON) = select MSPOUSE from MARRIED;
    BACHELOR(PERSON) = (select PERSON from MALE) 
                        minus 
                       (select PERSON from HUSBAND)

(2) Too few variables in negated goal!

    canBuy(X,Y) :- likes(X,Y), not broke(X).

    complement of BROKE relation may be infinite!

    rewrite rules as follows:

    liked(Y) :- likes(X,Y).
    brokedPair(X,Y) :- broke(X), liked(Y).
    canBuy(X,Y) :- likes(X,Y), not brokedPair(X,Y).

(3) More serious problem: We now have more than one minimal model! So, which 
    one to use to answer queries?


    r(1).
    p(X) :- r(X), not q(X).
    q(X) :- r(X), not p(X).

    minimal model 1: { r(1), p(1) }
    minimal model 2: { r(1), q(1) }

   Another example:

    r(0,0).
    r(1,0).
    p(X) :- r(Y,X).
    q(X) :- r(X,Y), not p(X).  

    Minimal Models:

      M1 = { r(0,0), r(1,0), p(0), q(1) }
      M2 = { r(0,0), r(1,0), p(0), p(1) }
          
Example:
  p(X,Y) :- b(X,Y).
  p(X,Y) :- b(X,Z), p(Z,Y).
  e(X,Y) :- g(X,Y), not p(X,Y).
  a(X,Y) :- e(X,Y).
  a(X,Y) :- e(X,Z), a(Z,Y).
  b(1,2).
  b(2,1).
  b(3,4).
  b(4,3).
  g(2,3).
  g(3,2).

Example:
  murderer(X) :- ingarden(X), suspect(X).
  ingarden(X) :- not inhouse(X).
  ingarden(dale) :- not ingarden(peter).
  inhouse(jessica).
  suspect(jessica).
  suspect(dale).
  suspect(peter).


Stratification Computation:
---------------------------

for each predicate p do
  stratum[p] = 1;
repeat
  for each rule r with head predicate p do {
    for each negated subgoal of r with predicate q do
      stratum[p] = max(stratum[p],1+stratum[q]);
    for each non-negated subgoal of r with predicate q do
      stratum[p] = max(stratum[p],stratum[q]); 
  }
until there are no changes to any stratum or some
      stratum exceeds the number of predicates

Example
-------
link(milano,genova).
link(milano,torino).
link(torino,genova).
link(milano,venezia).

cutpoint(X,A,B) :- connected(A,B), station(X), not circumvent(X,A,B).

circumvent(X,A,B) :- linked(A,B), X <> A, X <> B.
circumvent(X,A,B) :- circumvent(X,A,C), circumvent(X,C,B).

linked(A,B) :- link(A,B).
linked(A,B) :- link(B,A).

connected(A,B) :- linked(A,B).
connected(A,B) :- connected(A,C), linked(C,B).

existscutpoint(A,B) :- station(X), cutpoint(X,A,B).

safely-connected(A,B) :- connected(A,B), not existscutpoint(A,B).

station(X) :- linked(X,Y).

Non-stratified Negation
-----------------------
Consider the database:

move(a,b).
move(b,c).
win(X) :- move(X,Y), not win(Y).

The two minimal models are:

M1 = { move(a,b), move(b,c), win(a), win(c) }
M2 = { move(a,b), move(b,c), win(b) }

This database is not stratified; But there is an intuitive minimal model (M2).

Consider all ground instances of the rule:

win(a) :- move(a,a), not win(a).
win(a) :- move(a,b), not win(b).
win(a) :- move(a,c), not win(c).

win(b) :- move(b,a), not win(a).
win(b) :- move(b,b), not win(b).
win(b) :- move(b,c), not win(c).

win(c) :- move(c,a), not win(a).
win(c) :- move(c,b), not win(b).
win(c) :- move(c,c), not win(c).

All three ground instances which prove win(c) are USELESS! since 
at least one of their sub-goals is false. Which leads us to conclude that
win(c) must be false.

Once win(c) is determined to be false, win(b) can be determined to be true
using the third ground instance for win(b). win(a) can then be determined
to be false since all three ground instances for win(a) now have at least one
sub-goal false.

Hence, M2 is the intuitive minimal model.