title: Datalog Stratification
body: <p>So I'm trying to understand how Datalog works and one of the differences between it and Prolog is that it has stratification limitations placed upon negation and recursion. 
  To quote Wikipedia:</p>
  
  <blockquote>
    <p>If a predicate P is positively derived from a predicate Q (i.e., P is
    the head of a rule, and Q occurs positively in the body of the same
    rule), then the stratification number of P must be greater than or
    equal to the stratification number of Q</p>
    
    <p>If a predicate P is derived from a negated predicate Q (i.e., P is the
    head of a rule, and Q occurs negatively in the body of the same rule),
    then the stratification number of P must be greater than the
    stratification number of Q,</p>
  </blockquote>
  
  <p>So, going by this, the two following predicates do not result in a stratification error as they can simply be assigned the same stratification number. So these predicates are fine, despite the circular definition.</p>
  
  <ol>
  <li>A(x) :- B(x)</li>
  <li>B(x) :- A(x)</li>
  </ol>
  
  <p>But contrast that with what happens if we have a definition which has some negation involved (Where ~ is negation)</p>
  
  <ol>
  <li>A(x) :- ~ B(x)</li>
  <li>B(x) :- ~ A(x)</li>
  </ol>
  
  <p>Here a stratification is impossible. A(x,y) must have a stratification number greater than B(x,y), and B(x,y) must have a stratification number greater than A(x,y).  My first thought was that this was not okay because this is a circular definition, but stratification is fine with circularity so long as the predicates are not negated. But why? Truth values are simply binary. It seems extremely arbitrary to treat formulas which have a negation symbol differently in this manner. What is this stratification trying to prevent in the second case which isn't in the first? </p>