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.