title: Double negation and execution model in Prolog
body: <p>I am trying to understand why Prolog implementations do not behave according to the execution model in textbooks -- for example, the one in the book by Sterling and Shapiro's "The Art of Prolog" (chapter 6, "Pure Prolog", section 6.1, "The Execution Model of Prolog"). </p>
  
  <p>The execution model to which I refer is this (page 93 of Sterling &amp; Shapiro):</p>
  
  <p><b>Input:</b> A goal G and a program P</p>
  
  <p><b>Output:</b> An instance of G that is a logical consequence of P, or no otherwise</p>
  
  <p><b>Algorithm:</b></p>
  
  <pre><code>Initialize resolvent to the goal G
  while resolvent not empty:
      choose goal A from resolvent
      choose renamed clause A' &lt;- B_1, ..., B_n from P
              such that A, A' unify with mgu θ
          (if no such goal and clause exist, exit the "while" loop)
      replace A by B_1, ..., B_n in resolvent
      apply θ to resolvent and to G
  If resolvent empty, then output G, else output NO
  </code></pre>
  
  <p>Additionally (page 120 of the same book), Prolog chooses goals (<code>choose goal A</code>) in left-to-right order, and searches clauses (<code>choose renamed clause ...</code>) in the order they show up in the program.</p>
  
  <p>The program below has a definition of <code>not</code> (called <code>n</code> in the program) and one single fact.</p>
  
  <pre><code>n(X) :- X, !, fail.
  n(X).
  
  f(a).
  </code></pre>
  
  <p>If I try to prove <code>n(n(f(X)))</code>, it succeeds (according to two textbooks and also on SWI Prolog, GNU Prolog and Yap). But isn't this a bit strange? According to that execution model, which several books expose, this is what I would expect to happen (skipping renaming of variables to keep things simple, since there would be no conflict anyway):</p>
  
  <ul>
  <li><p>RESOLVENT: <code>n(n(f(Z)))</code></p></li>
  <li><p>unification matches <code>X</code> in first clause with <code>n(f(Z))</code>, and replaces the goal with the tail of that clause.</p></li>
  <li><p>RESOLVENT: <code>n(f(Z)), !, fail</code>.</p></li>
  <li><p>unification matches again <code>X</code> in the first clause with <code>f(Z)</code>, and replaces the first goal in the resolvent with the tail of the clause</p></li>
  <li><p>RESOLVENT: <code>f(Z), !, fail, !, fail</code>.</p></li>
  <li><p>unification matches <code>f(Z)</code> -> success! Now this is eliminated from the resolvent.</p></li>
  <li><p>RESOLVENT: <code>!, fail, !, fail</code>.</p></li>
  </ul>
  
  <p>And "<code>!, fail, !, fail</code>" should <em>not</em> succeed! After the cut there is a fail. End of story. (And indeed, entering <code>!,fail,!,fail</code> as a query will fail in all Prolog systems that I have access to).</p>
  
  <p>So may I presume that the execution model in textbooks is not precisely what Prolog uses?</p>
  
  <p><strong>edit</strong>: changing the first clause to <code>n(X) :- call(X), !, fail</code> makes no difference in all Prologs I tried.</p>