title: Prolog: why is true == not(not(true)) -> false?
body: <p>Obviously <code>true = not(not(true))</code> has to be false, because <code>=</code> tries to unify the atom <code>true</code> with the term <code>not(not(true))</code> (without evaluating the term), which is false, since the terms are not identical.</p>
  
  <p>However, I thought <code>==</code> really compares whatever is evaluated. Thus, I thought <code>true == not(not(true))</code> should evaluate to <code>true == true</code>, just like (for arithmetic operators) <code>4 =:= 2 + 2</code> would evaluate to <code>4 =:= 4</code> and return true.</p>
  
  <p>...but this is what I get in SWI-Prolog:</p>
  
  <pre><code>?- true == not(not(true)).
  false.
  </code></pre>
  
  <p>What am I getting wrong?</p>