part_i.html

---
layout: paper
part: Part I
---
<div class="WordSection1">
 <p class="romeinscijfer" id="logic_and_logic_programming">
  I
 </p>
 <div class="AutoStyle00">
  <h1 class="AutoStyle01" id="h_logic_and_logic_programming">
   Logic and<br>
   Logic Programming
</h1>
 </div>
 <p class="sektie1">
  <i>Logic Programming</i> is the name of a programming paradigm which was developed in the 70s. Rather than viewing a computer program as a step-by-step description of an algorithm, the program is conceived as a logical theory, and a procedure call is viewed as a theorem of which the truth needs to be established. Thus, executing a program means searching for a proof. In traditional (imperative) programming languages, the program is a <i>procedural</i> specification of <b>how</b> a problem needs to be solved. In contrast, a logic program concentrates on a <i>declarative</i> specification of <b>what</b> the problem is. Readers familiar with imperative programming will find that Logic Programming requires quite a different way of thinking. Indeed, their knowledge of the imperative paradigm will be partly incompatible with the logic paradigm.
 </p>
 <p class="sektie">
  This is certainly true with regard to the concept of a program <i>variable</i>. In imperative languages, a variable is a name for a memory location which can store data of certain types. While the contents of the location may vary over time, the variable always points to the same location. In fact, the term &lsquo;variable&rsquo; is a bit of a misnomer here, since it refers to a value that is well-defined at every moment. In contrast, a variable in a logic program is a variable in the mathematical sense, i.e. a placeholder that can take on any value. In this respect, Logic Programming is therefore much closer to mathematical intuition than imperative programming.
 </p>
 <p class="sektie">
  Imperative programming and Logic Programming also differ with respect to the <i>machine model</i> they assume. A machine model is an abstraction of the computer on which programs are executed. The imperative paradigm assumes a dynamic, state-based machine model, where the state of the computer is given by the contents of its memory. The effect of a program statement is a transition from one state to another. Logic Programming does not assume such a dynamic machine model. Computer plus program represent a certain amount of knowledge about the world, which is used to answer queries.
 </p>
 <p class="sektie">
  The first three chapters of the book are devoted to an introduction to Logic Programming. Chapter 1, <i>A brief introduction to clausal logic</i>, is an introductory chapter, introducing many concepts in Logic Programming by means of examples. These concepts get a more formal treatment in Chapter 2, <i>Clausal logic and resolution: theoretical backgrounds</i>. In Chapter 3, <i>Logic Programming and Prolog</i>, we take a closer look at Prolog as a logic programming language, explaining its main features and describing some common programming techniques.
 </p>
</div>
<b>
 <span class="AutoStyle02">
  <br clear="all"/>
 </span>
</b>
<div class="WordSection2">
 <p class="cijfer" id="a_brief_introduction_to_clausal_logic">
  1
 </p>
 <h2 id="h_a_brief_introduction_to_clausal_logic">
  A brief introduction to clausal logic
 </h2>
 <p class="sektie1">
  In this chapter, we will introduce clausal logic as a formalism for representing and reasoning with knowledge. The aim of this chapter is to acquaint the reader with the most important concepts, without going into too much detail. The theoretical aspects of clausal logic, and the practical aspects of Logic Programming, will be discussed in Chapters 2 and 3.
 </p>
 <p class="sektie">
  Our Universe of Discourse&nbsp;in this chapter will be the London Underground, of which a small part is shown in fig. 1.1. Note that this picture contains a wealth of information, about lines, stations, transit between lines, relative distance, etc. We will try to capture this information in logical statements. Basically, fig. 1.1 specifies which stations are directly connected by which lines. If we follow the lines from left to right (Northern downwards), we come up with the following 11 formulas:
 </p>

<div class="extract swish" id="1.0.1">
<pre class="source swish temp AutoStyle03" data-variant-id="group-1" id="swish.1.0.1" query-text="?-connected(bond_street,Y,L). ?-connected(X,piccadilly_circus,L). ?-connected(X,Y,piccadilly). ?-connected(X,Y,L),connected(Y,Z,L).">
connected(bond_street,oxford_circus,central).
connected(oxford_circus,tottenham_court_road,central).
connected(bond_street,green_park,jubilee).
connected(green_park,charing_cross,jubilee).
connected(green_park,piccadilly_circus,piccadilly).
connected(piccadilly_circus,leicester_square,piccadilly).
connected(green_park,oxford_circus,victoria).
connected(oxford_circus,piccadilly_circus,bakerloo).
connected(piccadilly_circus,charing_cross,bakerloo).
connected(tottenham_court_road,leicester_square,northern).
connected(leicester_square,charing_cross,northern).
</pre>
</div>

 <p class="tekst">
  Let&rsquo;s define two stations to be <i>nearby</i> if they are on the same line, with at most one station in between. This relation can also be represented by a set of logical formulas:
 </p>

<div class="extract swish" id="1.0.2">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.1.0.2" query-text="?-nearby(bond_street,Y). ?-nearby(X,piccadilly_circus). ?-nearby(X,Y). ?-nearby(X,Y),nearby(Y,Z).">
nearby(bond_street,oxford_circus).
nearby(oxford_circus,tottenham_court_road).
nearby(bond_street,tottenham_court_road).
nearby(bond_street,green_park).
nearby(green_park,charing_cross).
nearby(bond_street,charing_cross).
nearby(green_park,piccadilly_circus).
nearby(piccadilly_circus,leicester_square).
nearby(green_park,leicester_square).
nearby(green_park,oxford_circus).
nearby(oxford_circus,piccadilly_circus).
nearby(piccadilly_circus,charing_cross).
nearby(oxford_circus,charing_cross).
nearby(tottenham_court_road,leicester_square).
nearby(leicester_square,charing_cross).
nearby(tottenham_court_road,charing_cross).
</pre>
</div>

 <div class="extract figure" id="1.1">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle05">
       <p class="figure">
        <img src="img/part_i/image002.svg" v:shapes="_x0000_i1025" width="100%"/>
       </p>
      </div>
      <p class="caption">
       <b>Figure 1.1.</b> Part   of the London Underground. Reproduced by permission of London Regional   Transport (LRT Registered User No. 94/1954).
      </p>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="tekst">
  These 16 formulas have been derived from the previous 11 formulas in a systematic way. If <i>X</i> and <i>Y</i> are directly connected via some line <i>L</i>, then <i>X</i> and <i>Y</i> are nearby. Alternatively, if there is some <i>Z</i> in between, such that <i>X</i> and <i>Z</i> are directly connected via <i>L</i>, and <i>Z</i> and <i>Y</i> are also directly connected via <i>L</i>, then <i>X</i> and <i>Y</i> are also nearby. We can formulate this in logic as follows:
 </p>

<div class="extract swish" id="1.0.3">
<pre class="source swish inherit temp AutoStyle03" data-variant-id="group-1" id="swish.1.0.3" inherit-id="swish.1.0.1" query-text="?-nearby(tottenham_court_road,leicester_square). ?-nearby(tottenham_court_road,W). ?-nearby(X,leicester_square).">
nearby(X,Y):-connected(X,Y,L).
nearby(X,Y):-connected(X,Z,L),connected(Z,Y,L).
</pre>
</div>

 <p class="tekst">
  In these formulas, the symbol &lsquo; <tt>:-</tt> &rsquo; should be read as &lsquo;if&rsquo;, and the comma between <tt>connected(X,Z,L)</tt> and <tt>connected(Z,Y,L)</tt> should be read as &lsquo;and&rsquo;. The uppercase letters stand for universally quantified variables, such that, for instance, the second formula means:
 </p>
 <p class="citaat">
  <b>For any values</b> of <i>X</i>, <i>Y</i>, <i>Z</i> and <i>L</i>, <i>X</i> is nearby <i>Y</i> <b>if</b> <i>X</i> is directly connected to Z via L, <b>and</b> Z is directly connected to Y via L.
 </p>
 <p class="sektie">
  We now have two definitions of the nearby-relation, one which simply lists all pairs of stations that are nearby each other, and one in terms of direct connections. Logical formulas of the first type, such as
 </p>
 <p class="p-el">
  nearby(bond_street,oxford_circus)
 </p>
 <p class="tekst">
  will be called <i>facts</i>, and formulas of the second type, such as
 </p>
 <p class="p-el">
  nearby(X,Y):-connected(X,Z,L),connected(Z,Y,L)
 </p>
 <p class="tekst">
  will be called <i>rules</i>. Facts express unconditional truths, while rules denote conditional truths, i.e. conclusions which can only be drawn when the premises are known to be true. Obviously, we want these two definitions to be <i>equivalent</i>: for each possible query, both definitions should give exactly the same answer. We will make this more precise in the next section.
 </p>
<div class="extract exercise" id="1.1">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 1.1.</i> Two stations are &lsquo;not too far&rsquo; if they are on the same or a different line, with at most one station in between. Define rules for the predicate <tt>not_too_far</tt>.
  </p>

<div class="extract swish" id="1.0.4">
<pre class="source swish inherit AutoStyle08" data-variant-id="group-1" id="swish.1.0.4" inherit-id="swish.1.0.1" query-text="?-not_too_far(X,Y).">
not_too_far(X,Y):-true. % replace 'true' with your definition
not_too_far(X,Y):-true. % add more clauses as needed
</pre>
</div>

 </div>
</div>
 <h3 id="answering_queries">
  1.1&nbsp;&nbsp;&nbsp;Answering queries
 </h3>
 <p class="sektie1">
  A <i>query</i>&nbsp;like &lsquo;which station is nearby Tottenham Court Road?&rsquo; will be written as
 </p>
 <p class="p-el">
  ?-nearby(tottenham_court_road,W).
 </p>
</div>
<p class="tekst">
 where the prefix &lsquo; <tt>?-</tt> &rsquo; indicates that this is a query rather than a fact. An <i>answer</i>&nbsp;to this query, e.g. &lsquo;Leicester Square&rsquo;, will be written { <tt>W</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>leicester_square</tt> }, indicating a <i>substitution</i>&nbsp;of values for variables, such that the statement in the query, i.e.
</p>
<p class="p-el">
 ?-nearby(tottenham_court_road,leicester_square).
</p>
<p class="tekst">
 is true. Now, if the nearby-relation is defined by means of a list of facts, answers to queries are easily found: just look for a fact that <i>matches</i> the query, by which is meant that the fact and the query can be made identical by substituting values for variables in the query. Once we have found such a fact, we also have the substitution which constitutes the answer to the query.
</p>
<p class="sektie">
 If rules are involved, query-answering can take several of these steps. For answering the query <tt>?-nearby(tottenham_court_road,W)</tt>, we match it with the conclusion of the rule
</p>
<p class="p-el">
 nearby(X,Y):-connected(X,Y,L)
</p>
<p class="tekst">
 yielding the substitution { <tt>X</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>tottenham_court_road</tt>, <tt>Y</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>W</tt> }. We then try to find an answer for the premises of the rule under this substitution, i.e. we try to answer the query
</p>
<p class="p-el">
 ?-connected(tottenham_court_road,W,L).
</p>
<p class="tekst">
 That is, we can find a station nearby Tottenham Court Road, if we can find a station directly connected to it. This second query is answered by looking at the facts for direct connections, giving the answer { <tt>W</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>leicester_square</tt>, <tt>L</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>northern</tt> }. Finally, since the variable <tt>L</tt> does not occur in the initial query, we just ignore it in the final answer, which becomes { <tt>W</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>leicester_square</tt> } as above. In fig. 1.2, we give a graphical representation of this process. Since we are essentially <i>proving</i> that a statement follows logically from some other statements, this graphical representation is called a <i>proof tree</i>.
</p>
<div class="extract figure" id="1.2">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle05">
      <p class="figure">
       <img src="img/part_i/image004.svg" v:shapes="_x0000_i1026" width="100%"/>
      </p>
     </div>
     <p class="caption">
      <b>Figure 1.2.</b> A   proof tree for the query <tt>?-nearby(tottenham_court_road,W)</tt>.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="sektie">
 The steps in fig. 1.2 follow a very general reasoning pattern:
</p>
<p class="citaat">
 to answer a query <tt>?-</tt> <i>Q</i>
 <span class="AutoStyle10">
  1
 </span>
 <tt>,</tt> <i>Q</i>
 <span class="AutoStyle10">
  2
 </span>
 <tt>,</tt> &hellip; <tt>,</tt> <i>Q<span class="AutoStyle10">
   n
  </span></i>, find a rule <i>A</i> <tt>:-</tt> <i>B</i>
 <span class="AutoStyle10">
  1
 </span>
 <tt>,</tt> &hellip; <tt>,</tt> <i>B<span class="AutoStyle10">
   m
  </span></i>&nbsp;such that <i>A</i> matches with <i>Q</i>
 <span class="AutoStyle10">
  1
 </span>
 , and answer the query <tt>?-</tt> <i>B</i>
 <span class="AutoStyle10">
  1
 </span>
 <tt>,</tt> &hellip; <tt>,</tt> <i>B<span class="AutoStyle10">
   m
  </span></i> <tt>,</tt> <i>Q</i>
 <span class="AutoStyle10">
  2
 </span>
 <tt>,</tt> &hellip; <tt>,</tt> <i>Q<span class="AutoStyle10">
   n
  </span></i>.
</p>
<p class="tekst">
 This reasoning pattern is called <i>resolution</i>, and we will study it extensively in Chapters 2 and 3. Resolution adds a <b>procedural interpretation</b>&nbsp;to logical formulas, besides their declarative interpretation&nbsp;(they can be either true or false). Due to this procedural interpretation, logic can be used as a programming language. In an ideal logic programming system, the procedural interpretation would exactly match the declarative interpretation: everything that is calculated procedurally is declaratively true, and <i>vice versa</i>. In such an ideal system, the programmer would just bother about the declarative interpretation of the formulas she writes down, and leave the procedural interpretation to the computer. Unfortunately, in current logic programming systems the procedural interpretation does <b>not</b> exactly match the declarative interpretation: for example, some things that are declaratively true are not calculated at all, because the system enters an infinite loop. Therefore, the programmer should also be aware of the procedural interpretation given by the computer to her logical formulas.
</p>
<p class="sektie">
 The resolution proof process makes use of a technique that is known as <i>reduction to the absurd</i>: suppose that the formula to be proved is false, and show that this leads to a contradiction, thereby demonstrating that the formula to be proved is in fact true. Such a proof is also called a <i>proof by refutation</i>. For instance, if we want to know which stations are nearby Tottenham Court Road, we negate this statement, resulting in &lsquo;there are no stations nearby Tottenham Court Road&rsquo;. In logic, this is achieved by writing the statement as a rule with an empty conclusion, i.e. a rule for which the truth of its premises would lead to falsity:
</p>
<p class="p-el">
 :-nearby(tottenham_court_road,W)
</p>
<p class="tekst">
 Thus, the symbols &lsquo; <tt>?-</tt> &rsquo; and &lsquo; <tt>:-</tt> &rsquo; are in fact equivalent. A contradiction is found if resolution leads to the empty rule, of which the premises are always true (since there are none), but the conclusion is always false. Conventionally, the empty rule is written as &lsquo;
 <span class="AutoStyle11">
  □
 </span>
 &rsquo;.
</p>
<p class="sektie">
 At the beginning of this section, we posed the question: can we show that our two definitions of the nearby-relation are equivalent? As indicated before, the idea is that to be equivalent means to provide exactly the same answers to the same queries. To formalise this, we need some additional definitions. A <i>ground</i> fact&nbsp;is a fact without variables. Obviously, if <tt>G</tt> is a ground fact, the query <tt>?-G</tt> never returns a substitution as answer: either it <i>succeeds</i> (<tt>G</tt> does follow from the initial assumptions), or it <i>fails</i> (<tt>G</tt> does not). The set of ground facts <tt>G</tt> for which the query <tt>?-G</tt> succeeds is called the <i>success set</i>.&nbsp;Thus, the success set for our first definition of the nearby-relation consists simply of those 16 formulas, since they are ground facts already, and nothing else is derivable from them. The success set for the second definition of the nearby-relation is constructed by applying the two rules to the ground facts for connectedness. Thus we can say: two definitions of a relation are (procedurally) <i>equivalent</i> if they have the same success set (restricted to that relation).
</p>
<div class="extract exercise" id="1.2">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 1.2.</i> Construct the proof trees for the query<br>
  &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<tt>?-nearby(W,charing_cross)</tt>.
</p>
</div>
</div>
<h3 id="recursion">
 1.2&nbsp;&nbsp;&nbsp;Recursion
</h3>
<p class="sektie1">
 Until now, we have encountered two types of logical formulas: facts and rules. There is a special kind of rule which deserves special attention: the rule which defines a relation in terms of itself. This idea of &lsquo;self-reference&rsquo;, which is called <i>recursion</i>, is also present in most procedural programming languages. Recursion is a bit difficult to grasp, but once you&rsquo;ve mastered it, you can use it to write very elegant programs, e.g.
</p>
<p class="p-el">
 <span class="AutoStyle12">
  IF N=0<br>
  THEN FAC:=1<br>
  ELSE FAC:=N*FAC(N-1).
</span>
</p>
<p class="tekst">
 is a recursive procedure for calculating the factorial of a given number, written in a Pascal-like procedural language. However, in such languages <i>iteration</i>&nbsp;(looping a pre-specified number of times) is usually preferred over recursion, because it uses memory more efficiently.
</p>
<p class="sektie">
 In Prolog, however, recursion is the <b>only</b> looping structure
 <span class="CustomFootnote">
  <a href="#_ftn1" name="_ftnref1" title="">
   <span class="MsoFootnoteReference">
    <span class="AutoStyle13">
     <span class="AutoStyle14">
      [1]
     </span>
    </span>
   </span>
  </a>
 </span>
 . (This does not necessarily mean that Prolog is always less efficient than a procedural language, because there are ways to write recursive loops that are just as efficient as iterative loops, as we will see in section 3.6.) Perhaps the easiest way to think about recursion is the following: an arbitrarily large chain is described by describing how one link in the chain is connected to the next. For instance, let us define the relation of <i>reachability</i> in our underground example, where a station is reachable from another station if they are connected by one or more lines. We could define it by the following 20 ground facts:
</p>

<div class="extract swish" id="1.1.1">
<pre class="source swish temp AutoStyle03" data-variant-id="group-1" id="swish.1.1.1" query-text="?-reachable(bond_street,Y). ?-reachable(X,green_park). ?-reachable(X,Y).">
reachable(bond_street,charing_cross).
reachable(bond_street,green_park).
reachable(bond_street,leicester_square).
reachable(bond_street,oxford_circus).
reachable(bond_street,piccadilly_circus).
reachable(bond_street,tottenham_court_road).
reachable(green_park,charing_cross).
reachable(green_park,leicester_square).
reachable(green_park,oxford_circus).
reachable(green_park,piccadilly_circus).
reachable(green_park,tottenham_court_road).
reachable(leicester_square,charing_cross).
reachable(oxford_circus,charing_cross).
reachable(oxford_circus,leicester_square).
reachable(oxford_circus,piccadilly_circus).
reachable(oxford_circus,tottenham_court_road).
reachable(piccadilly_circus,charing_cross).
reachable(piccadilly_circus,leicester_square).
reachable(tottenham_court_road,charing_cross).
reachable(tottenham_court_road,leicester_square).
</pre>
</div>

<p class="tekst">
 Since any station is reachable from any other station by a route with at most two intermediate stations, we could instead use the following (non-recursive) definition:
</p>
<p class="p-eerst AutoStyle15">
 reachable(X,Y):-connected(X,Y,L).
</p>
<p class="programma AutoStyle15">
 reachable(X,Y):-connected(X,Z,L1),connected(Z,Y,L2).
</p>
<p class="p-laatst AutoStyle15">
 reachable(X,Y):-connected(X,Z1,L1),connected(Z1,Z2,L2),<br>
 connected(Z2,Y,L3).
</p>
<p class="tekst">
 Of course, if we were to define the reachability relation for the entire London underground, we would need a lot more, longer and longer rules. Recursion is a much more convenient and natural way to define such chains of arbitrary length:
</p>

<div class="extract swish" id="1.1.2">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-1" id="swish.1.1.2" inherit-id="swish.1.0.1" query-text="?-reachable(bond_street,Y). ?-reachable(X,green_park). ?-reachable(X,Y).">
reachable(X,Y):-connected(X,Y,L).
reachable(X,Y):-connected(X,Z,L),reachable(Z,Y).
</pre>
</div>

<p class="tekst">
 The reading of the second rule is as follows: &lsquo; <i>Y</i> is reachable from <i>X</i> if <i>Z</i> is directly connected to <i>X</i> via line <i>L</i>, and <i>Y</i> is reachable from <i>Z</i> &rsquo;.
</p>
<div class="extract figure" id="1.3">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle05">
      <p class="figure">
       <img src="img/part_i/image006.svg" v:shapes="_x0000_i1027" width="100%"/>
      </p>
     </div>
     <p class="caption">
      <b>Figure 1.3.</b> A   proof tree for the query <tt>?-reachable(bond_street,W)</tt>.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="sektie">
 We can now use this recursive definition to prove that Leicester Square is reachable from Bond Street (fig. 1.3). However, just as there are several routes from Bond Street to Leicester Square, there are several alternative proofs of the fact that Leicester Square is reachable from Bond Street. An alternative proof is given in fig. 1.4. The difference between these two proofs is that in the first proof we use the fact
</p>
<p class="p-el">
 connected(oxford_circus,tottenham_court_road,central)
</p>
<p class="tekst">
 while in the second proof we use
</p>
<p class="p-el">
 connected(oxford_circus,piccadilly_circus,bakerloo)
</p>
<p class="tekst">
 There is no reason to prefer one over the other, but since Prolog searches the given formulas top-down, it will find the first proof before the second. Thus, the order of the clauses determines the order in which answers are found. As we will see in Chapter 3, it sometimes even determines whether any answers are found at all.
</p>
<div class="extract exercise" id="1.3">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 1.3.</i> Give a third proof tree for the answer { <tt>W</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>leicester_square</tt> }, and change the order of the facts for connectedness, such that this proof tree is constructed first.
 </p>
</div>
</div>
<div class="extract figure" id="1.4">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle05">
      <p class="figure">
       <img src="img/part_i/image008.svg" v:shapes="_x0000_i1028" width="100%"/>
      </p>
     </div>
     <p class="caption">
      <b>Figure 1.4.</b> Alternative proof tree for the query <tt>?-reachable(bond_street,W)</tt>.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="sektie">
 In other words, Prolog&rsquo;s query-answering process is a <i>search process</i>, in which the answer depends on all the choices made earlier. A important point is that some of these choices may lead to a dead-end later. For example, if the recursive formula for the reachability relation had been tried before the non-recursive one, the bottom part of fig. 1.3 would have been as in fig. 1.5. This proof tree cannot be completed, because there are no answers to the query <tt>?-reachable(charing_cross,W)</tt>, as can easily be checked. Prolog has to recover from this failure by climbing up the tree, reconsidering previous choices. This search process, which is called <i>backtracking</i>, will be detailed in Chapter 5.
</p>
<h3 id="structured_terms">
 1.3&nbsp;&nbsp;&nbsp;Structured terms
</h3>
<p class="sektie1">
 Finally, we illustrate the way Prolog can handle more complex datastructures, such as a list of stations representing a route. Suppose we want to redefine the reachability relation, such that it also specifies the intermediate stations. We could adapt the non-recursive definition of <tt>reachable</tt> as follows:
</p>
<p class="p-eerst AutoStyle16">
 reachable0(X,Y):-connected(X,Y,L).
</p>
<p class="programma AutoStyle17">
 reachable1(X,Y,Z):-connected(X,Z,L1),<br>
 connected(Z,Y,L2).
</p>
<p class="p-laatst AutoStyle18">
 reachable2(X,Y,Z1,Z2):-connected(X,Z1,L1),<br>
 connected(Z1,Z2,L2),<br>
 connected(Z2,Y,L3).
</p>
<p class="tekst">
 The suffix of reachable indicates the number of intermediate stations; it is added to stress that relations with different number of arguments are really different relations, even if their names are the same. The problem now is that we have to know the number of intermediate stations in advance, before we can ask the right query. This is, of course, unacceptable.
</p>
<div class="extract figure" id="1.5">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle05">
      <p class="figure">
       <img src="img/part_i/image010.svg" v:shapes="_x0000_i1029" width="100%"/>
      </p>
     </div>
     <p class="caption">
      <b>Figure 1.5.</b> A   failing proof tree.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="sektie">
 We can solve this problem by means of <i>functors</i>. A functor&nbsp;looks just like a mathematical function, but the important difference is that <i>functor expressions are never evaluated to determine a value</i>. Instead, they provide a way to name a complex object composed of simpler objects. For instance, a route with Oxford Circus and Tottenham Court Road as intermediate stations could be represented by
</p>
<p class="p-el">
 route(oxford_circus,tottenham_court_road)
</p>
<p class="tekst">
 Note that this is not a ground fact, but rather an argument for a logical formula. The reachability relation can now be defined as follows:
</p>

<div class="extract swish" id="1.2.1">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-1" id="swish.1.2.1" inherit-id="swish.1.0.1" query-text="?-reachable(oxford_circus,charing_cross,R).">
reachable(X,Y,noroute):-connected(X,Y,L).
reachable(X,Y,route(Z)):-connected(X,Z,L1),
                         connected(Z,Y,L2).
reachable(X,Y,route(Z1,Z2)):-connected(X,Z1,L1),
                             connected(Z1,Z2,L2),
                             connected(Z2,Y,L3).
</pre>
</div>

<div class="extract swish" id="1.2.2">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-1" id="swish.1.2.2" inherit-id="swish.1.0.1" query-text="?-reachable(oxford_circus,charing_cross,R).">
reachable(X,Y,noroute):-connected(X,Y,L).
reachable(X,Y,route(Z,R)):-connected(X,Z,L),
                         connected(Z,Y,R).
</pre>
</div>

<p class="tekst">
 The query <tt>?-reachable(oxford_circus,charing_cross,R)</tt> now has three possible answers:
</p>
<p class="tekst AutoStyle19">
 { <tt>R</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>route(piccadilly_circus)</tt> }<br>
 { <tt>R</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>route(tottenham_court_road,leicester_square)</tt> }<br>
  { <tt>R</tt>
   <span class="AutoStyle09">
    &rarr;
   </span>
   <tt>route(piccadilly_circus,leicester_square)</tt> }
</p>
<div class="extract figure" id="1.6">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle20">
      <p class="med-figure AutoStyle07">
       <img src="img/part_i/image012.svg" v:shapes="_x0000_i1030" width="100%"/>
      </p>
     </div>
     <p class="med-caption">
      <b>Figure 1.6.</b> A   complex object as a tree.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="sektie">
 As argued in the previous section, we prefer the recursive definition of the reachability relation, in which case we use functors in a somewhat different way.
</p>

<div class="extract swish" id="1.2.2_2">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-1" id="swish.1.2.2" inherit-id="swish.1.0.1" query-text="?-reachable(oxford_circus,charing_cross,R).">
reachable(X,Y,noroute):-connected(X,Y,L).
reachable(X,Y,route(Z,R)):-connected(X,Z,L),
                           reachable(Z,Y,R).
</pre>
</div>

<p class="tekst">
 At first sight, there does not seem to be a big difference between this and the use of functors in the non-recursive program. However, the query
</p>
<p class="p-el">
 ?-reachable(oxford_circus,charing_cross,R)
</p>
<p class="tekst">
 now has the following answers:
</p>
<p class="p-eerst AutoStyle21">
 {R
 <span class="AutoStyle09">
  &rarr;
 </span>
 route(tottenham_court_road,<br>
 route(leicester_square,noroute))}
</p>
<p class="programma">
 {R
 <span class="AutoStyle09">
  &rarr;
 </span>
 route(piccadilly_circus,noroute)}
</p>
<p class="p-laatst AutoStyle21">
 {R
 <span class="AutoStyle09">
  &rarr;
 </span>
 route(piccadilly_circus,<br>
 route(leicester_square,noroute))}
</p>
<p class="tekst">
 The functor <tt>route</tt> is now also recursive in nature: its first argument is a station, but <i>its second argument is again a route</i>. For instance, the object
</p>
<p align="right" class="p-el AutoStyle22">
 route(tottenham_court_road,route(leicester_square,noroute))
</p>
<p class="tekst">
 can be pictured as in fig. 1.6. Such a figure is called a <i>tree</i>&nbsp;(we will have a lot more to say about trees in chapter 4). In order to find out the route represented by this complex object, we read the leaves of this tree from left to right, until we reach the &lsquo;terminator&rsquo; <tt>noroute</tt>. This would result in a linear notation like
</p>
<p class="p-el">
 [tottenham_court_road,leicester_square].
</p>
<div class="extract figure" id="1.7">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle20">
      <p class="med-figure AutoStyle07">
       <img src="img/part_i/image014.svg" v:shapes="_x0000_i1031" width="100%"/>
      </p>
     </div>
     <p class="med-caption">
      <b>Figure 1.7.</b> The list <tt>[a,b,c</tt>] as a tree.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="sektie">
 For user-defined functors, such a linear notation is not available. However, Prolog provides a built-in &lsquo;datatype&rsquo; called <i>lists</i>, for which both the tree-like notation and the linear notation may be used. The functor for lists is <tt>.</tt>&nbsp;(dot), which takes two arguments: the first element of the list (which may be any object), and the rest of the list (which must be a list). The list terminator is the special symbol <tt>[]</tt>, denoting the empty list. For instance, the term
</p>
<p class="p-el">
 .(a,.(b,.(c,[])))
</p>
<p class="tekst">
 denotes the list consisting of <tt>a</tt> followed by <tt>b</tt> followed by <tt>c</tt> (fig. 1.7). Alternatively, we may use the linear notation, which uses square brackets:
</p>
<p class="p-el">
 [a,b,c]
</p>
<p class="tekst">
 To increase readability of the tree-like notation, instead of
</p>
<p class="p-el">
 .(First,Rest)
</p>
<p class="tekst">
 one can also write
</p>
<p class="p-el">
 [First|Rest]
</p>
<p class="tekst">
 Note that <tt>Rest</tt> is a list: e.g., <tt>[a,b,c]</tt> is the same list as <tt>[a|[b,c]]</tt>. <tt>a</tt> is called the <i>head</i>&nbsp;of the list, and <tt>[b,c]</tt> is called its <i>tail</i>. Finally, to a certain extent the two notations can be mixed: at the head of the list, you can write any number of elements in linear notation. For instance,
</p>
<p class="p-el">
 [First,Second,Third|Rest]
</p>
<p class="tekst">
 denotes a list with three or more elements.
</p>
<div class="extract exercise" id="1.4">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 1.4.</i> A list is either the empty list <tt>[]</tt>, or a non-empty list <tt>[First|Rest]</tt> where <tt>Rest</tt> is a list. Define a relation <tt>list(L)</tt>, which checks whether <tt>L</tt> is a list. Adapt it such that it succeeds only for lists of (<i>i</i>) even length and (<i>ii</i>) odd length.
 </p>
</div>
</div>
<p class="sektie">
 The recursive nature of such datastructures makes it possible to ignore the size of the objects, which is extremely useful in many situations. For instance, the definition of a route between two underground stations does not depend on the length of the route; all that matters is whether there is an intermediate station or not. For both cases, there is a clause. Expressing the route as a list, we can state the final definition of the reachability relation:
</p>

<div class="extract swish" id="1.2.3">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-1" id="swish.1.2.3" inherit-id="swish.1.0.1" query-text="?-reachable(oxford_circus,charing_cross,R). ?-reachable(X,charing_cross,[A,B,C,D]). ?-reachable(bond_street,piccadilly_circus,[A,B|L]).">
reachable(X,Y,[]):-connected(X,Y,L).
reachable(X,Y,[Z|R]):-connected(X,Z,L),
                      reachable(Z,Y,R).
</pre>
</div>

<p class="tekst">
 The query <tt>?-reachable(oxford_circus,charing_cross,R)</tt> now results in the following answers:
</p>
<p class="tekst AutoStyle19">
 { <tt>R</tt>
 <span class="AutoStyle09">
  &rarr;
 </span>
 <tt>[tottenham_court_road,leicester_square]</tt> }<br>
 { <tt>R</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>[piccadilly_circus]</tt> }<br>
  { <tt>R</tt>
   <span class="AutoStyle09">
    &rarr;
   </span>
   <tt>[piccadilly_circus, leicester_square]</tt> }
</p>
<p class="tekst">
 Note that Prolog writes out lists of fixed length in the linear notation.
</p>
<p class="sektie">
 Should we for some reason want to know from which station Charing Cross can be reached via a route with four intermediate stations, we should ask the query
</p>
<p class="sektie AutoStyle23">
 <tt>?-reachable(X,charing_cross,[A,B,C,D])</tt>
</p>
<p class="tekst">
 which results in two answers:
</p>
<p class="p-eerst AutoStyle24">
 <span class="AutoStyle25">
  {&nbsp;
 </span>
 X
 <span class="AutoStyle09">
  &rarr;
 </span>
 bond_street
 <span class="AutoStyle25">
  ,
 </span>
 A
 <span class="AutoStyle09">
  &rarr;
 </span>
 green_park
 <span class="AutoStyle25">
  ,
 </span>
 B
 <span class="AutoStyle09">
  &rarr;
 </span>
 oxford_circus
 <span class="AutoStyle25">
  ,
 </span>
 C
 <span class="AutoStyle09">
  &rarr;
 </span>
 tottenham_court_road
 <span class="AutoStyle25">
  ,
 </span>
 D
 <span class="AutoStyle09">
  &rarr;
 </span>
 leicester_square
 <span class="AutoStyle25">
  }
 </span>
</p>
<p class="p-laatst AutoStyle26">
 <span class="AutoStyle25">
  {&nbsp;
 </span>
 X
 <span class="AutoStyle09">
  &rarr;
 </span>
 bond_street
 <span class="AutoStyle25">
  ,
 </span>
 A
 <span class="AutoStyle09">
  &rarr;
 </span>
 green_park
 <span class="AutoStyle25">
  ,
 </span>
 B
 <span class="AutoStyle09">
  &rarr;
 </span>
 oxford_circus
 <span class="AutoStyle25">
  ,
 </span>
 C
 <span class="AutoStyle09">
  &rarr;
 </span>
 piccadilly_circus
 <span class="AutoStyle25">
  ,
 </span>
 D
 <span class="AutoStyle09">
  &rarr;
 </span>
 leicester_square
 <span class="AutoStyle25">
  }.
 </span>
</p>
<div class="extract exercise" id="1.5">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 1.5.</i> Construct a query asking for a route from Bond Street to Piccadilly Circus with at least two intermediate stations.
 </p>
</div>
</div>
<h3 id="what_else_is_there_to_know_about_clausal_logic">
 1.4&nbsp;&nbsp;&nbsp;What else is there to know about clausal logic?
</h3>
<p class="sektie1">
 The main goal of this chapter has been to introduce the most important concepts in clausal logic, and how it can be used as a reasoning formalism. Needless to say, a subject like this needs a much more extensive and precise discussion than has been attempted here, and many important questions remain. To name a few:
</p>
<p class="opsomming AutoStyle27">
 &bull;what are the limits of expressiveness of clausal logic, i.e. what can and what cannot be expressed?
</p>
<p class="opsomming AutoStyle27">
 &bull;what are the limits of reasoning with clausal logic, i.e. what can and what cannot be (efficiently) computed?
</p>
<p class="opsomming AutoStyle27">
 &bull;how are these two limits related: is it for instance possible to enhance reasoning by limiting expressiveness?
</p>
<p class="tekst">
 In order to start answering such questions, we need to be more precise in defining what clausal logic is, what expressions in clausal logic mean, and how we can reason with them. That means that we will have to introduce some theory in the next chapter. This theory will not only be useful for a better understanding of Logic Programming, but it will also be the foundation for most of the topics in Part III (<i>Advanced reasoning techniques</i>).
</p>
<p class="sektie">
 Another aim of Part I of this book is to teach the skill of programming in Prolog. For this, theory alone, however important, will not suffice. Like any programming language, Prolog has a number of built-in procedures and datastructures that you should know about. Furthermore, there are of course numerous programming techniques and tricks of the trade, with which the Prolog programmer should be familiar. These subjects will be discussed in Chapter 3. Together, Chapters 2 and 3 will provide a solid foundation for the rest of the book.
</p>
<b>
 <span class="AutoStyle02">
  <br clear="all"/>
 </span>
</b>
<div class="WordSection3">
 <p class="cijfer" id="clausal_logic_and_resolution_theoretical_backgrounds">
  2
 </p>
 <h2 id="h_clausal_logic_and_resolution_theoretical_backgrounds">
  Clausal logic and resolution:<br>
  theoretical backgrounds
</h2>
 <p class="sektie1">
  In this chapter we develop a more formal view of Logic Programming by means of a rigorous treatment of clausal logic and resolution theorem proving. Any such treatment has three parts: syntax, semantics, and proof theory. <i>Syntax</i> defines the logical language we are using, i.e. the alphabet, different kinds of &lsquo;words&rsquo;, and the allowed &lsquo;sentences&rsquo;. <i>Semantics</i> defines, in some formal way, the meaning of words and sentences in the language. As with most logics, semantics for clausal logic is <i>truth-functional</i>, i.e. the meaning of a sentence is defined by specifying the conditions under which it is assigned certain <i>truth values</i> (in our case: <b>true</b> or <b>false</b>). Finally, <i>proof theory</i> specifies how we can obtain new sentences (theorems) from assumed ones (axioms) by means of pure symbol manipulation (inference rules).
 </p>
 <p class="sektie">
  Of these three, proof theory is most closely related to Logic Programming, because answering queries is in fact no different from proving theorems. In addition to proof theory, we need semantics for deciding whether the things we prove actually make sense. For instance, we need to be sure that the truth of the theorems is assured by the truth of the axioms. If our inference rules guarantee this, they are said to be <i>sound</i>. But this will not be enough, because sound inference rules can be actually very weak, and unable to prove anything of interest. We also need to be sure that the inference rules are powerful enough to eventually prove any possible theorem: they should be <i>complete</i>.
 </p>
 <p class="sektie">
  Concepts like soundness and completeness are called <i>meta-theoretical</i>, since they are not expressed <b>in</b> the logic under discussion, but rather belong to a theory <b>about</b> that logic (&lsquo;meta&rsquo; means above). Their significance is not merely theoretical, but extends to logic programming languages like Prolog. For example, if a logic programming language is unsound, it will give wrong answers to some queries; if it is incomplete, it will give no answer to some other queries. Ideally, a logic programming language should be sound and complete; in practice, this will not be the case. For instance, in the next chapter we will see that Prolog is both unsound and incomplete. This has been a deliberate design choice: a sound and complete Prolog would be much less efficient. Nevertheless, any Prolog programmer should know exactly the circumstances under which Prolog is unsound or incomplete, and avoid these circumstances in her programs.
 </p>
 <p class="sektie">
  The structure of this chapter is as follows. We start with a very simple (propositional) logical language, and enrich this language in two steps to full clausal logic. For each of these three languages, we discuss syntax, semantics, proof theory, and meta-theory. We then discuss definite clause logic, which is the subset of clausal logic used in Prolog. Finally, we relate clausal logic to Predicate Logic, and show that they are essentially equal in expressive power.
 </p>
 <h3 id="propositional_clausal_logic">
  2.1&nbsp;&nbsp;&nbsp;Propositional clausal logic
 </h3>
 <p class="sektie1">
  Informally, a <i>proposition</i>&nbsp;is any statement which is either true or false, such as &lsquo;2 + 2 = 4&rsquo; or &lsquo;the moon is made of green cheese&rsquo;. These are the building blocks of propositional logic, the weakest form of logic.
 </p>
 <p class="sektie1">
  <i>Syntax.&nbsp;&nbsp;</i> Propositions are abstractly denoted by <i>atoms</i>, which are single words starting with a lowercase character. For instance, <tt>married</tt> is an atom denoting the proposition &lsquo;he/she is married&rsquo;; similarly, <tt>man</tt> denotes the proposition &lsquo;he is a man&rsquo;. Using the special symbols &lsquo; <tt>:-</tt> &rsquo; (<b>if</b>), &lsquo; <tt>;</tt> &rsquo; (<b>or</b>) and &lsquo; <tt>,</tt> &rsquo; (<b>and</b>), we can combine atoms to form <i>clauses</i>. For instance,
 </p>
 <p class="p-el">
  married;bachelor:-man,adult
 </p>
 <p class="tekst">
  is a clause, with intended meaning: &lsquo;somebody is married <b>or</b> a bachelor <b>if</b> he is a man <b>and</b> an adult&rsquo;
  <span class="CustomFootnote">
   <a href="#_ftn2" name="_ftnref2" title="">
    <span class="MsoFootnoteReference">
     <span class="AutoStyle13">
      <span class="AutoStyle14">
       [2]
      </span>
     </span>
    </span>
   </a>
  </span>
  . The part to the left of the if-symbol &lsquo; <tt>:-</tt> &rsquo; is called the <i>head</i>&nbsp;of the clause, and the right part is called the <i>body</i>&nbsp;of the clause. The head of a clause is always a disjunction&nbsp;(<b>or</b>) of atoms, and the body of a clause is always a conjunction&nbsp;(<b>and</b>).
 </p>
<div class="extract exercise" id="2.1">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.1.</i> Translate the following statements into clauses, using the atoms <tt>person</tt>, <tt>sad</tt> and <tt>happy</tt>:<br>
   (<i>a</i>)&nbsp;&nbsp;&nbsp;&nbsp;persons are happy or sad;<br>
    (<i>b</i>)&nbsp;&nbsp;&nbsp;&nbsp;no person is both happy and sad;<br>
     (<i>c</i>)&nbsp;&nbsp;&nbsp;&nbsp;sad persons are not happy;<br>
      (<i>d</i>)&nbsp;&nbsp;&nbsp;&nbsp;non-happy persons are sad.
</p>
 </div>
</div>
 <p class="sektie">
  A <i>program</i>&nbsp;is a set of clauses, each of them terminated by a period. The clauses are to be read conjunctively; for example, the program
 </p>
 <p class="p-el">
  woman;man:-human.<br>
  human:-woman.<br>
  human:-man.
</p>
 <p class="tekst">
  has the intended meaning &lsquo;(<b>if</b> someone is human <b>then</b> she/he is a woman <b>or</b> a man) <b>and</b> (<b>if</b> someone is a woman <b>then</b> she is human) <b>and</b> (<b>if</b> someone is a man <b>then</b> he is human)&rsquo;, or, in other words, &lsquo;someone is human <b>if and only if</b> she/he is a woman <b>or</b> a man&rsquo;.
 </p>
 <p class="sektie1">
  <i>Semantics.&nbsp;&nbsp;</i> The <i>Herbrand base</i>&nbsp;of a program <i>P</i> is the set of atoms occurring in <i>P</i>. For the above program, the Herbrand base is { <tt>woman</tt>, <tt>man</tt>, <tt>human</tt> }. A <i>Herbrand interpretation</i>&nbsp;(or interpretation for short) for <i>P</i> is a mapping from the Herbrand base of <i>P</i> into the set of truth values { <b>true</b>, <b>false</b> }. For example, the mapping { <tt>woman</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <b>true</b>, <tt>man</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <b>false</b>, <tt>human</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <b>true</b> } is a Herbrand interpretation for the above program. A Herbrand interpretation can be viewed as describing a possible state of affairs in the Universe of Discourse&nbsp;(in this case: &lsquo;she is a woman, she is not a man, she is human&rsquo;). Since there are only two possible truth values in the semantics we are considering, we could abbreviate such mappings by listing only the atoms that are assigned the truth value <b>true</b>; by definition, the remaining ones are assigned the truth value <b>false</b>. Under this convention, which we will adopt in this book, a Herbrand interpretation is simply a subset of the Herbrand base. Thus, the previous Herbrand interpretation would be represented as { <tt>woman</tt>, <tt>human</tt> }.
 </p>
 <p class="sektie">
  Since a Herbrand interpretation assigns truth values to every atom in a clause, it also assigns a truth value to the clause as a whole. The rules for determining the truth value of a clause from the truth values of its atoms are not so complicated, if you keep in mind that the body of a clause is a conjunction of atoms, and the head is a disjunction. Consequently, the body of a clause is <b>true</b> if every atom in it is <b>true</b>, and the head of a clause is <b>true</b> if at least one atom in it is <b>true</b>. In turn, the truth value of the clause is determined by the truth values of head and body. There are four possibilities:
 </p>
 <p class="opsomming">
  (<i>i</i>)&nbsp;&nbsp;&nbsp;the body is <b>true</b>, and the head is <b>true</b>;
 </p>
 <p class="opsomming">
  (<i>ii</i>)&nbsp;&nbsp;the body is <b>true</b>, and the head is <b>false</b>;
 </p>
 <p class="opsomming">
  (<i>iii</i>)&nbsp;the body is <b>false</b>, and the head is <b>true</b>;
 </p>
 <p class="opsomming">
  (<i>iv</i>)&nbsp;the body is <b>false</b>, and the head is <b>false</b>.
 </p>
 <p class="tekst">
  The intended meaning of the clause is &lsquo; <b>if</b> body <b>then</b> head&rsquo;, which is obviously <b>true</b> in the first case, and <b>false</b> in the second case.
 </p>
 <p class="sektie">
  What about the remaining two cases? They cover statements like &lsquo; <b>if</b> the moon is made of green cheese <b>then</b> 2 + 2 = 4&rsquo;, in which there is no connection at all between body and head. One would like to say that such statements are neither <b>true</b> nor <b>false</b>. However, our semantics is not sophisticated enough to deal with this: it simply insists that clauses should be assigned a truth value in every possible interpretation. Therefore, we consider the clause to be <b>true</b> whenever its body is <b>false</b>. It is not difficult to see that under these truth conditions a clause is equivalent with the statement &lsquo;head <b>or not</b> body&rsquo;. For example, the clause <tt>married;bachelor:-man,adult</tt> can also be read as &lsquo;someone is married <b>or</b> a bachelor <b>ornot</b> a man <b>ornot</b> an adult&rsquo;. Thus, a clause is a disjunction of atoms, which are negated if they occur in the body of the clause. Therefore, the atoms in the body of the clause are often called <i>negative literals</i>, while those in the head of the clause are called <i>positive literals</i>.
 </p>
 <p class="sektie">
  To summarise: a clause is assigned the truth value <b>true</b> in an interpretation, if and only if at least one of the following conditions is true: (<i>a</i>) at least one atom in the body of the clause is <b>false</b> in the interpretation (cases (<i>iii</i>) and (<i>iv</i>)), or (<i>b</i>) at least one atom in the head of the clause is <b>true</b> in the interpretation (cases (<i>i</i>) and (<i>iii</i>)). If a clause is <b>true</b> in an interpretation, we say that the interpretation is a <i>model</i>&nbsp;for the clause. An interpretation is a model for a program if it is a model for each clause in the program. For example, the above program has the following models:
  <span class="AutoStyle09">
   &empty;
  </span>
  (the empty model, assigning <b>false</b> to every atom), { <tt>woman</tt>, <tt>human</tt> }, { <tt>man</tt>, <tt>human</tt> }, and { <tt>woman</tt>, <tt>man</tt>, <tt>human</tt> }. Since there are eight possible interpretations for a Herbrand base with three atoms, this means that the program contains enough information to rule out half of these.
 </p>
 <p class="sektie">
  Adding more clauses to the program means restricting its set of models. For instance, if we add the clause <tt>woman</tt> (a clause with an empty body) to the program, we rule out the first and third model, which leaves us with the models { <tt>woman</tt>, <tt>human</tt> }, and { <tt>woman</tt>, <tt>man</tt>, <tt>human</tt> }. Note that in both of these models, <tt>human</tt> is <b>true</b>. We say that <tt>human</tt> is a logical consequence of the set of clauses. In general, a clause <i>C</i> is a <i>logical consequence</i>&nbsp;of a program <i>P</i> if every model of the program is also a model of the clause; we write <i>P</i> =&nbsp;<i>C</i>.
 </p>
<div class="extract exercise" id="2.2">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.2.</i> Given the program<br>
   &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<tt>married;bachelor:-man,adult.<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;man.<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:-bachelor.</tt><br>
determine which of the following clauses are logical consequences of this program:<br>
(<i>a</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>married:-adult</tt>;<br>
      (<i>b</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>married:-bachelor</tt>;<br>
       (<i>c</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>bachelor:-man</tt>;<br>
        (<i>d</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>bachelor:-bachelor</tt>.
</p>
 </div>
</div>
 <p class="sektie">
  Of the two remaining models, obviously { <tt>woman</tt>, <tt>human</tt> } is the intended one; but the program does not yet contain enough information to distinguish it from the non-intended model { <tt>woman</tt>, <tt>man</tt>, <tt>human</tt> }. We can add yet another clause, to make sure that the atom <tt>man</tt> is mapped to <b>false</b>. For instance, we could add
 </p>
 <p class="p-el">
  :-man
 </p>
 <p class="tekst">
  (it is not a man) or
 </p>
 <p class="p-el">
  :-man,woman
 </p>
 <p class="tekst">
  (nobody is both a man and a woman). However, explicitly stating everything that is false in the intended model is not always feasible. Consider, for example, an airline database consulted by travel agencies: we simply want to say that if a particular flight (i.e., a combination of plane, origin, destination, date and time) is not listed in the database, then it does not exist, instead of listing all the dates that a particular plane does <b>not</b> fly from Amsterdam to London.
 </p>
 <p class="sektie">
  So, instead of adding clauses until a single model remains, we want to add a rule to our semantics which tells us which of the several models is the intended one. The airline example shows us that, in general, we only want to accept something as <b>true</b> if we are really forced to, i.e. if it is <b>true</b> in every possible model. This means that we should take the intersection of every model of a program in order to construct the intended model. In the example, this is { <tt>woman</tt>, <tt>human</tt> }. Note that this model is <i>minimal</i>&nbsp;in the sense that no subset of it is also a model. Therefore, this semantics is called a <i>minimal model semantics</i>.
 </p>
 <p class="sektie">
  Unfortunately, this approach is only applicable to a restricted class of programs. Consider the following program:
 </p>
 <p class="p-el">
  woman;man:-human.<br>
  human.
</p>
 <p class="tekst">
  This program has three models: { <tt>woman</tt>, <tt>human</tt> }, { <tt>man</tt>, <tt>human</tt> }, and { <tt>woman</tt>, <tt>man</tt>, <tt>human</tt> }. The intersection of these models is { <tt>human</tt> }, but this interpretation is not a model of the first clause! The program has in fact not one, but <b>two</b> minimal models, which is caused by the fact that the first clause has a disjunctive head. Such a clause is called <i>indefinite</i>, because it does not permit definite conclusions to be drawn.
 </p>
 <p class="sektie">
  On the other hand, if we would only allow <i>definite</i> clauses, i.e. clauses with a single positive literal, minimal models are guaranteed to be unique. We will deal with definite clauses in section 2.4, because Prolog is based on definite clause logic. In principle, this means that clauses like <tt>woman;man:-human</tt> are not expressible in Prolog. However, such a clause can be transformed into a &lsquo;pseudo-definite&rsquo; clause by moving one of the literals in the head to the body, extended with an extra negation. This gives the following two possibilities:
 </p>
 <p class="p-el">
  woman:-human,not(man).<br>
  man:-human,not(woman).
</p>
 <p class="tekst">
  In Prolog, we have to choose between these two clauses, which means that we have only an approximation of the original indefinite clause. Negation in Prolog is an important subject with many aspects. In Chapter 3, we will show how Prolog handles negation in the body of clauses. In Chapter 8, we will discuss particular applications of this kind of negation.
 </p>
 <p class="sektie1">
  <i>Proof theory.&nbsp;&nbsp;</i> Recall that a clause <i>C</i> is a logical consequence of a program <i>P</i> (<i>P</i> = <i>C</i>) if every model of <i>P</i> is a model of <i>C</i>. Checking this condition is, in general, unfeasible. Therefore, we need a more efficient way of computing logical consequences, by means of inference rules. If <i>C</i> can be derived from <i>P</i> by means of a number of applications of such inference rules, we say that <i>C</i> can be <i>proved</i> from <i>P</i>. Such inference rules are purely syntactic, and do not refer to any underlying semantics.
 </p>
 <p class="sektie">
  The proof theory for clausal logic consists of a single inference rule&nbsp;called <i>resolution</i>. Resolution is a very powerful inference rule. Consider the following program:
 </p>
 <p class="p-el">
  married;bachelor:-man,adult.<br>
  has_wife:-man,married.
</p>
 <p class="tekst">
  This simple program has no less than 26 models, each of which needs to be considered if we want to check whether a clause is a logical consequence of it.
 </p>
<div class="extract exercise" id="2.3">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.3.</i> Write down the six Herbrand interpretations that are not models of the program.
  </p>
 </div>
</div>
 <p class="sektie">
  The following clause is a logical consequence of this program:
 </p>
 <p class="p-el">
  has_wife;bachelor:-man,adult
 </p>
 <p class="tekst">
  By means of resolution, it can be produced in a single step. This step represents the following line of reasoning: &lsquo;if someone is a man and an adult, then he is a bachelor or married; but if he is married, he has a wife; therefore, if someone is a man and an adult, then he is a bachelor or he has a wife&rsquo;. In this argument, the two clauses in the program are related to each other by means of the atom <tt>married</tt>, which occurs in the head of the first clause (a positive literal) and in the body of the second (a negative literal). The derived clause, which is called the <i>resolvent</i>, consists of all the literals of the two input clauses, except <tt>married</tt> (the literal <i>resolved upon</i>). The negative literal <tt>man</tt>, which occurs in both input clauses, appears only once in the derived clause. This process is depicted in fig. 2.1.
 </p>
 <div class="extract figure" id="2.1">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle05">
       <p class="figure">
        <img src="img/part_i/image016.svg" v:shapes="_x0000_i1032" width="100%"/>
       </p>
      </div>
      <p class="caption">
       <b>Figure 2.1.</b> A   resolution step.
      </p>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="sektie">
  Resolution is most easily understood when applied to definite clauses. Consider the following program:
 </p>
 <p class="p-el">
  square:-rectangle,equal_sides.<br>
  rectangle:-parallelogram,right_angles.
</p>
 <p class="tekst">
  Applying resolution yields the clause
 </p>
 <p class="p-el">
  square:-parallelogram,right_angles,equal_sides
 </p>
 <div class="extract figure" id="2.2">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle05">
       <p class="figure">
        <img src="img/part_i/image018.svg" v:shapes="_x0000_i1033" width="100%"/>
       </p>
      </div>
      <p class="caption">
       <b>Figure 2.2.</b> Resolution with definite clauses.
      </p>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="tekst">
  That is, the atom <tt>rectangle</tt> in the body of the first clause is replaced by the body of the second clause (which has <tt>rectangle</tt> as its head). This process is also referred to as <i>unfolding</i>&nbsp;the second clause into the first one (fig. 2.2).
 </p>
 <p class="sektie">
  A resolvent resulting from one resolution step can be used as input for the next. A <i>proof</i>&nbsp;or <i>derivation</i>&nbsp;of a clause <i>C</i> from a program <i>P</i> is a sequence of clauses such that each clause is either in the program, or the resolvent of two previous clauses, and the last clause is <i>C</i>. If there is a proof of <i>C</i> from <i>P</i>, we write <i>P</i> |&nbsp;<i>C</i>.
 </p>
<div class="extract exercise" id="2.4">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.4.</i> Give a derivation of <tt>friendly</tt> from the following program:<br>
   &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<tt>happy;friendly:-teacher.<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;friendly:-teacher,happy.<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;teacher;wise.<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;teacher:-wise.</tt>
</p>
 </div>
</div>
 <p class="sektie1">
  <i>Meta-theory.&nbsp;&nbsp;</i> It is easy to show that propositional resolution is <b>sound</b>: you have to establish that every model for the two input clauses is a model for the resolvent. In our earlier example, every model of <tt>married;bachelor:-man,adult</tt> and <tt>has_wife:-man,married</tt> must be a model of <tt>has_wife;bachelor:-man,adult</tt>. Now, the literal resolved upon (in this case <tt>married</tt>) is either assigned the truth value <b>true</b> or <b>false</b>. In the first case, every model of <tt>has_wife:-man,married</tt> is also a model of <tt>has_wife:-man</tt>; in the second case, every model of <tt>married;bachelor:-man,adult</tt> is also a model of <tt>bachelor:-man,adult</tt>.
  In both cases, these models are models of a subclause of the resolvent, which means that they are also models of the resolvent itself.
 </p>
 <p class="sektie">
  In general, proving <b>completeness</b> is more complicated than proving soundness. Still worse, proving completeness of resolution is impossible, because resolution is not complete at all! For instance, consider the clause <tt>a:-a</tt>. This clause is a so-called <i>tautology</i>: it is true under any interpretation. Therefore, any model of an arbitrary program <i>P</i> is a model for it, and thus <i>P</i> = <tt>a:-a</tt> for any program <i>P</i>. If resolution were complete, it would be possible to derive the clause <tt>a:-a</tt> from some program <i>P</i> in which the literal <tt>a</tt> doesn&rsquo;t even occur! It is clear that resolution is unable to do this.
 </p>
 <p class="sektie">
  However, this is not necessarily bad, because although tautologies follow from any set of clauses, they are not very interesting. Resolution makes it possible to guide the inference process, by implementing the question &lsquo;is <i>C</i> a logical consequence of <i>P</i>?&rsquo; rather than &lsquo;what are the logical consequences of <i>P</i>?&rsquo;. We will see that, although resolution is unable to generate every logical consequence of a set of clauses, it is complete in the sense that resolution can always determine whether a specific clause is a logical consequence of a set of clauses.
 </p>
 <p class="sektie">
  The idea is analogous to a proof technique in mathematics called &lsquo;reduction to the absurd&rsquo;. Suppose for the moment that <i>C</i> consists of a single positive literal <tt>a</tt>; we want to know whether <i>P</i> = <tt>a</tt>, i.e. whether every model of <i>P</i> is also a model of <tt>a</tt>. It is easily checked that an interpretation is a model of <tt>a</tt> if, and only if, it is <b>not</b> a model of <tt>:-a</tt>. Therefore, every model of <i>P</i> is a model of <tt>a</tt> if, and only if, there is no interpretation which is a model of both <tt>:-a</tt> and <i>P</i>. In other words, <tt>a</tt> is a logical consequence of <i>P</i> if, and only if, <tt>:-a</tt> and <i>P</i> are mutually <i>inconsistent</i>&nbsp;(don&rsquo;t have a common model). So, checking whether <i>P</i> = <tt>a</tt> is equivalent to checking whether <i>P</i>
  <span class="AutoStyle09">
   &cup;
  </span>
  { <tt>:-a</tt> } is inconsistent.
 </p>
 <p class="sektie">
  Resolution provides a way to check this condition. Note that, since an inconsistent set of clauses doesn&rsquo;t have a model, it trivially satisfies the condition that any model of it is a model of any other clause; therefore, an inconsistent set of clauses has every possible clause as its logical consequence. In particular, the absurd or <i>empty</i> clause, denoted by
  <span class="AutoStyle11">
   □
  </span>
  <span class="CustomFootnote">
   <a href="#_ftn3" name="_ftnref3" title="">
    <span class="MsoFootnoteReference">
     <span class="AutoStyle13">
      <span class="AutoStyle14">
       [3]
      </span>
     </span>
    </span>
   </a>
  </span>
  , is a logical consequence of an inconsistent set of clauses. Conversely, if<br>
  <br>
  <span class="AutoStyle11">
     □
    </span>
is a logical consequence of a set of clauses, we know it must be inconsistent. Now, resolution is complete in the sense that <i>if P set of clauses is inconsistent, it is always possible to derive<span class="AutoStyle11">
    □
   </span>
   by resolution</i>. Since resolution is sound, we already know that if we can derive
  <span class="AutoStyle11">
   □
  </span>
  then the input clauses must be inconsistent. So we conclude: <tt>a</tt> is a logical consequence of <i>P</i> if, and only if, the empty clause can be deduced by resolution from <i>P</i> augmented with <tt>:-a</tt>.
  This process is called <i>proof by refutation</i>, and resolution is called <i>refutation complete</i>.
 </p>
 <p class="sektie">
  This proof method can be generalised to the case where <i>B</i> is not a single atom. For instance, let us check by resolution that <tt>a:-a</tt> is a tautology, i.e. a logical consequence of any set of clauses. Logically speaking, this clause is equivalent to &lsquo; <tt>a</tt> <b>or not</b> <tt>a</tt> &rsquo;, the negation of which is &lsquo; <b>not</b> <tt>a</tt> <b>and</b> <tt>a</tt> &rsquo;, which is represented by two separate clauses <tt>:-a</tt> and <tt>a</tt>. Since we can derive the empty clause from these two clauses in a single resolution step without using any other clauses, we have in fact proved that <tt>a:-a</tt> is a logical consequence of an empty set of clauses, hence a tautology.
 </p>
<div class="extract exercise" id="2.5">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.5.</i> Prove by refutation that <tt>friendly:-has_friends</tt> is a logical consequence of the following clauses:<br>
   &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<tt>happy:-has_friends.<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;friendly:-happy.</tt>
</p>
 </div>
</div>
 <p class="sektie">
  Finally, we mention that although resolution can always be used to prove inconsistency of a set of clauses it is not always fit to prove the opposite, i.e. consistency of a set of clauses. For instance, <tt>a</tt> is not a logical consequence of <tt>a:-a</tt>; yet, if we try to prove the inconsistency of <tt>:-a</tt> and <tt>a:-a</tt> (which should fail) we can go on applying resolution forever! The reason, of course, is that there is a loop in the system: applying resolution to <tt>:-a</tt> and <tt>a:-a</tt> again yields <tt>:-a</tt>. In this simple case it is easy to check for loops: just maintain a list of previously derived clauses, and do not proceed with clauses that have been derived previously.
 </p>
 <p class="sektie">
  However, as we will see, this is not possible in the general case of full clausal logic, which is <i>semi-decidable</i>&nbsp;with respect to the question &lsquo;is <i>B</i> a logical consequence of <i>A</i> &rsquo;: there is an algorithm which derives, in finite time, a proof if one exists, but there is no algorithm which, for any <i>A</i> and <i>B</i>, halts and returns &lsquo;no&rsquo; if no proof exists. The reason for this is that interpretations for full clausal logic are in general infinite. As a consequence, some Prolog programs may loop forever (just like some Pascal programs). One might suggest that it should be possible to check, just by examining the source code, whether a program is going to loop or not, but, as Alan Turing showed, this is, in general, impossible (the Halting Problem). That is, you can write programs for checking termination of programs, but for any such termination checking program you can write a program on which it will not terminate itself!
 </p>
 <h3 id="relational_clausal_logic">
  2.2&nbsp;&nbsp;&nbsp;Relational clausal logic
 </h3>
 <p class="sektie1">
  Propositional clausal logic is rather coarse-grained, because it takes propositions (i.e. anything that can be assigned a truth value) as its basic building blocks. For example, it is not possible to formulate the following argument in propositional logic:
 </p>
 <p class="opsomming AutoStyle28">
  Peter likes all his students
 </p>
 <p class="opsomming">
  Maria is one of Peter&rsquo;s students
 </p>
 <p class="opsomming AutoStyle29">
  Therefore, Peter likes Maria
 </p>
 <p class="tekst">
  In order to formalise this type of reasoning, we need to talk about individuals like Peter and Maria, sets of individuals like Peter&rsquo;s students, and relations between individuals, such as &lsquo;likes&rsquo;. This refinement of propositional clausal logic leads us into relational clausal logic.
 </p>
 <p class="sektie1">
  <i>Syntax.&nbsp;&nbsp;</i> Individual names are called <i>constants</i>; we follow the Prolog convention of writing them as single words starting with a lowercase character (or as arbitrary strings enclosed in single quotes, like <tt>'this is a constant'</tt>). Arbitrary individuals are denoted by <i>variables</i>, which are single words starting with an uppercase character. Jointly, constants and variables are denoted as <i>terms</i>. A <i>ground</i> term&nbsp;is a term without variables
  <span class="CustomFootnote">
   <a href="#_ftn4" name="_ftnref4" title="">
    <span class="MsoFootnoteReference">
     <span class="AutoStyle13">
      <span class="AutoStyle14">
       [4]
      </span>
     </span>
    </span>
   </a>
  </span>
  .
 </p>
 <p class="sektie">
  Relations between individuals are abstractly denoted by <i>predicates</i> (which follow the same notational conventions as constants). An <i>atom</i>&nbsp;is a predicate followed by a number of terms, enclosed in brackets and separated by commas, e.g. <tt>likes(peter,maria)</tt>. The terms between brackets are called the <i>arguments</i> of the predicate, and the number of arguments is the predicate&rsquo;s <i>arity</i>. The arity of a predicate is assumed to be fixed, and predicates with the same name but different arity are assumed to be different. A <i>ground</i> atom&nbsp;is an atom without variables.
 </p>
 <p class="sektie">
  All the remaining definitions pertaining to the syntax of propositional clausal logic, in particular those of literal, clause and program, stay the same. So, the following clauses are meant to represent the above statements:
 </p>

<div class="extract swish" id="2.2.1">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.2.1" query-text="?-likes(peter,S). ?-likes(T,maria). ?-likes(T,S).">
likes(peter,S):-student_of(S,peter).
student_of(maria,peter).
</pre>
</div>

 <p class="tekst">
  The intended meaning of these clauses are, respectively, &lsquo; <b>if</b> <i>S</i> is a student of Peter <b>then</b> Peter likes <i>S</i> &rsquo;, &lsquo;Maria is a student of Peter&rsquo;, and &lsquo;Peter likes Maria&rsquo;. Clearly, we want our logic to be such that the third clause follows logically from the first two, and we want to be able to prove this by resolution. Therefore, we must extend the semantics and proof theory in order to deal with variables.
 </p>
 <p class="sektie1">
  <i>Semantics.&nbsp;&nbsp;</i> The <i>Herbrand universe</i>&nbsp;of a program <i>P</i> is the set of ground terms (i.e. constants) occurring in it. For the above program, the Herbrand universe is { <tt>peter</tt>, <tt>maria</tt> }. The Herbrand universe is the set of all individuals we are talking about in our clauses. The <i>Herbrand base</i>&nbsp;of <i>P</i> is the set of <b>ground</b> atoms that can be constructed using the predicates in <i>P</i> and the ground terms in the Herbrand universe. This set represents all the things we can say about the individuals in the Herbrand universe.
 </p>
 <p class="sektie">
  The Herbrand base of the above program is
 </p>
 <p class="p-el AutoStyle30">
  <span class="AutoStyle25">
   {&nbsp;
  </span>
  likes(peter,peter)
  <span class="AutoStyle25">
   ,
  </span>
  likes(peter,maria)
  <span class="AutoStyle25">
   ,<br>
   </span>
  likes(maria,peter)
  <span class="AutoStyle25">
   ,
  </span>
  likes(maria,maria)
  <span class="AutoStyle25">
   ,<br>
   </span>
  student_of(peter,peter)
  <span class="AutoStyle25">
   ,
  </span>
  student_of(peter,maria)
  <span class="AutoStyle25">
   ,<br>
   </span>
  student_of(maria,peter)
  <span class="AutoStyle25">
   ,
  </span>
  student_of(maria,maria)
  <span class="AutoStyle25">
   }
  </span>
 </p>
 <p class="tekst">
  As before, a <i>Herbrand interpretation</i> is the subset of the Herbrand base whose elements are assigned the truth value <b>true</b>. For instance,
 </p>
 <p class="p-el">
  <span class="AutoStyle25">
   {
  </span>
  likes(peter,maria)
  <span class="AutoStyle25">
   ,
  </span>
  student_of(maria,peter)
  <span class="AutoStyle25">
   }
  </span>
 </p>
 <p class="tekst">
  is an interpretation of the above program.
 </p>
 <div class="extract infobox" id="logical_variables">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle31">
       <p class="inter-title AutoStyle32">
        Logical variables
       </p>
       <p class="intermezzo AutoStyle33">
        Variables in clausal logic are very similar to variables in   mathematical formulas: they are placeholders that can be substituted by   arbitrary ground terms from the Herbrand universe. It is very important to   notice that <i>logical variables are   global within a clause</i> (i.e. if the variable occurs at several positions   within a clause, it should be substituted everywhere by the same term), <i>but not within a program</i>. This can be   clearly seen from the semantics of relational clausal logic, where grounding   substitutions are applied to clauses rather than programs. As a consequence,   variables in two different clauses are distinct by definition,<br>
        even if they have the same name. It will sometimes be useful to rename the   variables in clauses, such that no two clauses share a variable; this is   called <i>standardising</i>&nbsp;the clauses <i>apart</i>.
</p>
      </div>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="sektie">
  Clearly, we want this interpretation to be a model of the program, but now we have to deal with the variables in the program. A <i>substitution</i>&nbsp;is a mapping from variables to terms. For example, { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt> } and { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>X</tt> } are substitutions. A substitution can be <i>applied</i> to a clause, which means that all occurrences of a variable occurring on the lefthand side in a substitution are replaced by the term on the righthand side. For instance, if <i>C</i> is the clause
 </p>
 <p class="p-el">
  likes(peter,S):-student_of(S,peter)
 </p>
 <p class="tekst">
  then the above substitutions yield the clauses
 </p>
 <p class="p-el">
  likes(peter,maria):-student_of(maria,peter)
 </p>
 <p class="pi-laatst">
  likes(peter,X):-student_of(X,peter)
 </p>
 <p class="tekst">
  Notice that the first clause is ground; it is said to be a <i>ground instance</i>&nbsp;of <i>C</i>, and the substitution { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt> } is called a <i>grounding substitution</i>. All the atoms in a ground clause occur in the Herbrand base, so reasoning with ground clauses is just like reasoning with propositional clauses. An interpretation is a model for a non-ground clause if it is a model for every ground instance of the clause. Thus, in order to show that
 </p>
 <p class="p-el">
  <i>
   <span class="AutoStyle25">
    M
   </span>
  </i>
  <span class="AutoStyle25">
   = {
  </span>
  likes(peter,maria)
  <span class="AutoStyle25">
   ,
  </span>
  student_of(maria,peter)
  <span class="AutoStyle25">
   }
  </span>
 </p>
 <p class="tekst">
  is a model of the clause <i>C</i> above, we have to construct the set of the ground instances of <i>C</i> over the Herbrand universe { <tt>peter</tt>, <tt>maria</tt> }, which is
 </p>
 <p class="p-el AutoStyle34">
  <span class="AutoStyle25">
   {
  </span>
  likes(peter,maria):-student_of(maria,peter)
  <span class="AutoStyle25">
   ,
  </span><br>
  likes(peter,peter):-student_of(peter,peter)
   <span class="AutoStyle25">
    }
   </span>
</p>
 <p class="tekst">
  and show that <i>M</i> is a model of every element of this set.
 </p>
<div class="extract exercise" id="2.6">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.6.</i> How many models does <i>C</i> have over the Herbrand universe<br>
   { <tt>peter</tt>, <tt>maria</tt> }?
</p>
 </div>
</div>
 <p class="sektie1">
  <i>Proof theory.&nbsp;&nbsp;</i> Because reasoning with ground clauses is just like reasoning with propositional clauses, a naive proof method in relational clausal logic would apply grounding substitutions to every clause in the program before applying resolution. Such a method is naive, because a program has many different grounding substitutions, most of which do not lead to a resolution proof. For instance, if the Herbrand universe contains four constants, then a clause with two distinct variables has 16 different grounding substitutions, and a program consisting of three such clauses has 4096 different grounding substitutions.
 </p>
 <p class="sektie">
  Instead of applying arbitrary grounding substitutions before trying to apply resolution, we will derive the required substitutions from the clauses themselves. Recall that in order to apply propositional resolution, the literal resolved upon should occur in both input clauses (positive in one clause and negative in the other). In relational clausal logic, atoms can contain variables. Therefore, we do not require that exactly the same atom occurs in both clauses; rather, we require that there is a pair of atoms <i>which can be made equal by substituting terms for variables</i>. For instance, let <i>P</i> be the following program:
 </p>
 <p class="p-el">
  likes(peter,S):-student_of(S,peter).<br>
  student_of(maria,T):-follows(maria,C),teaches(T,C).
</p>
 <p class="tekst">
  The second clause is intended to mean: &lsquo;Maria is a student of any teacher who teaches a course she follows&rsquo;. From these two clauses we should be able to prove that &lsquo;Peter likes Maria <b>if</b> Maria follows a course taught by Peter&rsquo;. This means that we want to resolve the two clauses on the <tt>student_of</tt> literals.
 </p>
 <p class="sektie">
  The two atoms <tt>student_of(S,peter)</tt> and <tt>student_of(maria,T)</tt> can be made equal by replacing <tt>S</tt> by <tt>maria</tt> and <tt>T</tt> by <tt>peter</tt>, by means of the substitution { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt>, <tt>T</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>peter</tt> }. This process is called <i>unification</i>, and the substitution is called a <i>unifier</i>. Applying this substitution yields the following two clauses:
 </p>
 <p class="p-el">
  likes(peter,maria):-student_of(maria,peter).<br>
  student_of(maria,peter):-follows(maria,C),<br>
  &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;teaches(peter,C).
</p>
 <p class="tekst">
  (Note that the second clause is not ground.) We can now construct the resolvent in the usual way, by dropping the literal resolved upon and combining the remaining literals, which yields the required clause
 </p>
 <p class="p-el">
  likes(peter,maria):-follows(maria,C),teaches(peter,C).
 </p>
<div class="extract exercise" id="2.7">
      <div class="AutoStyle06">
       <p class="exercise AutoStyle07">
        <i>Exercise 2.7</i>.   Write a clause expressing that Peter teaches all the first-year courses, and   apply resolution to this clause and the above resolvent.
       </p>
      </div>
 </div>
 <p class="sektie">
  Consider the following two-clause program <i>P</i>
  <span class="AutoStyle09">
   &prime;
  </span>
  :
 </p>
 <p class="p-el">
  likes(peter,S):-student_of(S,peter).<br>
  student_of(X,T):-follows(X,C),teaches(T,C).
</p>
 <p class="tekst">
  which differs from the previous program <i>P</i> in that the constant <tt>maria</tt> in the second clause has been replaced by a variable. Since this generalises the applicability of this clause from Maria to any of Peter&rsquo;s students, it follows that any model for <i>P</i>
  <span class="AutoStyle09">
   &prime;
  </span>
  over a Herbrand universe including <tt>maria</tt> is also a model for <i>P</i>, and therefore <i>P</i>
  <span class="AutoStyle09">
   &prime;
  </span>
  = <i>P</i>. In particular, this means that all the logical consequences of <i>P</i>
  <span class="AutoStyle09">
   &prime;
  </span>
  are also logical consequences of <i>P</i>. For instance, we can again derive the clause
 </p>
 <p class="p-el">
  likes(peter,maria):-follows(maria,C),teaches(peter,C).
 </p>
 <p class="tekst">
  from <i>P</i>
  <span class="AutoStyle09">
   &prime;
  </span>
  by means of the unifier { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt>, <tt>X</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt>, <tt>T</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>peter</tt> }.
 </p>
 <p class="sektie">
  Unifiers are not necessarily grounding substitutions: the substitution { <tt>X</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>S</tt>, <tt>T</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>peter</tt> } also unifies the two <tt>student_of</tt> literals, and the two clauses then resolve to
 </p>
 <p class="p-el">
  likes(peter,S):-follows(S,C),teaches(peter,C).
 </p>
 <p class="tekst">
  The first unifier replaces more variables by terms than strictly necessary, while the second contains only those substitutions that are needed to unify the two atoms in the input clauses. As a result, the first resolvent is a special case of the second resolvent, that can be obtained by means of the additional substitution { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt> }. Therefore, the second resolvent is said to be <i>more general</i> than the first
  <span class="CustomFootnote">
   <a href="#_ftn5" name="_ftnref5" title="">
    <span class="MsoFootnoteReference">
     <span class="AutoStyle13">
      <span class="AutoStyle14">
       [5]
      </span>
     </span>
    </span>
   </a>
  </span>
  . Likewise, the second unifier is called a more general unifier than the first.
 </p>
 <p class="sektie">
  As it were, more general resolvents summarise a lot of less general ones. It therefore makes sense to derive only those resolvents that are as general as possible, when applying resolution to clauses with variables. This means that we are only interested in a <i>most general unifier</i>&nbsp;(mgu) of two literals. Such an mgu, if it exists, is always unique, apart from an arbitrary renaming of variables (e.g. we could decide to keep the variable <tt>X</tt>, and replace <tt>S</tt> by <tt>X</tt>). If a unifier does not exist, we say that the two atoms are not unifiable. For instance, the atoms <tt>student_of(maria,peter)</tt> and <tt>student_of(S,maria)</tt> are not unifiable.
 </p>
 <p class="sektie">
  As we have seen before, the actual proof method in clausal logic is proof by refutation. If we succeed in deriving the empty clause, then we have demonstrated that the set of clauses is inconsistent <i>under the substitutions that are needed for unification of literals</i>. For instance, consider the program
 </p>

<div class="extract swish" id="2.2.7">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.2.7" query-text="?-likes(peter,N). ?-student_of(N,peter). ?-follows(N,C),teaches(peter,C). ?-teaches(peter,ai_techniques).">
likes(peter,S):-student_of(S,peter).
student_of(S,T):-follows(S,C),teaches(T,C).
teaches(peter,ai_techniques).
follows(maria,ai_techniques).
</pre>
</div>

 <p class="tekst">
  If we want to find out if there is anyone whom Peter likes, we add to the program the negation of this statement, i.e. &lsquo;Peter likes nobody&rsquo; or <tt>:-likes(peter,N)</tt>; this clause is called a <i>query</i>&nbsp;or a <i>goal</i>. We then try to refute this query by finding an inconsistency by means of resolution. A refutation proof is given in fig. 2.3. In this figure, which is called a <i>proof tree</i>, two clauses on a row are input clauses for a resolution step, and they are connected by lines to their resolvent, which is then again an input clause for a resolution step, together with another program clause. The mgu&rsquo;s are also shown. Since the empty clause is derived, the query is indeed refuted, but only under the substitution { <tt>N</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt> }, which constitutes the <i>answer</i>&nbsp;to the query.
 </p>
 <div class="extract figure" id="2.3">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle05">
       <p class="figure">
        <img src="img/part_i/image020.svg" v:shapes="_x0000_i1034" width="100%"/>
       </p>
      </div>
      <p class="caption">
       <b>Figure 2.3.</b> A   refutation proof which finds someone whom Peter likes.
      </p>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="sektie">
  In general, a query can have several answers. For instance, suppose that Peter does not only like his students, but also the people his students like (and the people those people like, and &hellip;):
 </p>

<div class="extract swish" id="2.2.8">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.2.8">
likes(peter,S):-student_of(S,peter).
likes(peter,Y):-likes(peter,X),likes(X,Y).
likes(maria,paul).
student_of(S,T):-follows(S,C),teaches(T,C).
teaches(peter,ai_techniques).
follows(maria,ai_techniques).
</pre>
</div>

 <p class="tekst">
  The query
 </p>

<div class="extract swish" id="1.2.8_2">
<pre class="swish query" source-id="swish.2.2.8">?-likes(peter,N).</pre>
</div>

 <p class="tekst">
  will now have two answers.
 </p>
<div class="extract exercise" id="2.8">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.8</i>. Draw the proof tree for the answer { <tt>N</tt>
   <span class="AutoStyle09">
    &rarr;
   </span>
   <tt>paul</tt> }.
  </p>
 </div>
</div>
 <p class="sektie1">
  <i>Meta-theory.&nbsp;&nbsp;</i> As with propositional resolution, relational resolution is sound&nbsp;(i.e. it always produces logical consequences of the input clauses), refutation complete (i.e. it always detects an inconsistency in a set of clauses), but not complete&nbsp;(i.e. it does not always generate every logical consequence of the input clauses). An important characteristic of relational clausal logic is that the Herbrand universe (the set of individuals we can reason about) is always finite. Consequently, models are finite as well, and there are a finite number of different models for any program. This means that, in principle, we could answer the question &lsquo;is <i>C</i> a logical consequence of <i>P</i>?&rsquo; by enumerating all the models of <i>P</i>, and checking whether they are also models of <i>C</i>. The finiteness of the Herbrand universe will ensure that this procedure always terminates. This demonstrates that relational clausal logic is decidable, and therefore it is (in principle) possible to prevent resolution from looping if no more answers can be found. As we will see in the next section, this does not hold for full clausal logic.
 </p>
 <h3 id="full_clausal_logic">
  2.3&nbsp;&nbsp;&nbsp;Full clausal logic
 </h3>
 <p class="sektie1">
  Relational logic extends propositional logic by means of the logical variable, which enables us to talk about arbitrary un-named individuals. However, consider the following statement:
 </p>
 <p class="sektie AutoStyle23">
  Everybody loves somebody.
 </p>
 <p class="tekst">
  The only way to express this statement in relational clausal logic, is by explicitly listing every pair of persons such that the first loves the second, e.g.
 </p>
 <p class="p-el">
  loves(peter,peter).<br>
  loves(anna,paul).<br>
  loves(paul,anna).<br>
  </p>
 <p class="tekst">
  First of all, this is not a precise translation of the above statement into logic, because it is too explicit (e.g. the fact that Peter loves himself does not follow from the original statement). Secondly, this translation works only for <i>finite</i> domains, while the original statement also allows infinite domains. Many interesting domains are infinite, such as the set of natural numbers. Full clausal logic allows us to reason about infinite domains by introducing more complex terms besides constants and variables. The above statement translates into full clausal logic as
 </p>
 <p class="p-el">
  loves(X,person_loved_by(X))
 </p>
 <p class="tekst">
  The fact <tt>loves(peter,person_loved_by(peter))</tt> is a logical consequence of this clause. Since we know that everybody loves somebody, there must exist someone whom Peter loves. We have given this person the <i>abstract name</i>
 </p>
 <p class="p-el">
  person_loved_by(peter)
 </p>
 <p class="tekst">
  without explicitly stating whom it is that Peter loves. As we will see, this way of composing complex names from simple names also gives us the possibility to reflect the structure of the domain in our logical formulas.
 </p>
<div class="extract exercise" id="2.9">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.9</i>. Translate to clausal logic:<br>
   (<i>a</i>)&nbsp;&nbsp;&nbsp;&nbsp;every mouse has a tail;<br>
    (<i>b</i>)&nbsp;&nbsp;&nbsp;&nbsp;somebody loves everybody;<br>
     (<i>c</i>)&nbsp;&nbsp;&nbsp;&nbsp;every two numbers have a maximum.
</p>
 </div>
</div>
 <p class="sektie1">
  <i>Syntax.&nbsp;&nbsp;</i> A <i>term</i>&nbsp;is either simple or complex. Constants and variables are <i>simple terms</i>. A <i>complex term</i>&nbsp;is a functor (which follows the same notational conventions as constants and predicates) followed by a number of terms, enclosed in brackets and separated by commas, e.g. <tt>eldest_child_of(anna,paul)</tt>. The terms between brackets are called the <i>arguments</i> of the functor, and the number of arguments is the functor&rsquo;s <i>arity</i>. Again, a <i>ground</i> term&nbsp;is a term without variables. All the other definitions (atom, clause, literal, program) are the same as for relational clausal logic.
 </p>
 <p class="sektie1">
  <i>Semantics.&nbsp;&nbsp;</i> Although there is no <b>syntactic</b> difference in full clausal logic between terms and atoms, their <b>meaning</b> and use is totally different, a fact which should be adequately reflected in the semantics. A term always denotes an individual from the domain, while an atom denotes a proposition about individuals, which can get a truth value. Consequently, we must change the definition of the Herbrand universe in order to accomodate for complex terms: given a program <i>P</i>, the <i>Herbrand universe</i>&nbsp;is the set of ground terms that can be constructed from the constants and functors in <i>P</i> (if <i>P</i> contains no constants, choose an arbitrary one). For instance, let <i>P</i> be the program
 </p>

<div class="extract swish" id="2.3.1">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.3.1" query-text="?-plus(s(0),s(s(0)),Z). ?-plus(s(0),Y,s(s(s(0)))). ?-plus(X,s(s(0)),s(s(s(0)))). ?-plus(X,Y,Z).">
plus(0,X,X).
plus(s(X),Y,s(Z)):-plus(X,Y,Z).
</pre>
</div>

 <p class="tekst">
  then the Herbrand universe of <i>P</i> is { <tt>0</tt>, <tt>s(0)</tt>, <tt>s(s(0))</tt>, <tt>s(s(s(0)))</tt>, &hellip;}. Thus, as soon as a program contains a functor, the Herbrand universe (the set of individuals we can reason about) is an infinite set.
 </p>
<div class="extract exercise" id="2.10">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.10</i>. Determine the Herbrand universe of the following program:
  </p>

<div class="extract swish" id="2.3.2">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.3.2" query-text="?-listlength([0,0,0],N). ?-listlength(L,s(s(0))). ?-listlength(L,N).">
listlength([],0).
listlength([_X|Y],s(L)):-listlength(Y,L).
</pre>
</div>

  <p class="exercise AutoStyle07">
   (Hint: recall that <tt>[]</tt> is a constant, and that <tt>[X|Y]</tt> is an alternative notation for the complex term <tt>.(X,Y)</tt> with binary functor &lsquo; <tt>.</tt> &rsquo;!)
  </p>
 </div>
</div>
 <p class="sektie">
  The <i>Herbrand base</i>&nbsp;of <i>P</i> remains the set of ground atoms that can be constructed using the predicates in <i>P</i> and the ground terms in the Herbrand universe. For the above program, the Herbrand base is
 </p>
 <p class="p-el AutoStyle36">
  <span class="AutoStyle25">
   {
  </span>
  plus(0,0,0)
  <span class="AutoStyle25">
   ,
  </span>
  plus(s(0),0,0)
  <span class="AutoStyle25">
   , &hellip;,
  </span><br>
  plus(0,s(0),0)
   <span class="AutoStyle25">
    ,
   </span>
   plus(s(0),s(0),0)
   <span class="AutoStyle25">
    , &hellip;,
   </span><br>
   <span class="AutoStyle25">
     &hellip;,
    </span><br>
    plus(s(0),s(s(0)),s(s(s(0))))
     <span class="AutoStyle25">
      , &hellip;}
     </span>
</p>
 <p class="tekst">
  As before, a <i>Herbrand interpretation</i>&nbsp;is a subset of the Herbrand base, whose elements are assigned the truth value <b>true</b>. For instance,
 </p>
 <p class="p-el">
  <span class="AutoStyle25">
   {
  </span>
  plus(0,0,0)
  <span class="AutoStyle25">
   ,
  </span>
  plus(s(0),0,s(0))
  <span class="AutoStyle25">
   ,
  </span>
  plus(0,s(0),s(0))
  <span class="AutoStyle25">
   }
  </span>
 </p>
 <p class="tekst">
  is an interpretation of the above program.
 </p>
 <div class="extract infobox" id="unification_vs_evaluation">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle31">
       <p class="inter-title AutoStyle32">
        Unification vs. evaluation
       </p>
       <p class="intermezzo AutoStyle32">
        Functors should not be confused with mathematical functions.   Although both can be viewed as mappings from objects to objects, <i>an expression containing a functor is not   evaluated</i> to determine the value of the mapping, as in mathematics.   Rather, the outcome of the mapping is a name, which is determined by <i>unification</i>. For instance, given the   complex term <tt>person_loved_by(X)</tt>, if   we want to know the name of the object to which Peter is mapped, we unify <tt>X</tt> with <tt>peter</tt> to get <tt>person_loved_by(peter)</tt>; this   ground term is not evaluated any further.
       </p>
       <p class="intermezzo AutoStyle33">
        This approach has the disadvantage that we introduce different   names for individuals that might turn out to be identical, e.g. <tt>person_loved_by(peter)</tt> might be the same   as <tt>peter</tt>. Consequently, reasoning   about equality (of different names for the same object) is a problem in   clausal logic. Several possible solutions exist, but they fall outside the   scope of this book.
       </p>
      </div>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="sektie">
  Is this interpretation also a model&nbsp;of the program? As in the propositional case, we define an interpretation to be a model of a program if it is a model of every ground instance of every clause in the program. But since the Herbrand universe is infinite, there are an infinite number of grounding substitutions, hence we must generate the ground clauses in a systematic way, e.g.
 </p>
 <p class="p-el">
  plus(0,0,0)<br>
  plus(s(0),0,s(0)):-plus(0,0,0)<br>
  plus(s(s(0)),0,s(s(0))):-plus(s(0),0,s(0))<br>
  plus(s(s(s(0))),0,s(s(s(0)))):-plus(s(s(0)),0,s(s(0)))<br>
  &hellip;<br>
  plus(0,s(0),s(0))<br>
  plus(s(0),s(0),s(s(0))):-plus(0,s(0),s(0))<br>
  plus(s(s(0)),s(0),s(s(s(0)))):-plus(s(0),s(0),s(s(0)))<br>
  &hellip;<br>
  plus(0,s(s(0)),s(s(0)))<br>
  plus(s(0),s(s(0)),s(s(s(0)))):-plus(0,s(s(0)),s(s(0)))<br>
  plus(s(s(0)),s(s(0)),s(s(s(s(0))))):-<br>
  &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;plus(s(0),s(s(0)),s(s(s(0))))<br>
  &hellip;
</p>
 <p class="tekst">
  Now we can reason as follows: according to the first ground clause, <tt>plus(0,0,0)</tt> must be in any model; but then the second ground clause requires that <tt>plus(s(0),0,s(0))</tt> must be in any model, the third ground clause requires <tt>plus(s(s(0)),0,s(s(0)))</tt> to be in any model, and so on. Likewise, the second group of ground clauses demands that
 </p>
 <p class="p-el">
  plus(0,s(0),s(0))<br>
  plus(s(0),s(0),s(s(0)))<br>
  plus(s(s(0)),s(0),s(s(s(0))))<br>
  &hellip;
</p>
 <p class="tekst">
  are in the model; the third group of ground clauses requires that
 </p>
 <p class="p-el">
  plus(0,s(s(0)),s(s(0)))<br>
  plus(s(0),s(s(0)),s(s(s(0))))<br>
  plus(s(s(0)),s(s(0)),s(s(s(s(0)))))<br>
  &hellip;
</p>
 <p class="tekst">
  are in the model, and so forth.
 </p>
 <p class="sektie">
  In other words, <i>every model of this program is necessarily infinite</i>. Moreover, as you should have guessed by now, it contains every ground atom such that the number of <tt>s</tt> &rsquo;s in the third argument equals the number of <tt>s</tt> &rsquo;s in the first argument <b>plus</b> the number of <tt>s</tt> &rsquo;s in the second argument. The way we generated this infinite model is particularly interesting, because it is essentially what was called the naive proof method in the relational case: generate all possible ground instances of program clauses by applying every possible grounding substitution, and then apply (propositional) resolution as long as you can. While, in the case of relational clausal logic, there inevitably comes a point where applying resolution will not give any new results (i.e. you reach a <i>fixpoint</i>), in the case of full clausal logic with infinite Herbrand universe you can go on applying resolution forever. On the other hand, as we saw above, we get a clear idea of what the infinite model
  <span class="CustomFootnote">
   <a href="#_ftn6" name="_ftnref6" title="">
    <span class="MsoFootnoteReference">
     <span class="AutoStyle13">
      <span class="AutoStyle14">
       [6]
      </span>
     </span>
    </span>
   </a>
  </span>
  we&rsquo;re constructing looks like, which means that it is still a fixpoint in some sense. There are mathematical techniques to deal with such infinitary fixpoints, but we will not dive into this subject here.
 </p>
 <p class="sektie">
  Although the introduction of only a single functor already results in an infinite Herbrand universe, models are not necessarily infinite. Consider the following program:
 </p>

<div class="extract swish" id="2.3.2_2">
 <pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.3.2" query-text="?-reachable(X,Y,R). ?-connected(X,Y,L).">
reachable(oxford,charing_cross,piccadilly).
reachable(X,Y,route(Z,R)):-
	connected(X,Z,_L),
	reachable(Z,Y,R).
connected(bond_street,oxford,central).
</pre>
</div>

 <p class="tekst">
  with intended meaning &lsquo;Charing Cross is reachable from Oxford Circus via Piccadilly Circus&rsquo;, &lsquo; <b>if</b> <i>X</i> is connected to <i>Z</i> by line <i>L</i> <b>and</b> <i>Y</i> is reachable from <i>Z</i> via <i>R</i> <b>then</b> <i>Y</i> is reachable from <i>X</i> via a route consisting of <i>Z</i> and <i>R</i> &rsquo; and &lsquo;Bond Street is connected to Oxford Circus by the Central line&rsquo;. The minimal model of this program is the finite set
 </p>
 <p class="p-el AutoStyle01">
  <span class="AutoStyle25">
   {
  </span>
  connected(bond_street,oxford,central)
  <span class="AutoStyle25">
   ,<br>
   </span>
  reachable(oxford,charing_cross,piccadilly)
  <span class="AutoStyle25">
   ,<br>
   </span>
  reachable(bond_street,charing_cross,route(oxford,piccadilly))
  <span class="AutoStyle25">
   }
  </span>
 </p>
 <p class="sektie">
  A Prolog program for constructing models of a given set of clauses (or submodels if the models are infinite) can be found in section 5.4.
 </p>
 <p class="sektie1">
  <i>Proof theory.&nbsp;&nbsp;</i> Resolution for full clausal logic is very similar to resolution for relational clausal logic: we only have to modify the unification&nbsp;algorithm in order to deal with complex terms. For instance, consider the atoms
 </p>
 <p class="p-el">
  plus(s(0),X,s(X))
 </p>
 <p class="tekst">
  and
 </p>
 <p class="p-el">
  plus(s(Y),s(0),s(s(Y)))
 </p>
 <p class="tekst">
  Their mgu&nbsp;is { <tt>Y</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>0</tt>, <tt>X</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>s(0)</tt> }, yielding the atom
 </p>
 <p class="p-el">
  plus(s(0),s(0),s(s(0)))
 </p>
 <p class="tekst">
  In order to find this mgu, we first of all have to make sure that the two atoms do not have any variables in common; if needed some of the variables should be renamed. Then, after making sure that both atoms contain the same predicate (with the same arity), we scan the atoms from left to right, searching for the first <b>subterms</b> at which the two atoms differ. In our example, these are <tt>0</tt> and <tt>Y</tt>. If one of these subterms is not a variable, then the two atoms are not unifiable; otherwise, substitute the other term for all occurrences of the variable in both atoms, and remember this partial substitution (in the above example: { <tt>Y</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>0</tt> }), because it is going to be part of the unifier we are constructing. Then, proceed with the next subterms at which the two atoms differ. Unification is finished when no such subterms can be found (the two atoms are made equal).
 </p>
 <p class="sektie">
  Although the two atoms initially have no variables in common, this may change during the unification process. Therefore, it is important that, before a variable is replaced by a term, we check whether the variable already occurs in that term; this is called the <i>occur check</i>. If the variable does not occur in the term by which it is to be replaced, everything is in order and we can proceed; if it does, the unification should fail, because it would lead to circular substitutions and infinite terms. To illustrate this, consider again the clause
 </p>
 <p class="p-el">
  loves(X,person_loved_by(X))
 </p>
 <p class="tekst">
  We want to know whether this implies that someone loves herself; thus, we add the query <tt>:-loves(Y,Y)</tt> to this clause and try to apply resolution. To this end, we must unify the two atoms. The first subterms at which they differ are the first arguments, so we apply the partial substitution <tt>Y</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>X</tt> to the two atoms, resulting in
 </p>
 <p class="p-el">
  loves(X,person_loved_by(X))
 </p>
 <p class="tekst">
  and
 </p>
 <p class="p-el">
  loves(X,X)
 </p>
 <p class="tekst">
  The next subterms at which these atoms differ are their second arguments, one of which is a variable. Suppose that we ignore the fact that this variable, <tt>X</tt>, already occurs in the other term; we construct the substitution <tt>X</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>person_loved_by(X)</tt>. Now, we have reached the end of the two atoms, so unification has succeeded, we have derived the empty clause, and the answer to the query is
 </p>
 <p class="p-el">
  X
  <span class="AutoStyle09">
   &rarr;
  </span>
  person_loved_by(person_loved_by(person_loved_by(&hellip;)))
 </p>
 <p class="tekst">
  which is an infinite term.
 </p>
 <p class="sektie">
  Now we have two problems. The first is that we did not define any semantics for infinite terms, because there are no infinite terms in the Herbrand base. But even worse, the fact that there exists someone who loves herself is not a logical consequence of the above clause! That is, this clause has models in which nobody loves herself. So, <i>unification without occur check would make resolution unsound</i>.
 </p>
<div class="extract exercise" id="2.11">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.11</i>. If possible, unify the following pairs of terms:<br>
   (<i>a</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>plus(X,Y,s(Y))</tt> and <tt>plus(s(V),W,s(s(V)))</tt>;<br>
    (<i>b</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>length([X|Y],s(0))</tt> and <tt>length([V],V)</tt>;<br>
     (<i>c</i>)&nbsp;&nbsp;&nbsp;&nbsp;<tt>larger(s(s(X)),X)</tt> and <tt>larger(V,s(V))</tt>.
</p>
 </div>
</div>
 <p class="sektie">
  The disadvantage of the occur check&nbsp;is that it can be computationally very costly. Suppose that you need to unify <tt>X</tt> with a list of thousand elements, then the complete list has to be searched in order to check whether <tt>X</tt> occurs somewhere in it. Moreover, cases in which the occur check is needed often look somewhat exotic. Since the developers of Prolog were also taking the efficiency of the Prolog interpreter into consideration, they decided to omit the occur check from Prolog&rsquo;s unification algorithm. On the whole, this makes Prolog unsound; but this unsoundness only occurs in very specific cases, and it is the duty of the programmer to avoid such cases.&nbsp;In case you really need sound unification, most available Prolog implementations provide it as a library routine, but you must build your own Prolog interpreter in order to incorporate it. In Chapter 3, we will see that this is in fact amazingly simple: it can even be done in Prolog!
 </p>
 <p class="sektie1">
  <i>Meta-theory.&nbsp;&nbsp;</i> Most meta-theoretical results concerning full clausal logic have already been mentioned. Full clausal resolution is sound&nbsp;(as long as unification is performed with the occur check), refutation complete but not complete. Moreover, due to the possibility of infinite interpretations full clausal logic is only semi-decidable: that is, if <i>A</i> is a logical consequence of <i>B</i>, then there is an algorithm that will check this in finite time; however, if <i>A</i> is not a logical consequence of <i>B</i>, then there is no algorithm which is guaranteed to check this in finite time for arbitrary <i>A</i> and <i>B</i>.Consequently, there is no general way to prevent Prolog from looping if no (further) answers to a query can be found.
 </p>
 <h3 id="definite_clause_logic">
  2.4&nbsp;&nbsp;&nbsp;Definite clause logic
 </h3>
 <p class="sektie1">
  In the foregoing three sections, we introduced and discussed three variants of clausal logic, in order of increasing expressiveness. In this section, we will show how an additional restriction on each of these variants will significantly improve the efficiency of a computational reasoning system for clausal logic. This is the restriction to definite clauses, on which Prolog is based. On the other hand, this restriction also means that definite clause logic is less expressive than full clausal logic, the main difference being that clausal logic can handle negative information. If we allow negated literals in the body of a definite clause then we obtain a so-called general clause, which is probably the closest we can get to full clausal logic without having to sacrifice efficiency.
 </p>
 <p class="sektie">
  Consider the following program:
 </p>
 <p class="p-el">
  married(X);bachelor(X):-man(X),adult(X).<br>
  man(peter).<br>
  adult(peter).<br>
  :-married(maria).<br>
  :-bachelor(maria).<br>
  man(paul).<br>
  :-bachelor(paul).
</p>
 <p class="tekst">
  There are many clauses that are logical consequences of this program. In particular, the following three clauses can be derived by resolution:
 </p>
 <p class="p-el">
  married(peter);bachelor(peter)<br>
  :-man(maria),adult(maria)<br>
  married(paul):-adult(paul)
</p>
<div class="extract exercise" id="2.12">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.12</i>. Draw the proof tree for each of these derivations.
  </p>
 </div>
</div>
 <p class="sektie">
  In each of these derivations, the first clause in the program is used in a different way. In the first one, only literals in the body are resolved away; one could say that the clause is used from right to left. In the second derivation&nbsp;the clause is used from left to right, and in the third one literals from both the head and the body are resolved away. The way in which a clause is used in a resolution proof cannot be fixed in advance, because it depends on the thing we want to prove (the query in refutation proofs).
 </p>
 <p class="sektie">
  On the other hand, this indeterminacy substantially increases the time it takes to find a refutation. Let us decide for the moment to use clauses only in one direction, say from right to left. That is, we can only resolve the negative literals away in a clause, as in the first derivation above, but not the positive literals. But now we have a problem: how are we going to decide whether Peter is married or a bachelor? We are stuck with a clause with two positive literals, representing a disjunctive or <i>indefinite</i>&nbsp;conclusion.
 </p>
 <p class="sektie">
  This problem can in turn be solved by requiring that clauses have exactly one positive literal, which leads us into <i>definite clause logic</i>. Consequently, a definite clause&nbsp;
 </p>
 <p class="sektie AutoStyle37">
  <i>A</i> <tt>:-</tt> <i>B</i>
  <span class="AutoStyle10">
   1
  </span>
  <tt>,</tt> &hellip; <tt>,</tt> <i>B<span class="AutoStyle10">
    n
   </span></i>&nbsp;
 </p>
 <p class="tekst">
  will always be used in the following way: <i>A</i> is proved by proving each of <i>B</i>
  <span class="AutoStyle10">
   1
  </span>
  ,&hellip;, <i>B<span class="AutoStyle10">
    n
   </span></i>. This is called the <i>procedural interpretation</i>&nbsp;of definite clauses, and its simplicity makes the search for a refutation much more efficient than in the indefinite case. Moreover, it allows for an implementation which limits the amount of memory needed, as will be explained in more detail in Chapter 5.
 </p>
 <p class="sektie">
  But how do we express in definite clause logic that adult men are bachelors or married? Even if we read the corresponding indefinite clause from right to left only, it basically has two different procedural interpretations:
 </p>
 <p class="opsomming">
  (<i>i</i>)&nbsp;&nbsp;&nbsp;to prove that someone is married, prove that he is a man and an adult, and prove that he is not a bachelor;
 </p>
 <p class="opsomming">
  (<i>ii</i>)&nbsp;&nbsp;to prove that someone is a bachelor, prove that he is a man and an adult, and prove that he is not married.
 </p>
 <p class="tekst">
  We should first choose one of these procedural interpretations, and then convert it into a &lsquo;pseudo-definite&rsquo; clause. In case (<i>i</i>), this would be
 </p>
 <p class="p-el">
  married(X):-man(X),adult(X),not bachelor(X)
 </p>
 <p class="tekst">
  and case (<i>ii</i>) becomes
 </p>
 <p class="p-el">
  bachelor(X):-man(X),adult(X),not married(X)
 </p>
 <p class="tekst">
  These clauses do not conform to the syntax of definite clause logic, because of the negation symbol <tt>not</tt>. We will call them <i>general clause</i> s.
 </p>
 <p class="sektie">
  If we want to extend definite clause logic to cover general clauses, we should extend resolution in order to deal with negated literals in the body of a clause. In addition, we should extend the semantics. This topic will be addressed in section 8.2. Without going into too much detail here, we will demonstrate that preferring a certain procedural interpretation corresponds to preferring a certain minimal model. Reconsider the original indefinite clause
 </p>
 <p class="p-el">
  married(X);bachelor(X):-man(X),adult(X)
 </p>
 <p class="tekst">
  Supposing that <tt>john</tt> is the only individual in the Herbrand universe, and that <tt>man(john)</tt> and <tt>adult(john)</tt> are both true, then the models of this clause are
 </p>
 <p class="p-el">
  <span class="AutoStyle25">
   {
  </span>
  man(john)
  <span class="AutoStyle25">
   ,
  </span>
  adult(john)
  <span class="AutoStyle25">
   ,
  </span>
  married(john)
  <span class="AutoStyle25">
   }<br>
   {
</span>
  man(john)
  <span class="AutoStyle25">
   ,
  </span>
  adult(john)
  <span class="AutoStyle25">
   ,
  </span>
  bachelor(john)
  <span class="AutoStyle25">
   }<br>
   {
</span>
  man(john)
  <span class="AutoStyle25">
   ,
  </span>
  adult(john)
  <span class="AutoStyle25">
   ,
  </span>
  married(john)
  <span class="AutoStyle25">
   ,
  </span>
  bachelor(john)
  <span class="AutoStyle25">
   }
  </span>
 </p>
 <p class="tekst">
  Note that the first <b>two</b> models are minimal, as is characteristic for indefinite clauses. If we want to make the clause definite, we should single out one of these two minimal models as the <i>intended</i> model. If we choose the first model, in which John is married but not a bachelor, we are actually preferring the general clause
 </p>
 <p class="p-el">
  married(X):-man(X),adult(X),not bachelor(X)
 </p>
 <p class="tekst">
  Likewise, the second model corresponds to the general clause
 </p>
 <p class="p-el">
  bachelor(X):-man(X),adult(X),not married(X)
 </p>
<div class="extract exercise" id="2.13">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.13.</i> Write a clause for the statement &lsquo;somebody is innocent unless proven guilty&rsquo;, and give its intended model (supposing that <tt>john</tt> is the only individual in the Herbrand universe).
  </p>
 </div>
</div>
 <p class="sektie">
  An alternative approach to general clauses is to treat <tt>not</tt> as a special Prolog predicate, as will be discussed in the next chapter. This has the advantage that we need not extend the proof theory and semantics to incorporate general clauses. However, a disadvantage is that in this way <tt>not</tt> can only be understood procedurally.
 </p>
 <h3 id="the_relation_between_clausal_logic_and_predicate_logic">
  2.5&nbsp;&nbsp;&nbsp;The relation between clausal logic and Predicate Logic
 </h3>
 <p class="sektie1">
  Clausal logic is a formalism especially suited for automated reasoning. However, the form of logic usually presented in courses on Symbolic Logic is (first-order) Predicate Logic. Predicate logic is more expressive in the sense that statements expressed in Predicate Logic often result in shorter formulas than would result if they were expressed in clausal logic. This is due to the larger vocabulary and less restrictive syntax of Predicate Logic, which includes quantifiers (&lsquo;for all&rsquo; (
  <span class="AutoStyle09">
   &forall;
  </span>
  ) and &lsquo;there exists&rsquo; (
  <span class="AutoStyle09">
   &exist;
  </span>
  )),  and various logical connectives (conjunction&nbsp;(
  <span class="AutoStyle09">
   &and;
  </span>
  ), disjunction&nbsp;(
  <span class="AutoStyle09">
   &or;
  </span>
  ), negation (
  <span class="AutoStyle09">
   &not;
  </span>
  ), implication&nbsp;(
  <span class="AutoStyle09">
   &rarr;
  </span>
  ), and equivalence&nbsp;(
  <span class="AutoStyle09">
   &harr;
  </span>
  )) which may occur anywhere within a formula.
 </p>
 <p class="sektie">
  Being syntactically quite different, clausal logic and Predicate Logic are semantically equivalent in the following sense: every set of clauses is, after minor modifications, a formula in Predicate Logic, and conversely, every formula in Predicate Logic can be rewritten to an &lsquo;almost&rsquo; equivalent set of clauses. Why then bother about Predicate Logic at all in this book? The main reason is that in Chapter 8, we will discuss an alternative semantics of logic programs, defined in terms of Predicate Logic. In this section, we will illustrate the semantic equivalence of clausal logic and Predicate Logic. We will assume a basic knowledge of the syntax and semantics of Predicate Logic.
 </p>
 <p class="sektie">
  We start with the propositional case. Any clause like
 </p>
 <p class="p-el">
  married;bachelor:-man,adult
 </p>
 <p class="tekst">
  can be rewritten by reversing head&nbsp;and body&nbsp;and replacing the &lsquo; <tt>:-</tt> &rsquo; sign by an implication &lsquo;
  <span class="AutoStyle09">
   &rarr;
  </span>
  &rsquo;, replacing &lsquo; <tt>,</tt> &rsquo; by a conjunction &lsquo;
  <span class="AutoStyle09">
   &and;
  </span>
  &rsquo;, and replacing &lsquo; <tt>;</tt> &rsquo; by a disjunction &lsquo;
  <span class="AutoStyle09">
   &or;
  </span>
  &rsquo;, which yields
 </p>
 <p class="p-el">
  man
  <span class="AutoStyle09">
   &and;
  </span>
  adult
  <span class="AutoStyle09">
   &rarr;
  </span>
  married
  <span class="AutoStyle09">
   &or;
  </span>
  bachelor
 </p>
 <p class="tekst">
  By using the logical laws <i>A</i>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <i>B</i>
  <span class="AutoStyle09">
   &equiv;
  </span>
  <span class="AutoStyle09">
   &not;
  </span>
  <i>A</i>
  <span class="AutoStyle09">
   &or;
  </span>
  <i>B</i> and
  <span class="AutoStyle09">
   &not;
  </span>
  (<i>C</i>
  <span class="AutoStyle09">
   &and;
  </span>
  <i>D</i>)
  <span class="AutoStyle09">
   &equiv;
  </span>
  <span class="AutoStyle09">
   &not;
  </span>
  <i>C</i>
  <span class="AutoStyle09">
   &or;&not;
  </span>
  <i>D</i>, this can be rewritten into the logically equivalent formula
 </p>
 <p class="p-el">
  &not;man
  <span class="AutoStyle09">
   &or;
  </span>
  &not;adult
  <span class="AutoStyle09">
   &or;
  </span>
  married
  <span class="AutoStyle09">
   &or;
  </span>
  bachelor
 </p>
 <p class="tekst">
  which, by the way, clearly demonstrates the origin of the terms <i>negative</i> literal&nbsp;and <i>positive</i> literal!
 </p>
 <p class="sektie">
  A set of clauses can be rewritten by rewriting each clause separately, and combining the results into a single conjunction, e.g.
 </p>
 <p class="p-el">
  married;bachelor:-man,adult.<br>
  has_wife:-man,married.
</p>
 <p class="tekst">
  becomes
 </p>
 <p class="p-el">
  (&not;man
  <span class="AutoStyle09">
   &or;
  </span>
  &not;adult
  <span class="AutoStyle09">
   &or;
  </span>
  married
  <span class="AutoStyle09">
   &or;
  </span>
  bachelor)
  <span class="AutoStyle09">
   &and;<br>
   </span>
  (&not;man
  <span class="AutoStyle09">
   &or;
  </span>
  &not;married
  <span class="AutoStyle09">
   &or;
  </span>
  has_wife)
 </p>
 <p class="tekst">
  Formulas like these, i.e. conjunctions of disjunctions of atoms and negated atoms, are said to be in <i>conjunctive normal form</i>&nbsp;(CNF).
 </p>
 <p class="sektie">
  The term &lsquo;normal form&rsquo; here indicates that <i>every formula of Predicate Logic can be rewritten into a unique equivalent formula in conjunctive normal form</i>, and therefore to a unique equivalent set of clauses. For instance, the formula
 </p>
 <p class="p-el">
  (married
  <span class="AutoStyle09">
   &or;
  </span>
  &not;child)
  <span class="AutoStyle09">
   &rarr;
  </span>
  (adult
  <span class="AutoStyle09">
   &and;
  </span>
  (man
  <span class="AutoStyle09">
   &or;
  </span>
  woman))
 </p>
 <p class="tekst">
  can be rewritten into CNF as (replace <i>A</i>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <i>B</i> by
  <span class="AutoStyle09">
   &not;
  </span>
  <i>A</i>
  <span class="AutoStyle09">
   &or;
  </span>
  <i>B</i>, push negations inside by means of De Morgan&rsquo;s laws:
  <span class="AutoStyle09">
   &not;
  </span>
  (<i>C</i>
  <span class="AutoStyle09">
   &and;
  </span>
  <i>D</i>)
  <span class="AutoStyle09">
   &equiv;
  </span>
  <span class="AutoStyle09">
   &not;
  </span>
  <i>C</i>
  <span class="AutoStyle09">
   &or;&not;
  </span>
  <i>D</i> and
  <span class="AutoStyle09">
   &not;
  </span>
  (<i>C</i>
  <span class="AutoStyle09">
   &or;
  </span>
  <i>D</i>)
  <span class="AutoStyle09">
   &equiv;
  </span>
  <span class="AutoStyle09">
   &not;
  </span>
  <i>C</i>
  <span class="AutoStyle09">
   &and;&not;
  </span>
  <i>D</i>, and distribute
  <span class="AutoStyle09">
   &and;
  </span>
  over
  <span class="AutoStyle09">
   &or;
  </span>
  by means of (<i>A</i>
  <span class="AutoStyle09">
   &and;
  </span>
  <i>B</i>)
  <span class="AutoStyle09">
   &or;
  </span>
  <i>C</i>
  <span class="AutoStyle09">
   &equiv;
  </span>
  (<i>A</i>
  <span class="AutoStyle09">
   &or;
  </span>
  <i>C</i>)
  <span class="AutoStyle09">
   &and;
  </span>
  (<i>B</i>
  <span class="AutoStyle09">
   &or;
  </span>
  <i>C</i>)):
 </p>
 <p class="p-el">
  (&not;married
  <span class="AutoStyle09">
   &or;
  </span>
  adult)
  <span class="AutoStyle09">
   &and;
  </span>
  (&not;married
  <span class="AutoStyle09">
   &or;
  </span>
  man
  <span class="AutoStyle09">
   &or;
  </span>
  woman)
  <span class="AutoStyle09">
   &and;<br>
   </span>
  (child
  <span class="AutoStyle09">
   &or;
  </span>
  adult)
  <span class="AutoStyle09">
   &and;
  </span>
  (child
  <span class="AutoStyle09">
   &or;
  </span>
  man
  <span class="AutoStyle09">
   &or;
  </span>
  woman)
 </p>
 <p class="tekst">
  and hence into clausal form as
 </p>
 <p class="p-el">
  adult:-married.<br>
  man;woman:-married.<br>
  child;adult.<br>
  child;man;woman.
</p>
 <p class="tekst">
  Using a normal form has the advantage that the language contains no redundancy: formulas are only equivalent if they are <b>identical</b> (up to the order of the subformulas). A slight disadvantage is that normal forms are often longer and less understandable (the same objection can be made against resolution proofs).
 </p>
 <div class="extract infobox" id="the_order_of_logics">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle31">
       <p class="inter-title AutoStyle32">
        The order of logics
       </p>
       <p class="intermezzo AutoStyle38">
        A logic with propositions   (statements that can be either true or false) as basic building blocks is   called a propositional logic; a logic built on predicates is called a   Predicate Logic. Since propositions can be viewed as nullary predicates (i.e.   predicates without arguments), any propositional logic is also a Predicate   Logic.
       </p>
       <p class="intermezzo AutoStyle38">
        A logic may or may not have   variables for its basic building blocks. If it does not include such   variables, both the logic and its building blocks are called <i>first-order</i>; this is the normal case.   Thus, in first-order Predicate Logic, there are no<br>
        predicate variables, but only first-order predicates.
</p>
       <p class="intermezzo AutoStyle38">
        Otherwise, an <i>n</i>
        <span class="AutoStyle39">
         th
        </span>
        &nbsp;order logic has variables (and thus   quantifiers) for its (<i>n</i> -1)
        <span class="AutoStyle39">
         th
        </span>
        &nbsp;order building blocks. For instance, the   statement
       </p>
       <p class="intermezzo AutoStyle38">
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>X</tt>
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>Y</tt>: <tt>equal(X,Y)</tt>
        <span class="AutoStyle09">
         &harr;
        </span>
        <tt>(</tt>
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>P</tt>: <tt>P(X)</tt>
        <span class="AutoStyle09">
         &harr;
        </span>
        <tt>P(Y))</tt>
       </p>
       <p class="intermezzo AutoStyle38">
        defining two individuals to be   equal if they have the same properties,<br>
        is a statement from second-order Predicate Logic, because <tt>P</tt> is a<br>
        variable ranging over first-order predicates.
</p>
       <p class="intermezzo AutoStyle38">
        Another example of a statement   from second-order Predicate Logic is
       </p>
       <p class="intermezzo AutoStyle38">
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>P</tt>: <tt>transitive(P)</tt>
        <span class="AutoStyle09">
         &harr;
        </span>
        <tt>(</tt>
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>X</tt>
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>Y</tt>
        <span class="AutoStyle09">
         &forall;
        </span>
        <tt>Z</tt>: <tt>P(X,Y)</tt>
        <span class="AutoStyle09">
         &and;
        </span>
        <tt>P(Y,Z)</tt>
        <span class="AutoStyle09">
         &rarr;
        </span>
        <tt>P(X,Z))</tt>
       </p>
       <p class="intermezzo AutoStyle33">
        This statement defines the   transitivity of binary relations. Since <tt>transitive</tt> has a second-order   variable as argument, it is called a <i>second-order   predicate</i>.
       </p>
      </div>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <p class="sektie">
  For rewriting clauses from full clausal logic to Predicate Logic, we use the same rewrite rules as for propositional clauses. Additionally, we have to add universal quantifiers for every variable in the clause. For example, the clause
 </p>
 <p class="pi-el">
  reachable(X,Y,route(Z,R)):-<br>
  connected(X,Z,L),<br>
  reachable(Z,Y,R).
</p>
 <p class="tekst">
  becomes
 </p>
 <p align="center" class="p-el AutoStyle40">
  <span class="AutoStyle09">
   &forall;
  </span>
  X
  <span class="AutoStyle09">
   &forall;
  </span>
  Y
  <span class="AutoStyle09">
   &forall;
  </span>
  Z
  <span class="AutoStyle09">
   &forall;
  </span>
  R
  <span class="AutoStyle09">
   &forall;
  </span>
  L: &not;connected(X,Z,L)
  <span class="AutoStyle09">
   &or;
  </span>
  &not;reachable(Z,Y,R)
  <span class="AutoStyle09">
   &or;<br>
   </span>
  reachable(X,Y,route(Z,R))
 </p>
 <p class="sektie">
  The reverse process of rewriting a formula of Predicate Logic&nbsp;into an equivalent set of clauses is somewhat complicated if existential quantifiers are involved (the exact procedure is given as a Prolog program in Appendix B.1). An existential quantifier&nbsp;allows us to reason about individuals without naming them. For example, the statement &lsquo;everybody loves somebody&rsquo; is represented by the Predicate Logic formula
 </p>
 <p class="p-el">
  <span class="AutoStyle09">
   &forall;
  </span>
  X
  <span class="AutoStyle09">
   &exist;
  </span>
  Y: loves(X,Y)
 </p>
 <p class="tekst">
  Recall that we translated this same statement into clausal logic as
 </p>
 <p class="p-el">
  loves(X,person_loved_by(X))
 </p>
 <p class="tekst">
  These two formulas are not logically equivalent! That is, the Predicate Logic formula has models like { <tt>loves(paul,anna)</tt> } which are <b>not</b> models of the clause. The reason for this is, that in clausal logic we are forced to introduce abstract names, while in Predicate Logic we are not (we use existential quantification instead). On the other hand, every model of the Predicate Logic formula, if not a model of the clause, can always be converted to a model of the clause, like { <tt>loves(paul,person_loved_by(paul))</tt> }. Thus, we have that the formula has a model if and only if the clause has a model (but not necessarily the same model).
 </p>
 <p class="sektie">
  So, existential quantifiers are replaced by functors. The arguments of the functor are given by the universal quantifiers in whose scope the existential quantifier occurs. In the above example,
  <span class="AutoStyle09">
   &exist;
  </span>
  <tt>Y</tt> occurs within the scope of
  <span class="AutoStyle09">
   &forall;
  </span>
  <tt>X</tt>, so we replace <tt>Y</tt> everywhere in the formula by <tt>person_loved_by(X)</tt>, where <tt>person_loved_by</tt> should be a <b>new</b> functor, not occurring anywhere else in the clause (or in any other clause). This new functor is called a <i>Skolem functor</i>, and the whole process is called <i>Skolemisation</i>. Note that, if the existential quantifier does not occur inside the scope of a universal quantifier, the Skolem functor does not get any arguments, i.e. it becomes a <i>Skolem constant</i>. For example, the formula
 </p>
 <p class="p-el">
  <span class="AutoStyle09">
   &exist;
  </span>
  X
  <span class="AutoStyle09">
   &forall;
  </span>
  Y: loves(X,Y)
 </p>
 <p class="tekst">
  (&lsquo;somebody loves everybody&rsquo;) is translated to the clause
 </p>
 <p class="p-el">
  loves(someone_who_loves_everybody,X)
 </p>
 <p class="sektie">
  Finally, we illustrate the whole process of converting from Predicate Logic&nbsp;to clausal logic by means of an example. Consider the sentence &lsquo;Everyone has a mother, but not every woman has a child&rsquo;. In Predicate Logic, this can be represented as
 </p>
 <p class="p-el">
  <span class="AutoStyle09">
   &forall;
  </span>
  Y
  <span class="AutoStyle09">
   &exist;
  </span>
  X: mother_of(X,Y)
  <span class="AutoStyle09">
   &and;
  </span>
  &not;
  <span class="AutoStyle09">
   &forall;
  </span>
  Z
  <span class="AutoStyle09">
   &exist;
  </span>
  W: woman(Z)
  <span class="AutoStyle09">
   &rarr;
  </span>
  mother_of(Z,W)
 </p>
 <p class="tekst">
  First, we push the negation inside by means of the equivalences
  <span class="AutoStyle09">
   &not;&forall;
  </span>
  <i>X</i>: <i>F</i>
  <span class="AutoStyle09">
   &equiv; &exist;
  </span>
  <i>X</i>:
  <span class="AutoStyle09">
   &not;
  </span>
  <i>F</i> and
  <span class="AutoStyle09">
   &not;&exist;
  </span>
  <i>Y</i>: <i>G</i>
  <span class="AutoStyle09">
   &equiv; &forall;
  </span>
  <i>Y</i>:
  <span class="AutoStyle09">
   &not;
  </span>
  <i>G</i>, and the previously given propositional equivalences, giving
 </p>
 <p class="p-el">
  <span class="AutoStyle09">
   &forall;
  </span>
  Y
  <span class="AutoStyle09">
   &exist;
  </span>
  X: mother_of(X,Y)
  <span class="AutoStyle09">
   &and;
  </span>
  <span class="AutoStyle09">
   &exist;
  </span>
  Z
  <span class="AutoStyle09">
   &forall;
  </span>
  W: woman(Z)
  <span class="AutoStyle09">
   &and;
  </span>
  &not;mother_of(Z,W)
 </p>
 <p class="tekst">
  The existential quantifiers are Skolemised: <tt>X</tt> is replaced by <tt>mother(Y)</tt>, because it is in the scope of the universal quantifier
  <span class="AutoStyle09">
   &forall;
  </span>
  <tt>Y</tt>. <tt>Z</tt>, however, is not in the scope of a universal quantifier; therefore it is replaced by a Skolem constant <tt>childless_woman</tt>. The universal quantifiers can now be dropped:
 </p>
 <p class="p-el">
  mother_of(mother(Y),Y)
  <span class="AutoStyle09">
   &and;
  </span>
  woman(childless_woman)
  <span class="AutoStyle09">
   &and;
  </span>
  &not;mother_of(childless_woman,W)
 </p>
 <p class="tekst">
  This formula is already in CNF, so we obtain the following set of clauses:
 </p>
 <p class="p-el">
  mother_of(mother(Y),Y).<br>
  woman(childless_woman).
   <span class="AutoStyle09"><br>
   :-
</span>
   mother_of(childless_woman,W).
</p>
<div class="extract exercise" id="2.14">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 2.14</i>. Translate to clausal logic:<br>
   (<i>a</i>)&nbsp;&nbsp;&nbsp;&nbsp;
    <span class="AutoStyle09">
     &forall;
    </span>
    <tt>X</tt>
    <span class="AutoStyle09">
     &exist;
    </span>
    <tt>Y: mouse(X)</tt>
    <span class="AutoStyle09">
     &rarr;
    </span>
    <tt>tail_of(Y,X)</tt>;<br>
    (<i>b</i>)&nbsp;&nbsp;&nbsp;&nbsp;
     <span class="AutoStyle09">
      &forall;
     </span>
     <tt>X</tt>
     <span class="AutoStyle09">
      &exist;
     </span>
     <tt>Y: loves(X,Y)</tt>
     <span class="AutoStyle09">
      &and;
     </span>
     <tt>(</tt>
     <span class="AutoStyle09">
      &forall;
     </span>
     <tt>Z: loves(Y,Z))</tt>;<br>
     (<i>c</i>)&nbsp;&nbsp;&nbsp;&nbsp;
      <span class="AutoStyle09">
       &forall;
      </span>
      <tt>X</tt>
      <span class="AutoStyle09">
       &forall;
      </span>
      <tt>Y</tt>
      <span class="AutoStyle09">
       &exist;
      </span>
      <tt>Z: number(X)</tt>
      <span class="AutoStyle09">
       &and;
      </span>
      <tt>number(Y)</tt>
      <span class="AutoStyle09">
       &rarr;
      </span>
      <tt>maximum(X,Y,Z)</tt>.
</p>
 </div>
</div>
 <h3 id="further_reading_2">
  Further reading
 </h3>
 <p class="sektie1">
  Many (but not all) aspects of Artificial Intelligence are amenable to logical analysis. An early advocate of this approach is Kowalski (1979). Overviews of different types of logics used in Artificial Intelligence can be found in (Turner, 1984; Genesereth &amp; Nilsson, 1987; Ramsay, 1988). Bl&auml;sius and B&uuml;rckert (1989) discuss more technical aspects of automated theorem proving.
 </p>
 <p class="sektie">
  The main source for theoretical results in Logic Programming is (Lloyd, 1987). Hogger (1990) gives a more accessible introduction to this theory. (Mendelson, 1987) is an excellent introduction to Predicate Logic.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   K.H. Bl&auml;sius &amp; H.J. B&uuml;rckert
  </span>
  (eds)
  <span class="AutoStyle41">
   (
  </span>
  1989)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Deduction Systems in Artificial Intelligence</i>, Ellis Horwood.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   M.R. Genesereth &amp; N.J. Nilsson (
  </span>
  1987)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Logical Foundations of Artificial Intelligence</i>, Morgan Kaufmann.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   C.J. Hogger (
  </span>
  1990)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Essentials of Logic Programming</i>, Oxford University Press.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   R.A. Kowalski (
  </span>
  1979)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Logic for Problem Solving</i>, North-Holland.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   J.W. Lloyd (
  </span>
  1987)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Foundations of Logic Programming</i>, Springer-Verlag, second edition.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   E. Mendelson (
  </span>
  1987)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Introduction to Mathematical Logic</i>, Wadsworth &amp; Brooks/Cole, third edition.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   R. Turner (
  </span>
  1984)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Logics for Artificial Intelligence</i>, Ellis Horwood.
 </p>
 <p class="referenties">
  <span class="AutoStyle41">
   A. Ramsay (
  </span>
  1988)
  <span class="AutoStyle41">
   ,
  </span>
  <i>Formal Methods in Artificial Intelligence</i>, Cambridge University Press.
 </p>
</div>
<b>
 <span class="AutoStyle02">
  <br clear="all"/>
 </span>
</b>
<div class="WordSection4">
 <p class="cijfer" id="logic_programming_and_prolog">
  3
 </p>
 <h2 id="h_logic_programming_and_prolog">
  Logic Programming and Prolog
 </h2>
 <p class="sektie1">
  In the previous chapters we have seen how logic can be used to represent knowledge about a particular domain, and to derive new knowledge by means of logical inference. A distinct feature of logical reasoning is the separation between model theory and proof theory: a set of logical formulas determines the set of its models, but also the set of formulas that can be derived by applying inference rules. Another way to say the same thing is: logical formulas have both a <i>declarative</i> meaning and a <i>procedural</i> meaning. For instance, declaratively the order of the atoms in the body of a clause is irrelevant, but procedurally it may determine the order in which different answers to a query are found.
 </p>
 <p class="sektie">
  Because of this procedural meaning of logical formulas, logic can be used as a programming language. If we want to solve a problem in a particular domain, we write down the required knowledge and apply the inference rules built into the logic programming language. Declaratively, this knowledge specifies <b>what</b> the problem is, rather than <b>how</b> it should be solved. The distinction between declarative and procedural aspects of problem solving is succinctly expressed by Kowalski&rsquo;s equation
 </p>
 <p class="p-el">
  <i>
   <span class="AutoStyle25">
    algorithm = logic + control
   </span></i>&nbsp;
 </p>
 <p class="tekst">
  Here, <i>logic</i> refers to declarative knowledge, and <i>control</i> refers to procedural knowledge. The equation expresses that both components are needed to solve a problem algorithmically.
 </p>
 <p class="sektie">
  In a purely declarative programming language, the programmer would have no means to express procedural knowledge, because logically equivalent programs would behave identical. However, Prolog is not a purely declarative language, and therefore the procedural meaning of Prolog programs cannot be ignored. For instance, the order of the literals in the body of a clause usually influences the efficiency of the program to a large degree. Similarly, the order of clauses in a program often determines whether a program will give an answer at all. Therefore, in this chapter we will take a closer look at Prolog&rsquo;s inference engine and its built-in features (some of which are non-declarative). Also, we will discuss some common programming techniques.
 </p>
 <h3 id="sld_resolution">
  3.1&nbsp;&nbsp;&nbsp;SLD-resolution
 </h3>
 <p class="sektie1">
  Prolog&rsquo;s proof procedure is based on resolution refutation in definite clause logic. Resolution refutation has been explained in the previous chapter. In order to turn it into an executable proof procedure, we have to specify how a literal to resolve upon is selected, and how the second input clause is found. Jointly, this is called a <i>resolution strategy</i>. Consider the following program:
 </p>

<div class="extract swish" id="3.1.1">
<pre class="source swish temp AutoStyle03" data-variant-id="group-2" id="swish.3.1.1">
student_of(X,T):-follows(X,C),teaches(T,C).
follows(paul,computer_science).
follows(paul,expert_systems).
follows(maria,ai_techniques).
teaches(adrian,expert_systems).
teaches(peter,ai_techniques).
teaches(peter,computer_science).
</pre>
</div>

 <p class="tekst">
  The query
 </p>

<div class="extract swish" id="3.1.1_2">
<pre class="swish query" id="query3.1.1"> ?-student_of(S,peter).</pre>
</div>

 <p class="tekst">
  has two possible answers: { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>paul</tt> } and { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>maria</tt> }. In order to find these answers, we first resolve the query with the first clause, yielding
 </p>

<div class="extract swish" id="3.1.2">
<pre class="swish query" id="query3.1.2">
?-follows(S,C),teaches(peter,C).
</pre>
</div>

 <p class="tekst">
  Now we have to decide whether we will search for a clause which resolves on <tt>follows(S,C)</tt>, or for a clause which resolves on <tt>teaches(peter,C)</tt>. This decision is governed by a <i>selection rule</i>. Prolog&rsquo;s selection rule is left to right, thus Prolog will search for a clause with a positive literal unifying with <tt>follows(S,C)</tt>. There are three of these, so now we must decide which one to try first. Prolog searches the clauses in the program top-down, so Prolog finds the answer { <tt>S</tt>
  <span class="AutoStyle09">
   &rarr;
  </span>
  <tt>paul</tt> } first. Note that the second choice leads to a dead end: the resolvent is
 </p>

<div class="extract swish" id="3.1.3">
<pre class="swish query" id="query3.1.3">
?-teaches(peter,expert_systems).
</pre>
</div>

 <p class="tekst">
  which doesn&rsquo;t resolve with any clause in the program.
 </p>
 <p class="sektie">
  This process is called <i>SLD-resolution</i>: <b>S</b> for selection rule, <b>L</b> for <i>linear</i> resolution&nbsp;(which refers to the shape of the proof trees obtained), and <b>D</b> for <i>definite</i> clauses. Graphically, SLD-resolution can be depicted as in fig. 3.1. This <i>SLD-tree</i>&nbsp;should not be confused with a proof tree: first, only the resolvents are shown (no input clauses or unifiers), and second, it contains every possible resolution step. Thus, every leaf of an SLD-tree which contains the empty clause&nbsp;
  <span class="AutoStyle11">
   □
  </span>
  corresponds to a refutation and hence to a proof tree; such a leaf is also called a <i>success branch</i>. An underlined leaf which does not contain
  <span class="AutoStyle11">
   □
  </span>
  represents a <i>failure branch</i>.
 </p>
<div class="extract exercise" id="3.1">
 <div class="AutoStyle06">
  <p class="exercise AutoStyle07">
   <i>Exercise 3.1.</i> Draw the proof trees for the two success branches in fig. 3.1.
  </p>
 </div>
</div>
 <p class="sektie">
  As remarked already, Prolog searches the clauses in the program top-down, which is the same as traversing the SLD-tree from left to right. This not only determines the order in which answers (i.e. success branches) are found: it also determines whether any answers are found at all, because an SLD-tree may contain infinite branches, if some predicates in the program are recursive. As an example, consider the following program:
 </p>

<div class="extract swish" id="3.1.3_2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.1.3">
brother_of(X,Y):-brother_of(Y,X).
brother_of(paul,peter).
</pre>
</div>

 <div class="extract figure" id="3.1">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle04" valign="top">
      <div class="AutoStyle05">
       <p class="figure">
        <img src="img/part_i/image022.svg" v:shapes="_x0000_i1035" width="100%"/>
       </p>
      </div>
      <p class="caption">
       <b>Figure 3.1.</b> An   SLD-tree.
      </p>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <div class="extract figure" id="3.2">
  <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
   <tbody>
    <tr>
     <td align="left" class="AutoStyle42" valign="top">
      <div class="AutoStyle20">
       <p class="med-figure AutoStyle07">
        <img src="img/part_i/image024.svg" v:shapes="_x0000_i1036" width="100%"/>
       </p>
      </div>
      <p class="med-caption">
       <b>Figure 3.2.</b> An SLD-tree with infinite branches.
      </p>
     </td>
    </tr>
   </tbody>
  </table>
 </div>
 <br clear="ALL">
  <p class="tekst">
   An SLD-tree for the query
  </p>

<div class="extract swish" id="3.1.3a">
<pre class="swish query" id="query3.1.3a">
?-brother_of(peter,B).</pre>
</div>

  <p class="tekst">
   is depicted in fig. 3.2. If we descend this tree taking the left branch at every node, we will never reach a leaf. On the other hand, if we take the right branch at every node, we almost immediately reach a success branch. Taking right branches instead of left branches in an SLD-tree corresponds to searching the clauses from bottom to top. The same effect would be obtained by reversing the order of the clauses in the program, and the SLD-tree clearly shows that this is enough to prevent Prolog from looping on this query. This is a rule of thumb that applies to most cases: <i>put non-recursive clauses before recursive ones</i>.
  </p>
  <p class="sektie">
   However, note that, even after this modification, the program still has some problems. For one thing, the query <tt>?-brother_of(peter,B)</tt> will be answered an infinite number of times, because there are infinitely many refutations of it. But, even worse, consider a query that does <b>not</b> have an answer, like
  </p>

<div class="extract swish" id="3.1.4">
<pre class="swish query" id="query3.1.4">?-brother_of(peter,maria).</pre>
</div>

  <p class="sektie">
   No matter the order in which the SLD-tree is descended, Prolog will never discover that the query has in fact no answer, <i>simply because the SLD-tree is infinite</i>. So, one should be careful with programs like the above, which define a predicate to be <i>symmetric</i>.
  </p>
  <div class="extract figure" id="3.3">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle04" valign="top">
       <div class="AutoStyle05">
        <p class="figure">
         <img src="img/part_i/image026.svg" v:shapes="_x0000_i1037" width="100%"/>
        </p>
       </div>
       <p class="caption">
        <b>Figure 3.3.</b> An   SLD-tree with infinite branches and expanding resolvents.
       </p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <p class="sektie">
   Another property of predicates which can cause similar problems is <i>transitivity</i>.Consider the following program:
  </p>

<div class="extract swish" id="3.1.4_2">
<pre class="source swish temp AutoStyle03" data-variant-id="group-2" id="swish.3.1.4">
brother_of(paul,peter).
brother_of(peter,adrian).
brother_of(X,Y):-brother_of(X,Z),brother_of(Z,Y).
</pre>
</div>

  <p class="tekst">
   The third clause ensures that <tt>?-brother_of(paul,adrian)</tt> is a logical consequence of the program. The SLD-tree for the query
  </p>

<div class="extract swish" id="3.1.6">
<pre class="swish query" id="query3.1.6">?-brother_of(paul,B).</pre>
</div>

  <p class="tekst">
   is depicted in fig. 3.3. Not only is this SLD-tree infinite, but the resolvents get longer and longer on deeper levels in the tree.
  </p>
  <p class="sektie">
   We have encountered two problems with SLD-resolution: (<i>i</i>) we might never reach a success branch in the SLD-tree, because we get &lsquo;trapped&rsquo; into an infinite subtree, and (<i>ii</i>) any infinite SLD-tree causes the inference engine to loop if no (more) answers are to be found. The first problem means that Prolog is <i>incomplete</i>: some logical consequences of a program may never be found.&nbsp;Note carefully that this incompleteness is <b>not</b> caused by the inference rule of resolution, which is refutation complete. Indeed, for any program and any query, all the possible answers will be represented by success branches in the SLD-tree. The incompleteness of SLD-resolution&nbsp;is caused by the way the SLD-tree is searched.
  </p>
  <p class="sektie">
   There exists a solution to this problem: if we descend the tree layer by layer rather than branch-by-branch, we will find any leaf before we descend to the next level. However, this also means that we must keep track of <b>all</b> the resolvents on a level, instead of just a single one. Therefore, this <i>breadth-first</i> search&nbsp;strategy needs much more memory than the <i>depth-first</i>&nbsp;strategy used by Prolog. In fact, Prolog&rsquo;s incompleteness was a deliberate design choice, sacrifying completeness in order to obtain an efficient use of memory
   <span class="CustomFootnote">
    <a href="#_ftn7" name="_ftnref7" title="">
     <span class="MsoFootnoteReference">
      <span class="AutoStyle13">
       <span class="AutoStyle14">
        [7]
       </span>
      </span>
     </span>
    </a>
   </span>
   . As we saw above, this problem can often be avoided by ordering the clauses in the program in a specific way (which means that we have to take the procedural meaning of the program into account).
  </p>
  <p class="sektie">
   As for the second problem, we already saw that this is due to the semi-decidability of full clausal logic, which means that there is no general solution to it.
  </p>
<div class="extract exercise" id="3.2">
  <div class="AutoStyle06">
   <p class="exercise AutoStyle07">
    <i>Exercise 3.2.</i> Draw the SLD-tree for the following program:
   </p>

<div class="extract swish" id="2.3.2_3">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.2.3.2">
list([]).
list([_H|T]):-list(T).
</pre>
</div>

   <p class="exercise AutoStyle07">
    and the query
   </p>

<div class="extract swish" id="3.1.6a">
<pre class="swish query" id="query3.1.6a">?-list(L).</pre>
</div>

  </div>
</div>
  <h3 id="pruning_the_search_by_means_of_cut">
   3.2&nbsp;&nbsp;&nbsp;Pruning the search by means of cut
  </h3>
  <p class="sektie1">
   As shown in the previous section, Prolog constantly searches the clauses in a program in order to reach a success branch in the SLD-tree for a query. If a failure branch is reached (i.e., a non-empty resolvent which cannot be reduced any further), Prolog has to &lsquo;unchoose&rsquo; the last-chosen program clause, and try another one. This amounts to going up one level in the SLD-tree, and trying the next branch to the right. This process of reconsidering previous choices is called <i>backtracking</i>. Note that backtracking requires that all previous resolvents are remembered for which not all alternatives have been tried yet, together with a pointer to the most recent program clause that has been tried at that point. Because of Prolog&rsquo;s depth-first search&nbsp;strategy, we can easily record all previous resolvents in a <i>goal stack</i>: backtracking&nbsp;is then implemented by popping the upper resolvent from the stack, and searching for the next program clause to resolve with.
  </p>
  <p class="sektie">
   As an illustration, consider again the SLD-tree in fig. 3.1. The resolvent&nbsp;in the middle branch
  </p>
  <p class="p-el">
   :-teaches(peter,expert_systems)
  </p>
  <p class="tekst">
   cannot be reduced any further, and thus represents a failure branch. At that point, the stack contains (top-down) the previous resolvents
  </p>
  <p class="p-el">
   :-follows(S,C),teaches(peter,C)<br>
   ?-student_of(S,peter)
</p>
  <p class="tekst">
   The top one is popped from the stack; it has been most recently resolved with <tt>follows(paul,expert_systems)</tt>, so we continue searching the program from that clause, finding <tt>follows(maria,ai_techniques)</tt> as the next alternative.
  </p>
  <p class="sektie">
   A node in the SLD-tree which is not a leaf is called a <i>choice point</i>, because the subtree rooted at that node may contain several success branches, each of which may be reached by a different choice for a program clause to resolve with. Now, suppose a subtree contains only one success branch, yielding an answer to our query. If we want to know whether there are any alternative answers, we can force Prolog to backtrack. However, since the rest of the subtree does not contain any success branches, we might as well skip it altogether, thus speeding up backtracking. But how do we tell Prolog that a subtree contains only one success branch? For this, Prolog provides a control device which is called <i>cut</i>&nbsp;(written <tt>!</tt>), because it cuts away (or prunes) part of the SLD-tree.
  </p>
  <div class="extract figure" id="3.4">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle04" valign="top">
       <div class="AutoStyle20">
        <p class="med-figure AutoStyle07">
         <img src="img/part_i/image028.svg" v:shapes="_x0000_i1038" width="100%"/>
        </p>
       </div>
       <p class="med-caption">
        <b>Figure 3.4.</b> SLD-tree for the query<br>
        <tt>?-parent(john,C)</tt>.
</p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <p class="sektie">
   To illustrate the effect of cut, consider the following program.
  </p>

<div class="extract swish" id="3.2.2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.2.2">
parent(X,Y):-father(X,Y).
parent(X,Y):-mother(X,Y).
father(john,paul).
mother(mary,paul).
</pre>
</div>

  <p class="tekst">
   The SLD-tree for the query
  </p>

<div class="extract swish" id="3.2.3_2">
<pre class="swish query" id="query3.2.3">?-parent(john,C).</pre>
</div>

  <p class="tekst">
   is given in fig. 3.4. The answer given by Prolog is { <tt>C</tt>
   <span class="AutoStyle09">
    &rarr;
   </span>
   <tt>paul</tt> }. By asking whether there are any other answers, we force Prolog to backtrack to the most recent choice point for which there are any alternatives left, which is the root of the SLD-tree (i.e. the original query). Prolog tries the second clause for <tt>parent</tt>, but discovers that this leads to a failure branch.
  </p>
  <p class="sektie">
   Of course, <b>we</b> know that this backtracking step did not make sense: if John is a father of anyone, he can&rsquo;t be a mother. We can express this by adding a cut to the first <tt>parent</tt> clause:
  </p>

<div class="extract swish" id="3.2.3">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.2.3" query-id="query3.2.3">
parent(X,Y):-father(X,Y),!.
parent(X,Y):-mother(X,Y).
father(john,paul).
mother(mary,paul).
</pre>
</div>

  <div class="extract figure" id="3.5">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle04" valign="top">
       <div class="AutoStyle20">
        <p class="med-figure AutoStyle07">
         <img src="img/part_i/image030.svg" v:shapes="_x0000_i1039" width="100%"/>
        </p>
       </div>
       <p class="med-caption">
        <b>Figure 3.5.</b> The effect of cut.
       </p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <p class="tekst">
   The cut says: <i>once you&rsquo;ve reached me, stick to all the variable substitutions you&rsquo;ve found after you entered my clause</i>. That is: don&rsquo;t try to find any alternative solutions to the literals left of the cut, and also: don&rsquo;t try any alternative clauses for the one in which the cut is found. Given this modified program, the SLD-tree for the same query is shown in fig. 3.5. Since <tt>!</tt> is true by definition, the resolvent <tt>:-!</tt> reduces to the empty clause. The shaded part represents the part of the SLD-tree which is pruned as a result of the cut. That is: every alternative at choice points below and including <tt>?-parent(john,C)</tt>, which are on the stack when the cut is reached, are pruned. Note carefully that a cut does not prune <b>every</b> choice point. First of all, pruning does not occur above the choice point containing the head of the clause in which the cut is found. Secondly, choice points created by literals to the right of the cut, which are below the cut in the SLD-tree but are not yet on the stack when the cut is reached, are not pruned either (fig. 3.6).
  </p>
  <p class="sektie">
   A cut is harmless if it does not cut away subtrees containing success branches.&nbsp;If a cut prunes success branches, then some logical consequences of the program are not returned as answers, resulting in a procedural meaning different from the declarative meaning. Cuts of the first kind are called <i>green</i> cuts, while cuts of the second kind are called <i>red</i> cuts. A green cut merely stresses that the conjunction of literals to its left is <i>deterministic</i>: it does not give alternative solutions. In addition, it signifies that if those literals give a solution, the clauses below it will not result in any alternatives.
  </p>
  <p class="sektie">
   This seems to be true for the above program: John is the father of only one child, and no-one is both a father and a mother. However, note that we only analysed the situation with regard to a particular query. We can show that the cut is in fact red by asking the query
  </p>

<div class="extract swish" id="3.2.3a">
<pre class="swish query" id="query3.2.3a" source-id="swish.3.2.2 swish.3.2.3">?-parent(P,paul).</pre>
</div>

  <p class="tekst">
   The answer { <tt>P</tt>
   <span class="AutoStyle09">
    &rarr;
   </span>
   <tt>mary</tt> } is pruned by the cut (fig. 3.7). That is, the literal <tt>father(X,Y)</tt> left to the cut is only deterministic if <tt>X</tt> is <i>instantiated</i>&nbsp;(is substituted by a non-variable value).
  </p>
  <div class="extract figure" id="3.6">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle04" valign="top">
       <div class="AutoStyle20">
        <p class="med-figure AutoStyle07">
         <img src="img/part_i/image032.svg" v:shapes="_x0000_i1040" width="100%"/>
        </p>
       </div>
       <p class="med-caption">
        <b>Figure 3.6.</b> Cut prunes away alternative solutions for <tt>s</tt>,   but not for <tt>t</tt>. Also, choice points   above <tt>:‑q(X,Y)</tt> are not pruned.
       </p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <p class="sektie">
   Note that success branches are also pruned for the first query if John has several children:
  </p>

<div class="extract swish" id="3.2.4">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.2.4" query-id="query3.2.3a">
parent(X,Y):-father(X,Y),!.
parent(X,Y):-mother(X,Y).
father(john,paul).
father(john,peter).
mother(mary,paul).
mother(mary,peter).
</pre>
</div>

  <p class="tekst">
   The SLD-tree for the query
  </p>

<div class="extract swish" id="3.2.4_2">
<pre class="swish query" id="query3.2.4">?-parent(john,C).</pre>
</div>

  <p class="tekst">
   is given in fig. 3.8. Indeed, the second answer { <tt>C</tt>
   <span class="AutoStyle09">
    &rarr;
   </span>
   <tt>peter</tt> } is pruned by the cut. This clearly shows that the effect of a cut is not only determined by the clause in which it occurs but also by other clauses. Therefore, the effect of a cut is often hard to understand.
  </p>
  <div class="extract figure" id="3.7">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle04" valign="top">
       <div class="AutoStyle20">
        <p class="small-figure AutoStyle07">
         <img src="img/part_i/image034.svg" v:shapes="_x0000_i1041" width="100%"/>
        </p>
       </div>
       <p class="small-caption">
        <b>Figure 3.7.</b> A success branch is pruned.
       </p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <div class="extract figure" id="3.8">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle04" valign="top">
       <div class="AutoStyle20">
        <p class="med-figure AutoStyle07">
         <img src="img/part_i/image036.svg" v:shapes="_x0000_i1042" width="100%"/>
        </p>
       </div>
       <p class="med-caption">
        <b>Figure 3.8.</b> Another   success branch is pruned.
       </p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <p class="sektie">
   Programs with cuts are not only difficult to understand; this last example also shows that their procedural interpretation&nbsp;(the set of answers they produce to a query) may be different from their declarative interpretation&nbsp;(the set of its logical consequences). Logically, cut has no meaning: it always evaluates to <b>true</b>, and therefore it can always be added or removed from the body of a clause without affecting its declarative interpretation. Procedurally, cut may have many effects, as the preceding examples show. This<br>
   <br>
   </p>
  <p class="sektie AutoStyle43">
   &nbsp;incompatibility between declarative and procedural interpretation makes it a very problematic concept.&nbsp;Much research in Logic Programming aims at replacing it by higher-level constructs which have cleaner declarative meanings and which are easier to understand. The most important of these will be considered in the next two sections.
  </p>
<div class="extract exercise" id="3.3">
  <div class="AutoStyle06">
   <p class="exercise AutoStyle07">
    <i>Exercise 3.3.</i> Draw the SLD-tree for the query
   </p>

<div class="extract swish" id="3.2.ex3.3">
<pre class="swish query" id="query3.2.ex3.3">?-likes(A,B).</pre>
</div>

   <p class="exercise AutoStyle07">
    given the following program:
   </p>

<div class="extract swish" id="3.2.ex3.3_2">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="swish.3.2.ex3.3" query-id="query3.2.ex3.3">
likes(peter,Y):-friendly(Y).
likes(T,S):-student_of(S,T).
student_of(maria,peter).
student_of(paul,peter).
friendly(maria).
</pre>
</div>

   <p class="exercise AutoStyle07">
    Add a cut in order to prune away one of the answers { <tt>A</tt>
    <span class="AutoStyle09">
     &rarr;
    </span>
    <tt>peter</tt>, <tt>B</tt>
    <span class="AutoStyle09">
     &rarr;
    </span>
    <tt>maria</tt> }, and indicate the result in the SLD-tree. Can this be done without pruning away the third answer?
   </p>
  </div>
</div>
  <h3 id="negation_as_failure">
   3.3&nbsp;&nbsp;&nbsp;Negation as failure
  </h3>
  <p class="sektie1">
   The following program computes the maximum of two integers:
  </p>

<div class="extract swish" id="3.3.1">
  <pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.3.1">
max(M,N,M):- M &gt;= N.
max(M,N,N):- M =&lt; N.
</pre>
</div>

  <p class="tekst">
   <tt>&gt;=</tt>&nbsp;and <tt>=&lt;</tt>&nbsp;are built-in predicates with meaning &lsquo;greater than or equal&rsquo; and &lsquo;less than or equal&rsquo;, respectively
   <span class="CustomFootnote">
    <a href="#_ftn8" name="_ftnref8" title="">
     <span class="MsoFootnoteReference">
      <span class="AutoStyle13">
       <span class="AutoStyle14">
        [8]
       </span>
      </span>
     </span>
    </a>
   </span>
   . Declaratively, the program captures the intended meaning, but procedurally there are two different ways to solve queries of the form <tt>?-max(N,N,M)</tt>. The reason for this is that the bodies of the two clauses are not exclusive: they both succeed if the first two values of the <tt>max</tt> predicate are equal. We could of course remove one of the equality symbols, but suppose that we use a cut instead:
  </p>

<div class="extract swish" id="3.3.2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.3.2">
max(M,N,M):- M &gt;= N,!.
max(_M,N,N).
</pre>
</div>

  <p class="tekst">
   With a red cut, this program can only be understood procedurally. The question is: does the procedural meaning correspond to the intended meaning? Perhaps surprisingly, the answer is no! For instance, the query
  </p>

<div class="extract swish" id="3.3.1">
<pre class="swish query" id="query3.3.1" source-id="swish.3.3.1 swish.3.3.2">
?-max(5,3,3).
</pre>
</div>

  <p class="tekst">
   succeeds: the cut is never reached, because the literal in the query does not unify with the head of the first clause. The second program is in fact a very bad program: the declarative and procedural meanings differ, and <b>neither</b> of them captures the intended meaning.
  </p>
<div class="extract exercise" id="3.4">
       <div class="AutoStyle06">
        <p class="exercise AutoStyle07">
         <i>Exercise 3.4.</i> Show that this cut is red, by drawing an SLD-tree   in which a success branch is pruned.
        </p>
       </div>
</div>
  <p class="sektie">
   The procedural meaning of the program would be correct if its use is restricted to queries with uninstantiated third argument. It illustrates a very common use of cut: to ensure that the bodies of the clauses are mutually exclusive. In general, if we have a program of the form
  </p>
  <p class="p-el">
   p:-q,!,r.<br>
   p:-s.
</p>
  <p class="tekst">
   its meaning is something like
  </p>
  <p class="p-el">
   p:-q,r.<br>
   p:-not_q,s.
</p>
  <p class="tekst">
   How should <tt>not_q</tt> be defined, in order to make the second program work? If <tt>q</tt> succeeds, <tt>not_q</tt> should fail. This is expressed by the following clause:
  </p>
  <p class="p-el">
   not_q:-q,fail
  </p>
  <p class="tekst">
   where <tt>fail</tt>&nbsp;is a built-in predicate, which is always <b>false</b>. If <tt>q</tt> fails, <tt>not_q</tt> should succeed. This can be realised by the program
  </p>
  <p class="p-el">
   not_q:-q,!,fail.<br>
   not_q.
</p>
  <p class="tekst">
   The cut in the first clause is needed to prevent backtracking to the second clause when <tt>q</tt> succeeds.
  </p>
  <p class="sektie">
   This approach is not very practical, because it only works for a single proposition symbol, without variables. We would like to treat the literal to be negated as a parameter, as in
  </p>
  <p class="p-el">
   not(Goal):- /* execute Goal, */ !,fail.<br>
   not(Goal).
  </p>
  <p class="tekst">
   The problem now is to execute a goal which is passed to the predicate <tt>not</tt> as a term. Prolog provides two facilities for this. One is the built-in predicate <tt>call</tt>, which takes a goal as argument and succeeds if and only if execution of that goal succeeds. The second facility
   <span class="CustomFootnote">
    <a href="#_ftn9" name="_ftnref9" title="">
     <span class="MsoFootnoteReference">
      <span class="AutoStyle13">
       <span class="AutoStyle14">
        [9]
       </span>
      </span>
     </span>
    </a>
   </span>
   is merely a shorthand for this: instead of writing <tt>call(Goal)</tt>, one may simply write <tt>Goal</tt>, as in
  </p>

<div class="extract swish" id="3.3.2_2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.3.2" query-text="?-not(true). ?-not(false).">
not(Goal):- Goal,!,fail.
not(_Goal).
</pre>
</div>

  <p class="tekst">
   This is a slight abuse of the syntax rules, because a variable (a term) occurs in a position where only atoms are allowed.&nbsp;As long as the variable is instantiated to a goal before it is reached, this will, however, cause no problem (if it is not correctly instantiated, Prolog will generate an error-message). Predicates like <tt>not</tt> and <tt>call</tt> are called <i>meta-predicates</i>, that take formulas from the same logical language in which they are written as arguments. As we will see in later chapters, meta-predicates play an important role in this book.
  </p>
  <div class="extract figure" id="3.9">
   <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
    <tbody>
     <tr>
      <td align="left" class="AutoStyle42" valign="top">
       <div class="AutoStyle20">
        <p class="med-figure AutoStyle07">
         <img src="img/part_i/image038.svg" v:shapes="_x0000_i1043" width="100%"/>
        </p>
       </div>
       <p class="med-caption">
        <b>Figure 3.9.</b> SLD-tree with <tt>not</tt>.
       </p>
      </td>
     </tr>
    </tbody>
   </table>
  </div>
  <br clear="ALL">
   <div class="extract figure" id="3.10">
    <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
     <tbody>
      <tr>
       <td align="left" class="AutoStyle42" valign="top">
        <div class="AutoStyle20">
         <p class="small-figure AutoStyle07">
          <img src="img/part_i/image040.svg" v:shapes="_x0000_i1044" width="70%"/>
         </p>
        </div>
        <p class="small-caption">
         <b>Figure 3.10.</b> Equivalent   SLD-tree with cut.
        </p>
       </td>
      </tr>
     </tbody>
    </table>
   </div>
   <br clear="ALL">
    <p class="sektie">
     We illustrate the operation of <tt>not</tt> by means of the following propositional program:
    </p>
    <p class="p-el">
     p:-q,r.<br>
     p:-not(q),s.<br>
     s.
</p>
    <p class="tekst">
     and the query <tt>?-p</tt>. The SLD-tree is shown in fig. 3.9. The first clause for <tt>p</tt> leads to a failure branch, because <tt>q</tt> cannot be proved. The second clause for <tt>p</tt> is tried, and <tt>not(q)</tt> is evaluated by trying to prove <tt>q</tt>. Again, this fails, which means that the second clause for <tt>not</tt> is tried, which succeeds. Thus, <tt>not(q)</tt> <i>is proved by failing to prove</i> <tt>q</tt>! Therefore, this kind of negation is called <i>negation as failure</i>.
    </p>
    <p class="sektie">
     Fig. 3.9 shows, that Prolog tries to prove <tt>q</tt> twice. Consequently, the program with <tt>not</tt> is slightly less efficient than the version with cut:
    </p>
    <p class="p-el">
     p:-q,!,r.<br>
     p:-s.<br>
     s.
</p>
    <p class="tekst">
     which leads to the SLD-tree shown in fig. 3.10. Here, <tt>q</tt> is tried only once. However, in general we prefer the use of <tt>not</tt>, because it leads to programs of which the declarative meaning corresponds more closely to the procedural meaning.
    </p>
    <div class="extract figure" id="3.11">
     <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
      <tbody>
       <tr>
        <td align="left" class="AutoStyle04" valign="top">
         <div class="AutoStyle20">
          <p class="med-figure AutoStyle07">
           <img src="img/part_i/image042.svg" v:shapes="_x0000_i1045" width="100%"/>
          </p>
         </div>
         <p class="med-caption">
          <b>Figure 3.11.</b> <tt>:-not(q)</tt> fails because <tt>:-q</tt> succeeds.
         </p>
        </td>
       </tr>
      </tbody>
     </table>
    </div>
    <p class="sektie">
     In the following program, <tt>:-not(q)</tt> fails because <tt>:-q</tt> succeeds:
    </p>
    <p class="p-el">
     p:-not(q),r.<br>
     p:-q.<br>
     q.<br>
     r.
</p>
    <p class="tekst">
     The SLD-tree for the query <tt>?-p</tt> is shown in fig. 3.11. Since <tt>q</tt> succeeds, <tt>fail</tt> ensures that <tt>not(q)</tt> fails. The cut is needed to ensure that everything following the <tt>not</tt> is pruned, even if it contains a success branch.
    </p>
    <p class="sektie">
     The implementation of <tt>not</tt>&nbsp;illustrated above can lead to problems if variables are involved. Take a look at the following program:
    </p>

<div class="extract swish" id="3.3.3">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.3.3" query-text="?-bachelor(fred). ?-bachelor(peter).">
bachelor(X):-not(married(X)),man(X).
man(fred).
man(peter).
married(fred).
</pre>
</div>

<div class="extract exercise" id="3.5">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.5.</i> Draw the SLD-trees for the queries <tt>?-bachelor(fred)</tt> and<br>
      <tt>?-bachelor(peter)</tt>.
</p>
    </div>
</div>
    <div class="extract figure" id="3.12">
     <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
      <tbody>
       <tr>
        <td align="left" class="AutoStyle04" valign="top">
         <div class="AutoStyle05">
          <p class="figure">
           <img src="img/part_i/image044.svg" v:shapes="_x0000_i1046" width="100%"/>
          </p>
         </div>
         <p class="caption">
          <b>Figure 3.12.</b> There are no bachelors?!
         </p>
        </td>
       </tr>
      </tbody>
     </table>
    </div>
    <p class="sektie">
     Consider the query
    </p>

<div class="extract swish" id="3.3.2_3">
<pre class="query" id="query3.3.2"><span class="swish query">?-bachelor(X).</span></pre>
</div>

    <p class="tekst">
     for which the SLD-tree is depicted in fig. 3.12. According to negation as failure, Prolog tries to prove <tt>not(married(X))</tt> by trying <tt>married(X)</tt> first. Since this succeeds for <tt>X</tt> = <tt>fred</tt>, the cut is reached and the success branch to the right (representing the correct answer { <tt>X</tt>
     <span class="AutoStyle09">
      &rarr;
     </span>
     <tt>peter</tt> }) is pruned. Thus, <tt>:‑not(married(X))</tt> fails because <tt>:‑married(X)</tt> succeeds for one value of <tt>X</tt>. That is, <tt>not(married(X))</tt> is interpreted as &lsquo;it is false that somebody is married&rsquo;, or equivalently, &lsquo;nobody is married&rsquo;. But this means that the clause
    </p>
    <p class="p-el">
     bachelor(X):-not(married(X)),man(X)
    </p>
    <p class="tekst">
     is interpreted as &lsquo; <i>X</i> is a bachelor if nobody is married and <i>X</i> is a man&rsquo;, which is of course not as intended.
    </p>
    <div class="extract infobox" id="negation_as_failure_vs_logical_negation">
     <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
      <tbody>
       <tr>
        <td align="left" class="AutoStyle04" valign="top">
         <div class="AutoStyle31">
          <p class="inter-title AutoStyle32">
           Negation as failure vs. logical negation
          </p>
          <p class="intermezzo AutoStyle32">
           Negation as failure is not the same as logical negation: if we   cannot prove <tt>q</tt>, we know that <tt>q</tt> is not a logical consequence of the   program, but this does not mean that its negation <tt>:-q</tt> is a logical consequence of the program. Adopting   negation as failure is similar to saying &lsquo;I cannot prove that God exists,   therefore I conclude God does not exist&rsquo;. It is a kind of reasoning that is   applicable in some contexts, but inadequate in others. Logical negation can   only be expressed by<br>
           indefinite clauses, as in the following program:
</p>
          <p align="left" class="intermezzo AutoStyle44">
           <tt>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;p:-q,r.<br>
            &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;p;q:-s.<br>
            &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;s.</tt>
          </p>
          <p class="intermezzo AutoStyle33">
           Semantically speaking, if we don&rsquo;t have enough information to   conclude that a formula <i>F</i> is true   or false, the truth value of its logical negation will also be undecided, but <tt>not</tt> (<i>F</i>) will be true. This property of negation as failure can be very   useful when dealing with exceptions to rules: if we don&rsquo;t know that something   is an exception to a rule, we assume that it&rsquo;s not, so we only have to list   the exceptions and not the normal cases. This approach will be extensively   discussed in Chapter 8 on reasoning with incomplete information.
          </p>
         </div>
        </td>
       </tr>
      </tbody>
     </table>
    </div>
    <p class="sektie">
     Thus, if <tt>G</tt> is instantiated&nbsp;to a goal containing variables at the time <tt>not(G)</tt> is called, the result may be not in accordance with negation as failure. <i>It is the programmer&rsquo;s responsibility to avoid this.</i> A simple remedy that will often work is to ensure the grounding of <tt>G</tt> by literals preceding <tt>not(G)</tt> in the body of the clause, i.e.
    </p>

<div class="extract swish" id="3.3.3a">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.3.3a" query-text="?-bachelor(X).">
bachelor(X):-man(X),not(married(X)).
man(fred).
man(peter).
married(fred).
</pre>
</div>

<div class="extract exercise" id="3.6">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.6.</i> Show that the modified program produces the right answer, by drawing the SLD-tree for the query <tt>?-bachelor(X)</tt>.
     </p>
    </div>
</div>
    <p class="sektie">
     Thus, we see that changing the order of the literals in the body of a clause does not only affect the order in which answers to a query are found, but it may also change the set of answers! Of course, this is very much against the spirit of declarative programming, because the declarative interpretation&nbsp;of a clause does not depend on the order of the literals. Therefore, some Prolog interpreters provide a mechanism which defers the evaluation of <tt>not(G)</tt> until <tt>G</tt> is ground. However, with standard Prolog it is the programmer&rsquo;s duty to ensure that <tt>not</tt> is never called with a non-ground argument.
    </p>
    <p class="sektie">
     Let&rsquo;s summarise the points made about negation in Prolog. It is often used to ensure that only one of several possible clauses is applicable. The same effect can be achieved by means of cut, but in general we prefer the use of <tt>not</tt>, although it is somewhat less efficient
     <span class="CustomFootnote">
      <a href="#_ftn10" name="_ftnref10" title="">
       <span class="MsoFootnoteReference">
        <span class="AutoStyle13">
         <span class="AutoStyle14">
          [10]
         </span>
        </span>
       </span>
      </a>
     </span>
     . <tt>not</tt> is supplied by Prolog as a meta-predicate (i.e. a predicate which takes formulas from the same logical language in which it is written as arguments). It is only a partially correct implementation of negation as failure, since it does not operate correctly when its argument is a goal containing variables.
    </p>
    <h3 id="other_uses_of_cut">
     3.4&nbsp;&nbsp;&nbsp;Other uses of cut
    </h3>
    <p class="sektie1">
     Consider the following propositional program:
    </p>
    <p class="p-el">
     p:-q,r,s,!,t.<br>
     p:-q,r,u.<br>
     q.<br>
     r.<br>
     u.
</p>
<div class="extract exercise" id="3.7">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.7.</i> Show that the query <tt>?-p</tt> succeeds, but that <tt>q</tt> and <tt>r</tt> are tried twice.
     </p>
    </div>
</div>
    <p class="tekst">
     This inefficiency can be avoided by putting <tt>s,!</tt> at the beginning of the body of the first clause. However, in full clausal logic the goals preceding <tt>s</tt> might supply necessary variable bindings, which requires them to be called first. A possible solution would be the introduction of an extra proposition symbol:
    </p>
    <p class="p-el">
     p:-q,r,if_s_then_t_else_u.<br>
     if_s_then_t_else_u:-s,!,t.<br>
     if_s_then_t_else_u:-u.
</p>
<div class="extract exercise" id="3.8">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.8.</i> Show that <tt>q</tt> and <tt>r</tt> are now tried only once.
     </p>
    </div>
</div>
    <p class="sektie">
     Just as we did with <tt>not</tt>, we can rewrite this new proposition symbol to a generally applicable meta-predicate:
    </p>
    <p class="p-el">
     if_then_else(S,T,U):-S,!,T.<br>
     if_then_else(S,T,U):-U.
</p>
    <p class="tekst">
     Note that we can nest applications of <tt>if_then_else</tt>, for instance
    </p>
    <p class="pi-el">
     if_then_else_else(P,Q,R,S,T):-<br>
     if_then_else(P,Q,if_then_else(R,S,T)).
</p>
    <p class="tekst">
     Unfolding the definition of <tt>if_then_else</tt> yields
    </p>
    <p class="p-el">
     if_then_else_else(P,Q,R,S,T):-P,!,Q.<br>
     if_then_else_else(P,Q,R,S,T):-R,!,S.<br>
     if_then_else_else(P,Q,R,S,T):-T.
</p>
    <p class="tekst">
     which clearly shows the meaning of the predicate: &lsquo;if <i>P</i> then <i>Q</i> else if <i>R</i> then <i>S</i> else <i>T</i> &rsquo;. This resembles the CASE-statement of procedural languages, only the above notation is much more clumsy. Most Prolog interpreters provide the notation <tt>P-&gt;Q;R</tt> for if-then-else; the nested variant then becomes <tt>P-&gt;Q;(R-&gt;S;T)</tt>. The parentheses are not strictly necessary, but in general the outermost if-then-else literal should be enclosed in parentheses. A useful lay-out is shown by the following program:
    </p>
    <p class="pi-el">
     diagnosis(Patient,Condition):-<br>
     temperature(Patient,T),<br>
     ( T=&lt;37&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;blood_pressure(Patient,Condition)<br>
     ; T&gt;37,T&lt;38&nbsp;-&gt;&nbsp;Condition=ok<br>
     ; otherwise&nbsp;-&gt;&nbsp;diagnose_fever(Patient,Condition)<br>
     ).
</p>
    <p class="tekst">
     <tt>otherwise</tt>&nbsp;is always assigned the truthvalue <b>true</b>, so the last rule applies if all the others fail.
    </p>
    <p class="sektie">
     <tt>not</tt> and if-then-else show that many uses of cut can be replaced by higher-level constructs, which are easier to understand. However, this is not true for every use of cut. For instance, consider the following program:
    </p>
    <p class="pi-eerst">
     play(Board,Player):-<br>
     lost(Board,Player).
</p>
    <p class="pi-laatst">
     play(Board,Player):-<br>
     find_move(Board,Player,Move),<br>
     make_move(Board,Move,NewBoard),<br>
     next_player(Player,Next),<br>
     play(NewBoard,Next).
</p>
    <p class="tekst">
     This program plays a game by recursively looking for best moves. Suppose one game has been finished; that is, the query <tt>?-play(Start,First)</tt> (with appropriate instantiations of the variables) has succeeded. As usual, we can ask Prolog whether there are any alternative solutions. Prolog will start backtracking, looking for alternatives for the most recent move, then for the move before that one, and so on. That is, <i>Prolog has maintained all previous board situations, and every move made can be undone</i>. Although this seems a desirable feature, in reality it is totally unpractical because of the memory requirements: after a few moves you would get a stack overflow. In such cases, we tell Prolog not to reconsider any previous moves, by placing a cut just before the recursive call. This way, we pop the remaining choice points from the stack before entering the next recursion. In fact, this technique results in a use of memory similar to that of iterative loops in procedural languages.
    </p>
    <p class="sektie">
     Note that this only works if the recursive call is the last call in the body. In general, it is advisable to write your recursive predicates like <tt>play</tt> above: the non-recursive clause before the recursive one, and the recursive call at the end of the body. A recursive predicate written this way is said to be <i>tail recursive</i>.&nbsp;If in addition the literals before the recursive call are deterministic (yield only one solution), some Prolog interpreters may recognise this and change recursion into iteration. This process is called <i>tail recursion optimisation</i>. As illustrated above, you can force this optimisation by placing a cut before the recursive call.
    </p>
    <h3 id="arithmetic_expressions">
     3.5&nbsp;&nbsp;&nbsp;Arithmetic expressions
    </h3>
    <p class="sektie1">
     In Logic Programming, recursion&nbsp;is the only looping control structure.&nbsp;Consequently, recursive datatypes&nbsp;such as lists can be expressed very naturally. Natural numbers also have a recursive nature: &lsquo;0 is a natural number, and if <i>X</i> is a natural number, then the successor of <i>X</i> is also a natural number&rsquo;. In Prolog, this is expressed as
    </p>

<div class="extract swish" id="3.5.0">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.5.0" query-text="?-nat(s(s(0))).">
nat(0).
nat(s(X)):-nat(X).
</pre>
</div>

    <p class="tekst">
     Addition of natural numbers is defined in terms of successors:
    </p>

<div class="extract swish" id="3.5.1">
<pre class="source swish temp AutoStyle03" data-variant-id="group-2" id="swish.3.5.1" query-text="?-add(s(s(0)),Y,s(s(s(0)))).">
add(0,X,X).
add(s(X),Y,s(Z)):-add(X,Y,Z).
</pre>
</div>

    <p class="tekst">
     The following query asks for the sum of two and three:
    </p>

<div class="extract swish" id="3.5.1_2">
<pre class="swish query" id="query3.5.1">
?-add(s(s(0)),s(s(s(0))),Z).
</pre>

    <p class="p-el">
     Z = s(s(s(s(s(0)))))
    </p>
    <p class="tekst">
     We can also find an <i>X</i> such that the sum of <i>X</i> and <i>Y</i> is <i>Z</i> (i.e., subtract <i>Y</i> from <i>Z</i>):
    </p>

<div class="extract swish" id="3.5.1_3">
<pre class="swish query" id="query3.5.1">
?-add(X,s(s(s(0))),s(s(s(s(s(0)))))).
</pre>
</div>

    <p class="p-el">
     X = s(s(0))
    </p>
    <p class="tekst">
     We can even find all <i>X</i> and <i>Y</i> which add up to a given sum. Thus, this program is fully declarative. Similarly, multiplication is repeated addition:
    </p>

<div class="extract swish" id="3.5.2">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-2" id="swish.3.5.2" inherit-id="swish.3.5.1" query-text="?-mul(0,X,0). ?-mul(s(s(0)),s(s(s(0))),Z).">
mul(0,_X,0).
mul(s(X),Y,Z):-mul(X,Y,Z1),add(Y,Z1,Z).
</pre>
</div>

    <p class="sektie">
     There are two problems with this approach to representing and manipulating natural numbers. First, naming natural numbers by means of the constant symbol <tt>0</tt> and the functor <tt>s</tt> is very clumsy, especially for large numbers. Of course, it would be possible to write a translator from decimal notation to successor notation, and back. However, the second problem is more fundamental: multiplication as repeated addition is extremely inefficient compared to the algorithm for multiplicating numbers in decimal notation. Therefore, Prolog has built-in arithmetic facilities, which we will discuss now.
    </p>
    <p class="sektie">
     Consider the arithmetic expression <tt>5+7-3</tt>. Prolog will view this expression as the term <tt>+(5,-(7,3))</tt>, with the functors <tt>+</tt> and <tt>-</tt> written as infix operators. We want to <i>evaluate</i> this expression, i.e. we want a single numerical value which represents somehow the same number as the expression. A program for doing this would look something like
    </p>
    <p class="pi-eerst">
     is(V,E1+E2):-<br>
     is(V1,E1),is(V2,E2),<br>
     fast_add(V1,V2,V).
</p>
    <p class="pi">
     is(V,E1-E2):-<br>
     is(V1,E1,),is(V2,E2),<br>
     fast_sub(V1,V2,V).
</p>
    <p class="pi-laatst">
     is(E,E):-<br>
     number(E).
</p>
    <p class="tekst">
     Here, <tt>fast_add</tt> and <tt>fast_sub</tt> represent the fast, built-in procedures for addition and subtraction, which are not directly available to the user. These procedures are <b>not</b> reversible: its first two arguments must be instantiated. Therefore, the predicate <tt>is</tt> will include a test for groundness of its second argument (the arithmetic expression), and will quit with an error-message if this test fails.
    </p>
    <div class="extract infobox" id="operators">
     <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
      <tbody>
       <tr>
        <td align="left" class="AutoStyle04" valign="top">
         <div class="AutoStyle31">
          <p class="inter-title AutoStyle32">
           Operators
          </p>
          <p class="intermezzo AutoStyle33">
           In Prolog, functors and predicates are collectively called <i>operators</i>. An operator is declared by   the query <tt>?-op(Priority,Type,Name)</tt>,   where <tt>Priority</tt> is a number between 0   and 1200 (lower priority binds stronger), and <tt>Type</tt> is <tt>fx</tt> or <tt>fy</tt> for prefix, <tt>xfx</tt>, <tt>xfy</tt> or <tt>yfx</tt> for infix, and <tt>xf</tt> or <tt>yf</tt> for postfix. The <tt>x</tt> and <tt>y</tt> determine associativity: for instance, <tt>xfx</tt> means not associative (you cannot write <tt>X   op Y op Z</tt>, but must either write <tt>(X   op Y) op Z</tt> or <tt>X op (Y op Z)</tt>), <tt>xfy</tt> means right-associative (<tt>X op Y op Z</tt> means <tt>op(X,op(Y,Z))</tt>), and <tt>yfx</tt> means left-associative (<tt>X op Y op Z</tt> means <tt>op(op(X,Y),Z)</tt>). Every special   symbol of Prolog, such as &lsquo; <tt>:-</tt> &rsquo; and &lsquo; <tt>,</tt> &rsquo; (conjunction&nbsp;in the body of a clause), is a predefined   operator. The interpretation of operators can be visualised by means of the   predicate <tt>display</tt>, which writes a   term without operators. For instance,<br>
           the query <tt>?-display((p:-q,r,s))</tt> writes <tt>:-(p,','(q,','(r,s)))</tt>.<br>
            The extra parentheses are needed because <tt>:-</tt> binds very weakly.
</p>
         </div>
        </td>
       </tr>
      </tbody>
     </table>
    </div>
    <p class="sektie">
     The <tt>is</tt> predicate is a built-in feature of Prolog, and is declared as an infix operator. Its behaviour is illustrated by the following queries:
    </p>
    <p class="query">
     ?-X is 5+7-3<br>
     X = 9
</p>
    <p class="query">
     ?-9 is 5+7-3<br>
     Yes
</p>
    <p class="query">
     ?-9 is X+7-3<br>
     Error in arithmetic expression
</p>
    <p class="query AutoStyle45">
     ?-X is 5*3+7/2<br>
     X = 18.5
</p>

<div class="extract swish" id="3.5.4">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.5.4" query-text="?-X is 5+7-3. ?-9 is 5+7-3. ?-9 is X+7-3. ?-X is 5*3+7/2.">
% Try these queries here.
</pre>
</div>

    <p class="tekst">
     The last example shows, that arithmetic expressions obey the usual precedence rules (which can be overruled using parentheses). Also, note that the <tt>is</tt> predicate can handle real numbers.
    </p>
    <p class="sektie">
     Prolog also provides a built-in predicate <tt>=</tt>, but this predicate behaves quite differently from <tt>is</tt>, since it performs <i>unification</i>&nbsp;rather than arithmetic evaluation (see also section 2.3). The following queries illustrate the operation of <tt>=</tt>:
    </p>
    <p class="query">
     ?-X = 5+7-3<br>
     X = 5+7-3
</p>
    <p class="query">
     ?-9 = 5+7-3<br>
     No
</p>
    <p class="query">
     ?-9 = X+7-3<br>
     No
</p>
    <p class="query">
     ?-X = Y+7-3<br>
     X = _947+7-3<br>
     Y = _947
</p>
    <p class="query AutoStyle45">
     ?-X = f(X)<br>
     X&nbsp;=&nbsp;f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f<br>
     (f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(<br>
     Error: term being written is too deep
</p>

<div class="extract swish" id="3.5.5">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.5.5" query-text="?-X = 5+7-3. ?-9 = 5+7-3. ?-9 = X+7-3. ?-X = Y+7-3. ?-X = f(X).">
% Try these queries here. Is the answer to the last query really as described here?
</pre>
</div>

    <p class="tekst">
     The first query just unifies <tt>X</tt> with the term <tt>5+7-3</tt> (i.e. <tt>+(5,-(7,3))</tt>), which of course succeeds. In the second and third query, we try to unify a constant with a complex term, which fails. The fourth query succeeds, leaving <tt>Y</tt> unbound (<tt>_947</tt> is an internal variable name, generated by Prolog).
    </p>
    <p class="sektie">
     The fifth query illustrates that Prolog indeed omits the occur check (section 2.3) in unification: the query should have failed, but instead it succeeds, resulting in the circular binding { <tt>X</tt>
     <span class="AutoStyle09">
      &rarr;
     </span>
     <tt>f(X)</tt> }. The problem only becomes apparent when Prolog tries to write the resulting term, which is infinite. Just to stress that Prolog quite happily constructs circular bindings, take a look at the following strange program:
    </p>
    <p class="p-el">
     strange:-X=f(X).
    </p>
    <p class="tekst">
     The query <tt>?-strange</tt> succeeds, and since there is no answer substitution, it is not apparent that there is a circular binding involved.
    </p>
<div class="extract exercise" id="3.9">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.9.</i> Write a predicate <tt>zero(A,B,C,X)</tt> which, given the coefficients <i>a</i>, <i>b</i> and <i>c</i>, calculates both values of <i>x</i> for which <i>ax</i>
      <span class="AutoStyle46">
       2
      </span>
      + <i>bx</i> + <i>c</i> =0.
     </p>
    </div>
</div>
    <p class="sektie">
     Finally, we mention that Prolog provides a number of other useful arithmetic predicates, including the inequality tests <tt>&lt;</tt> and <tt>&gt;</tt>, and their reflexive counterparts <tt>=&lt;</tt> and <tt>&gt;=</tt>. For these tests, both arguments should be instantiated to numbers.
    </p>
    <h3 id="accumulators">
     3.6&nbsp;&nbsp;&nbsp;Accumulators
    </h3>
    <p class="sektie1">
     The condition that the righthand-side of <tt>is</tt> should not contain variables sometimes determines the ordering of literals in the body of the clause. For instance, in the program below, which computes the length of a list, the <tt>is</tt> literal should be placed after the recursive <tt>length</tt> call, which instantiates <tt>M</tt>. This means that the resolvent first collects as many <tt>is</tt> literals as there are elements in the list, before doing the actual calculation. Each of these literals contains some &lsquo;local&rsquo; variables that require some space in memory. The total memory requirements are thus proportional to the depth of the recursion.
    </p>

<div class="extract swish" id="3.6.0">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.6.0" query-text="?-naive_length([a,b,c],N).">
naive_length([],0).
naive_length([_H|T],N):-naive_length(T,M),N is M+1.
</pre>
</div>

<div class="extract exercise" id="3.10">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.10.</i> Draw the proof tree for the query <tt>?-naive_length([a,b,c],N)</tt>.
     </p>
    </div>
</div>
    <p class="sektie">
     Programs with tail recursion&nbsp;need less memory because they do all the work on one recursive level before proceeding to the next. There is a common trick to transform even the <tt>length</tt> predicate above into a tail recursive program, using an auxiliary argument called an <i>accumulator</i>.
    </p>

<div class="extract swish" id="3.6.1">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.6.1" query-text="?-length_acc([a,b,c],N). ?-length_acc([a,b,c],0,N). ?-length_acc([a,b,c],3,N).">
length_acc(L,N):-length_acc(L,0,N).

length_acc([],N,N).
length_acc([_H|T],N0,N):-N1 is N0+1,length_acc(T,N1,N).
</pre>
</div>

    <p class="tekst">
     <tt>length_acc(L,N0,N)</tt> is true if <tt>N</tt> is the number of elements in <tt>L</tt> plus <tt>N0</tt>. Initialising <tt>N0</tt> to <tt>0</tt> results in <tt>N</tt> returning the length of <tt>L</tt>. Note that the actual counting is done by the second argument: only when the list is empty is the third argument unified with the second argument. The main point is that, since the accumulator is given an initial value of <tt>0</tt>, it is always instantiated, such that the <tt>is</tt> literal can be placed before the recursive call.
    </p>
<div class="extract exercise" id="3.11">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.11.</i> Draw the proof tree for the query <tt>?-length_acc([a,b,c],N)</tt>.
     </p>
    </div>
</div>
    <p class="sektie">
     Accumulators can be used in very many programs. Suppose we want to reverse the order of elements in a list. We could do this by recursively reversing the tail of the list, and putting the head at the end of the result:
    </p>

<div class="extract swish" id="3.6.2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.6.2" query-text="?-naive_reverse([a,b,c],R).">
naive_reverse([],[]).
naive_reverse([H|T],R):-naive_reverse(T,R1),append(R1,[H],R).

append([],Y,Y).
append([H|T],Y,[H|Z]):-append(T,Y,Z).
</pre>
</div>

    <p class="tekst">
     This predicate is called &lsquo;naive&rsquo; because a lot of unnecessary work is done by the <tt>append</tt> calls in the recursive clause.
    </p>
<div class="extract exercise" id="3.12">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.12.</i> Draw the proof tree for the query <tt>?-naive_reverse([a,b,c],R)</tt>.
     </p>
    </div>
</div>
    <p class="tekst">
     By using an accumulator, we can get rid of the <tt>append</tt> predicate, as follows:
    </p>

<div class="extract swish" id="3.6.3">
    <pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.6.3" query-text="?-reverse([a,b,c],R). ?-reverse([a,b,c],[],R). ?-reverse([b,c],[a],R). ?-reverse([c],[b,a],R).">
reverse(X,Y):- reverse(X,[],Y).

reverse([],Y,Y).
reverse([H|T],Y0,Y):- reverse(T,[H|Y0],Y).
</pre>
</div>

    <p class="tekst">
     <tt>reverse(X,Y0,Y)</tt> is true if <tt>Y</tt> consists of the reversal of <tt>X</tt> followed by <tt>Y0</tt>. Initialising <tt>Y0</tt> to <tt>[]</tt> results in <tt>Y</tt> returning the reversal of <tt>X</tt>.
    </p>
    <p class="sektie">
     The use of an accumulator in this more efficient program for reversing a list is closely related to another programming trick for increasing the efficiency of list handling. The idea is not to represent a list by a single term, but instead by a pair of terms <tt>L1-L2</tt>, such that the list actually represented is the <b>difference</b> between <tt>L1</tt> and <tt>L2</tt>. The term <tt>L1-L2</tt> is appropriately called a <i>difference list</i>; <tt>L1</tt> is called the <i>plus list</i>, and <tt>L2</tt> is called the <i>minus list</i>. For instance, the difference list <tt>[a,b,c,d]-[d]</tt> represents the simple list <tt>[a,b,c]</tt>, as does the difference list <tt>[a,b,c,1234,5678]-[1234,5678]</tt>, and even the difference list <tt>[a,b,c|X]-X</tt>. The last difference list can be seen as summarising every possible difference list representing the same simple list, by introducing a variable for the part which is not contained in the simple list.
    </p>
    <p class="sektie">
     As was remarked above, <tt>reverse(X,Y0,Y)</tt> is true if <tt>Y</tt> consists of the reversal of <tt>X</tt> followed by <tt>Y0</tt>. Another way to say the same thing is that the reversal of <tt>X</tt> is the difference between <tt>Y</tt> and <tt>Y0</tt>. That is, the reversal of <tt>X</tt> is represented by the difference list <tt>Y-Y0</tt>! We can make this explicit by a small syntactic change to <tt>reverse</tt>, resulting in the following program:
    </p>

<div class="extract swish" id="3.6.4">
    <pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.6.4" query-text="?-reverse_dl([a,b,c],R). ?-reverse([a,b,c],R-[]). ?-reverse([b,c],R-[a]). ?-reverse([c],R-[b,a]).">
reverse_dl(X,Y):- reverse(X,Y-[]).

reverse([],Y-Y).
reverse([H|T],Y-Y0):- reverse(T,Y-[H|Y0]).
</pre>
</div>

    <p class="tekst">
     For instance, the third clause in this program says: if the reversal of <tt>T</tt> is represented by the difference list <tt>Y-[H|Y0]</tt>, then adding <tt>H</tt> to the head of <tt>T</tt> is the same as removing <tt>H</tt> from the minus list in the difference list.
    </p>
    <p class="sektie">
     If the minus list is a variable, it can be used as a pointer to the end of the represented list. It is this property which makes difference lists so useful. For instance, if we unify <tt>[a,b,c|X]-X</tt> with <tt>Y-[d,e]</tt>, we get <tt>Y=[a,b,c,d,e]</tt> &mdash; we have managed to append two lists together in a single unification step! In this example, the second term is not a difference list, nor is the result. If we want to append two difference lists
    </p>
    <p class="p-el">
     [a,b,c|XMinus]-XMinus
    </p>
    <p class="tekst">
     and
    </p>
    <p class="p-el">
     [d,e|YMinus]-YMinus
    </p>
    <p class="tekst">
     we must unify <tt>XMinus</tt> with <tt>[d,e|YMinus]</tt> (the plus list of the second difference list), such that the first difference list becomes
    </p>
    <p class="p-el">
     [a,b,c,d,e|YMinus]-[d,e|YMinus]
    </p>
    <p class="tekst">
     Combining the plus list of this difference list with <tt>YMinus</tt>, we get exactly what we want.
    </p>
    <div class="extract figure" id="3.13">
     <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
      <tbody>
       <tr>
        <td align="left" class="AutoStyle04" valign="top">
         <div class="AutoStyle05">
          <p class="figure">
           <img src="img/part_i/image046.svg" v:shapes="_x0000_i1047" width="50%"/>
          </p>
         </div>
         <p class="caption">
          <b>Figure 3.13.</b> Appending   two difference lists: the &lsquo;length&rsquo; of <tt>XMinus</tt> is adjusted by unification with <tt>YPlus</tt>,   the result is given by <tt>XPlus-YMinus</tt>.
         </p>
        </td>
       </tr>
      </tbody>
     </table>
    </div>
    <p class="sektie">
     In general, given two difference lists <tt>XPlus-XMinus</tt> and <tt>YPlus-YMinus</tt>, we unify <tt>XMinus</tt> with <tt>YPlus</tt>, and the result is given by <tt>XPlus-YMinus</tt> (fig. 3.13):
    </p>
    <p class="p-el">
     append_dl(XPlus-XMinus,YPlus-YMinus,XPlus-YMinus):-<br>
     &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;XMinus=YPlus.
</p>
    <p class="tekst">
     or even shorter
    </p>

<div class="extract swish" id="3.6.5">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.6.5" query-text="?-append_dl([a,b,c|X]-X,[d,e|Y]-Y,Z-Z0). ?-append_dl([a,b,c|X]-X,[d,e|Y]-Y,Z-[]).">
append_dl(XPlus-YPlus,YPlus-YMinus,XPlus-YMinus).
</pre>
</div>

    <p class="tekst">
     Appending a simple list to another simple list of <i>n</i> elements requires <i>n</i> resolution steps; appending two difference lists requires no resolution at all, just one unification. Using difference lists is almost always a good idea if you have to do a lot of list processing.
    </p>
<div class="extract exercise" id="3.13">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.13.</i> In the <tt>naive_reverse</tt> predicate, represent the reversed list by a difference list, use <tt>append_dl</tt> instead of <tt>append</tt>, and show that this results in the predicate <tt>reverse_dl</tt> by unfolding the definition of <tt>append_dl</tt>.
     </p>
    </div>
</div>
    <h3 id="second_order_predicates">
     3.7&nbsp;&nbsp;&nbsp;Second-order predicates
    </h3>
    <p class="sektie1">
     Suppose we need a program to determine, given two lists of persons of equal length, whether a person in the first list is the parent of the corresponding person in the second list. The following program will do the job:
    </p>
    <p class="pi-eerst">
     parents([],[]).
    </p>
    <p class="pi-laatst">
     parents([P|Ps],[C|Cs]):-<br>
     parent(P,C),<br>
     parents(Ps,Cs).
</p>
    <p class="tekst">
     We can generalise this program by including the relation which must hold between corresponding elements of the two lists as a parameter:
    </p>
    <p class="pi-eerst">
     rel(R,[],[]).
    </p>
    <p class="pi-laatst">
     rel(R,[X|Xs],[Y|Ys]):-<br>
     R(X,Y),<br>
     rel(R,Xs,Ys).
</p>
    <p class="tekst">
     A term like <tt>R(X,Y)</tt> is allowed at the position of an atom in the body of a clause, as long as it is correctly instantiated at the time it is called.
    </p>
    <p class="sektie">
     Some Prolog interpreters don&rsquo;t allow this, in which case you must explicitly construct the literal by means of the built-in predicate &lsquo; <tt>=..</tt> &rsquo; (sometimes called <i>univ</i>). It is a fully declarative predicate, which can both be used to construct a term from a list of arguments preceded by a functor, or to decompose a term into its constituents:
    </p>
    <p class="query">
     ?-Term =.. [parent,X,peter]<br>
     Term = parent(X,peter)
</p>
    <p class="query AutoStyle45">
     ?-parent(maria,Y) =.. List<br>
     List = [parent,maria,Y]
</p>
    <p class="tekst">
     &lsquo; <tt>=..</tt> &rsquo; is declared as an infix operator in Prolog.
    </p>
<div class="extract exercise" id="3.14">
    <div class="AutoStyle06">
     <p class="exercise AutoStyle07">
      <i>Exercise 3.14.</i> Rewrite the program for <tt>rel</tt>, using <tt>=..</tt>
     </p>
    </div>
</div>
    <div class="extract infobox" id="global_datastructure_in_prolog">
     <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
      <tbody>
       <tr>
        <td align="left" class="AutoStyle04" valign="top">
         <div class="AutoStyle31">
          <p class="inter-title AutoStyle32">
           Global datastructures in Prolog
          </p>
          <p class="intermezzo AutoStyle33">
           Since Prolog variables do not have a scope outside the clause   in which they occur (section 2.2), pure Prolog does not provide any support   for global datastructures. However, Prolog provides access to its internal   database where it stores the program clauses, by means of the built-in   predicates <tt>assert</tt>&nbsp;and <tt>retract</tt>. The query <tt>?-assert(Clause)</tt> results in the addition of <tt>Clause</tt> (which must be instantiated to a   valid Prolog clause) to your program; the query <tt>?‑retract(Clause)</tt> removes the first clause which   unifies with <tt>Clause</tt> from your   program. These predicates are fairly low-level, and should be used with care.
          </p>
         </div>
        </td>
       </tr>
      </tbody>
     </table>
    </div>
    <p class="sektie">
     The predicate <tt>rel</tt> is called a <i>second-order</i> predicate, because it takes a (first-order) predicate as an argument
     <span class="CustomFootnote">
      <a href="#_ftn11" name="_ftnref11" title="">
       <span class="MsoFootnoteReference">
        <span class="AutoStyle13">
         <span class="AutoStyle14">
          [11]
         </span>
        </span>
       </span>
      </a>
     </span>
     . We can now define the <tt>parents</tt> predicate as
    </p>
    <p class="p-el">
     parents(Ps,Cs):-rel(parent,Ps,Cs).
    </p>
    <p class="tekst">
     Suppose now you have the following facts in your program, and you want to collect all the children of a particular parent in a list:
    </p>

<div class="extract swish" id="3.7.1">
<pre class="source swish temp AutoStyle03" data-variant-id="group-2" id="swish.3.7.1">
parent(john,peter).
parent(john,paul).
parent(john,mary).
parent(mick,davy).
parent(mick,dee).
parent(mick,dozy).
</pre>
</div>

    <p class="tekst">
     Of course, it is easy to generate all the children upon backtracking; the problem is to collect them in a global list. To this end, Prolog provides the second-order predicates <tt>findall</tt>, <tt>bagof</tt>, and <tt>setof</tt>. For instance, we could use the following program and query:
    </p>

<div class="extract swish" id="3.7.2">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-2" id="swish.3.7.2" inherit-id="swish.3.7.1">
children(Parent,Children):- findall(C,parent(Parent,C),Children).
</pre>
</div>

<div class="extract swish" id="3.7.1_2">
<pre class="swish query" id="query3.7.1">
?-children(john,Children).
</pre>
</div>

    <p class="query AutoStyle47">
     Children = [peter,paul,mary]
    </p>
    <p class="tekst">
     In general, the query
    </p>
    <p class="p-el">
     ?-findall(X,Goal,ListofX)
    </p>
    <p class="tekst">
     generates all the possible solutions of the query <tt>?‑Goal</tt>, recording the substitutions for <tt>X</tt> for each of these solutions in the list <tt>ListofX</tt> (<tt>Goal</tt> must be instantiated to a term representing a Prolog goal).
    </p>
    <p class="sektie">
     The <tt>bagof</tt>&nbsp;predicate acts similarly. However, its behaviour is different when the goal contains free variables. Consider the query
    </p>
    <p class="query">
     ?-bagof(C,parent(P,C),L)
    </p>
    <p class="tekst">
     in which the variable <tt>P</tt> is unbound. This query has two possible interpretations: &lsquo;find a parent and a list of his children&rsquo;, and &lsquo;find the list of children <i>that have a parent</i> &rsquo;. In the first case, we get a possible value for <tt>P</tt> and a list of <tt>P</tt> &rsquo;s children, which means that there are two solutions:
    </p>

<div class="extract swish" id="3.7.2_2">
<pre class="swish query" id="query3.7.2" source-id="swish.3.7.1">
?-bagof(C,parent(P,C),L).
</pre>
</div>

<p class="query">
     C = _951<br>
     P = john<br>
     L = [peter,paul,mary];
</p>
<p class="query AutoStyle48">
     C = _951<br>
     P = mick<br>
     L = [davy,dee,dozy]
</p>
<p class="tekst">
     In the second case, the goal to prove is &lsquo;there exists a <tt>P</tt> such that <tt>parent(P,C)</tt> is true&rsquo;, which means that the variable <tt>P</tt> is existentially quantified. This is signalled by prefixing the goal with <tt>P^</tt>:
</p>

<div class="extract swish" id="3.7.3">
<pre class="swish query" id="query3.7.3" source-id="swish.3.7.1">
?-bagof(C,P^parent(P,C),L).
</pre>
</div>

    <p class="query AutoStyle45">
     C = _957<br>
     P = _958<br>
     L = [peter,paul,mary,davy,dee,dozy]
</p>
    <p class="tekst">
     The query
    </p>

<div class="extract swish" id="3.7.4">
<pre class="swish query" id="query3.7.4" source-id="swish.3.7.1">
?-findall(C,parent(P,C),L).</pre>
</div>
</div>

<p class="tekst">
 (without existential quantification) can only generate this second solution.
</p>
<p class="sektie">
 Finally, Prolog provides the predicate <tt>setof</tt>, which acts just like <tt>bagof</tt>, except that the resulting list is sorted and does not contain duplicates. Thus, <tt>setof</tt> is slightly less efficient than <tt>bagof</tt>, and the latter is preferred in cases where the list of solutions is known not to contain duplicates.
</p>
<div class="extract exercise" id="3.15">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 3.15.</i> Write a program which sorts and removes duplicates from a list, using <tt>setof</tt>.
 </p>
</div>
</div>
<h3 id="meta_programs">
 3.8&nbsp;&nbsp;&nbsp;Meta-programs
</h3>
<p class="sektie1">
 Prolog represents a clause <tt>Head:-Body</tt> in the same way as a term <tt>:-(Head,Body)</tt>. Thus, it is easy to write programs that manipulate clauses. In the first case, &lsquo; <tt>:-</tt> &rsquo; is treated as a predicate, and in the second case it is treated as a functor. The combination of these two interpretations occurs frequently in Prolog programs, and can be applied to any predicate <tt>p</tt>. Such programs are called <i>meta-programs</i>; the interpretation of <tt>p</tt> as a predicate occurs on the <i>object-level</i>, and the interpretation as a functor occurs on the <i>meta-level</i>. (Note that the difference between meta-predicates and higher-order predicates is that meta-predicates take object-level <i>clauses</i> as arguments, while the latter take lower-order <i>predicates</i> as arguments.)
</p>
<p class="sektie">
 For instance, suppose we have the following biological knowledge, expressed as propositional if-then rules:
</p>

<div class="extract swish" id="3.8.1">
<pre class="source swish temp AutoStyle03" data-variant-id="group-2" id="swish.3.8.1" query-text="?-if tweety then C. ?-if A and lays_eggs then is_bird.">
% if A and B then C means if(then(and(A,B),C))
:-op(900,fx,if).
:-op(800,xfx,then).
:-op(700,yfx,and).
% object-level rules
if has_feathers and lays_eggs then is_bird.
if has_gills and lays_eggs then is_fish.
if tweety then has_feathers.
if tweety then lays_eggs.
</pre>
</div>

<p class="tekst">
 Suppose we want to prove that Tweety is a bird. That is, we want to show that the rule
</p>
<p class="p-el">
 if tweety then is_bird
</p>
<p class="tekst">
 follows logically from the given rules This can be done by a meta-program, which manipulates the rules on the object-level:
</p>

<div class="extract swish" id="3.8.2">
<pre class="source swish inherit AutoStyle03" data-variant-id="group-2" id="swish.3.8.2" inherit-id="swish.3.8.1" query-text="?-derive(if tweety then is_bird). ?-derive(if tweety then C). ?-derive(if A then is_bird).">
% meta-program
derive(if Assumptions then Goal):-
	if Body then Goal,
	derive(if Assumptions then Body).
derive(if Assumptions then Goal1 and Goal2):-
	derive(if Assumptions then Goal1),
	derive(if Assumptions then Goal2).
derive(if Assumptions then Goal):-
	assumed(Goal,Assumptions).
	
assumed(A,A).
assumed(A,A and _As).
assumed(A,_B and As):- assumed(A,As).
</pre>
</div>

<p class="tekst">
 The three clauses for the <tt>derive</tt> predicate represent the three possible cases:
</p>
<p class="opsomming">
 (<i>i</i>)&nbsp;&nbsp;&nbsp;a goal matches the head of a rule, in which case we should proceed<br>
 with the body;
</p>
<p class="opsomming">
 (<i>ii</i>)&nbsp;&nbsp;a goal is a conjunction&nbsp;(for instance, because it was produced in<br>
 the previous step), of which each conjunct is derived separately;
</p>
<p class="opsomming">
 (<i>iii</i>)&nbsp;a goal is among the assumptions.
</p>
<p class="tekst">
 As explained above, <tt>if</tt> is a predicate on the object-level, and a functor on the meta-level.
</p>
<div class="extract exercise" id="3.16">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 3.16.</i> Draw the SLD-tree for the query<br>
  &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<tt>?-derive(if tweety then is_bird)</tt>.
</p>
</div>
</div>
<p class="sektie">
 Since propositional definite clauses are similar to the above if-then rules, one could view this program as a propositional Prolog simulator. In fact, it is possible to push the resemblance closer, by adopting the Prolog-representation of clauses at the object-level. One minor complication is that the clause constructor &lsquo; <tt>:-</tt> &rsquo; is not directly available as an object-level predicate. Instead, Prolog provides the built-in predicate <tt>clause</tt>: a query <tt>?‑clause(H,B)</tt> succeeds if <tt>H:-B</tt> unifies with a clause in the internal Prolog database (if <tt>H</tt> unifies with a fact, <tt>B</tt> is unified with <tt>true</tt>). A further modification with respect to the above program is that Prolog queries do not have the form <tt>if Assumptions then Goal</tt>; instead, the <tt>Assumptions</tt> are added to the object-level program, from which a proof of <tt>Goal</tt> is attempted.
</p>
<p class="sektie">
 Following these observations, the predicate <tt>derive</tt> is changed as follows:
</p>
<p class="pi-eerst">
 prove(Goal):-<br>
 clause(Goal,Body),<br>
 prove(Body).
</p>
<p class="pi">
 prove((Goal1,Goal2)):-<br>
 prove(Goal1),<br>
 prove(Goal2).
</p>
<p class="pi-laatst">
 prove(true).
</p>
<p class="tekst">
 This program nicely reflects the process of constructing a resolution proof:
</p>
<p class="opsomming">
 (<i>i</i>)&nbsp;&nbsp;&nbsp;if the resolvent contains a single atom, find a clause with that atom in the head and proceed with its body;
</p>
<p class="opsomming">
 (<i>ii</i>)&nbsp;&nbsp;if the resolvent contains various atoms, start with the first and proceed with the rest;
</p>
<p class="opsomming">
 (<i>iii</i>)&nbsp;if the resolvent is empty, we&rsquo;re done.
</p>
<p class="tekst">
 Some Prolog interpreters have problems if <tt>clause</tt> is called with the first argument instantiated to <tt>true</tt> or a conjunction, because <tt>true</tt> and &lsquo; <tt>,</tt> &rsquo; (comma) are built-in predicates. To avoid these problems, we should add the conditions <tt>not A=true</tt> and <tt>not A=(X,Y)</tt> to the first clause. A less declarative solution is to reorder the clauses and use cuts:
</p>
<p class="pi-eerst">
 prove(true):-!.
</p>
<p class="pi">
 prove((A,B)):-!,<br>
 prove(A),<br>
 prove(B).
</p>
<p class="pi-laatst">
 prove(A):-<br>
 /* not A=true, not A=(X,Y) */<br>
 clause(A,B),<br>
 prove(B).
</p>
<p class="tekst">
 We will adopt this less declarative version for pragmatic reasons: it is the one usually found in the literature. As this program illustrates, whenever you use cuts it is normally a good idea to add a declarative description of their effect between comment brackets.
</p>
<p class="sektie">
 A meta-program interpreting programs in the same language in which it is written is called a <i>meta-interpreter</i>. In order to &lsquo;lift&rsquo; this propositional meta-interpreter to clauses containing variables, it is necessary to incorporate unification&nbsp;into the third clause. Suppose we are equipped with predicates <tt>unify</tt> and <tt>apply</tt>, such that <tt>unify(T1,T2,MGU,T)</tt> is <b>true</b> if <tt>T</tt> is the result of unifying <tt>T1</tt> and <tt>T2</tt> with most general unifier <tt>MGU</tt>, and <tt>apply(T,Sub,TS)</tt> is <b>true</b> if <tt>TS</tt> is the term obtained from <tt>T</tt> by applying substitution <tt>Sub</tt>. The meta-interpreter would then look like this:
</p>
<p class="pi-eerst">
 prove_var(true):-!.
</p>
<p class="pi">
 prove_var((A,B)):-!,<br>
 prove(A),<br>
 prove(B).
</p>
<p class="pi-laatst">
 prove_var(A):-<br>
 clause(Head,Body),<br>
 unify(A,Head,MGU,Result),<br>
 apply(Body,MGU,NewBody),<br>
 prove_var(NewBody).
</p>
<p class="tekst">
 Prolog&rsquo;s own unification predicate <tt>=</tt>&nbsp;does not return the most general unifier explicitly, but rather unifies the two original terms implicitly. Therefore, if we want to use the built-in unification algorithm in our meta-interpreter, we do not need the <tt>apply</tt> predicate, and we can write the third clause as
</p>
<p class="pi-el">
 prove_var(A):-<br>
 clause(Head,Body),<br>
 A=Head,<br>
 prove_var(Body)
</p>
<div class="extract figure" id="3.14">
 <table align="center" cellpadding="0" cellspacing="0" hspace="0" vspace="0">
  <tbody>
   <tr>
    <td align="left" class="AutoStyle04" valign="top">
     <div class="AutoStyle05">
      <p class="figure">
       <img src="img/part_i/image048.svg" v:shapes="_x0000_i1048" width="60%"/>
      </p>
     </div>
     <p class="caption">
      <b>Figure 3.14.</b> The <tt>prove</tt> meta-interpreter embodies a   declarative implementation of the resolution proof procedure, making use of   built-in unification.
     </p>
    </td>
   </tr>
  </tbody>
 </table>
</div>
<p class="tekst">
 If we now change the explicit unification in the body of this clause to an implicit unification in the head, we actually obtain the propositional meta-interpreter again! That is, while this program is read <b>declaratively</b> as a meta-interpreter for propositional programs, it nevertheless operates <b>procedurally</b> as an interpreter of first-order clauses (fig. 3.14).
</p>
<div class="extract exercise" id="3.17">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 3.17.</i> Draw the SLD-tree for the query <tt>?-prove(is_bird(X))</tt>, given the following clauses:<br>
  &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<tt>is_bird(X):-has_feathers(X),lays_eggs(X).<br>
    &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;is_fish(X):-has_gills(X),lays_eggs(X).<br>
    &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;has_feathers(tweety).<br>
    &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;lays_eggs(tweety).</tt>
</p>
</div>
</div>
<p class="tekst">
 Note that this meta-interpreter is able to handle only &lsquo;pure&rsquo; Prolog programs, without system predicates like cut or <tt>is</tt>, since there are no explicit clauses for such predicates.
</p>
<p class="sektie">
 A variety of meta-interpreters will be encountered in this book. Each of them is a variation of the above &lsquo;canonical&rsquo; meta-interpreter in one of the following senses:
</p>
<p class="opsomming">
 (<i>i</i>)&nbsp;&nbsp;&nbsp;application of a different search strategy;
</p>
<p class="opsomming">
 (<i>ii</i>)&nbsp;&nbsp;application of a different proof procedure;
</p>
<p class="opsomming">
 (<i>iii</i>)&nbsp;enlargement of the set of clauses that can be handled;
</p>
<p class="opsomming">
 (<i>iv</i>)&nbsp;extraction of additional information from the proof process.
</p>
<p class="tekst">
 The first variation will be illustrated in section 5.3, where the meta-interpreter adopts a breadth-first search strategy. In the same section, this meta-interpreter is changed to an interpreter for full clausal logic (<i>iii</i>). Different proof procedures are extensively used in Chapters 8 and 9. Here, we will give two example variations. In the first example, we change the meta-interpreter in order to handle general clauses by means of negation as failure (<i>iii</i>). All we have to do is to add the following clause:
</p>
<p class="pi-el">
 prove(not A):-<br>
 not prove(A)
</p>
<p class="tekst">
 This clause gives a declarative description of negation as failure.
</p>
<p class="sektie">
 The second variation extracts additional information from the SLD proof procedure by means of a proof tree&nbsp;(<i>iv</i>). To this end, we need to make a slight change to the meta-interpreter given above. The reason for this is that the second clause of the original meta-interpreter breaks up the current resolvent if it is a conjunction, whereas in a proof tree we want the complete resolvent to appear.
</p>
<p class="pi-eerst">
 % meta-interpreter with complete resolvent
</p>
<p class="pi">
 prove_r(true):-!.
</p>
<p class="pi">
 prove_r((A,B)):-!,<br>
 clause(A,C),<br>
 conj_append(C,B,D),<br>
 prove_r(D).
</p>
<p class="pi-laatst">
 prove_r(A):-<br>
 clause(A,B),<br>
 prove_r(B).
</p>
<p class="pi-laatst">
 %%% conj_append/3: see Appendix A.2
</p>
<p class="tekst">
 We now extend <tt>prove_r/1</tt> with a second argument, which returns the proof tree as a list of pairs <tt>p(Resolvent,Clause)</tt>:
</p>

<div class="extract swish" id="3.8.2_2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.8.2" query-text="?-prove_p(student_of(S,T)). ?-prove_p(is_bird(X))." source-text-end="
conj_append(true,Ys,Ys).
conj_append(X,Ys,(X,Ys)):-X\=true,X\=(_One,_TheOther).
conj_append((X,Xs),Ys,(X,Zs)):-conj_append(Xs,Ys,Zs).

student_of(S,T):-teaches(T,C),follows(S,C).
teaches(peter,cs).
teaches(peter,ai).
follows(maria,cs).
follows(paul,ai).

is_bird(X):-has_feathers(X),lays_eggs(X).
is_fish(X):-has_gills(X),lays_eggs(X).
has_feathers(tweety).
lays_eggs(tweety).
">
% display a proof tree
prove_p(A):-prove_p(A,P),write_proof(P).

% prove_p(A,P) &lt;- P is proof tree of A
prove_p(true,[]):-!.
prove_p((A,B),[p((A,B),(A:-C))|Proof]):-!,
	clause(A,C),
	conj_append(C,B,D),
	prove_p(D,Proof).
prove_p(A,[p(A,(A:-B))|Proof]):-
	clause(A,B),
	prove_p(B,Proof).

write_proof([]):-
	write('...............[]'),nl.
write_proof([p(A,B)|Proof]):-
	write((:-A)),nl,
	write('.....|'),write('..........'),write(B),nl,
	write('.....|'),write('..................../'),nl,
	write_proof(Proof).
</pre>
</div>

<p class="tekst">
 For instance, given the following clauses:
</p>
<p class="p-el">
 student_of(S,T):-teaches(T,C),follows(S,C).<br>
 teaches(peter,cs).<br>
 teaches(peter,ai).<br>
 follows(maria,cs).<br>
 follows(paul,ai).
</p>
<p class="tekst">
 and the query <tt>?-prove_p(student_of(S,T))</tt>, the program writes the following proof trees:
</p>
<p class="p-eerst">
 :-student_of(peter,maria)
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;student_of(peter,maria):-teaches(peter,cs),follows(maria,cs)
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/
</p>
<p class="programma AutoStyle49">
 :-(teaches(peter,cs),follows(maria,cs))
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;teaches(peter,cs):-true
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/
</p>
<p class="programma AutoStyle49">
 :-follows(maria,cs)
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;follows(maria,cs):-true
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/
</p>
<p class="p-laatst">
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[]
</p>
<p class="programma AutoStyle49">
 :-student_of(peter,paul)
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;student_of(peter,paul):-teaches(peter,ai),follows(paul,ai)
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/
</p>
<p class="programma AutoStyle49">
 :-(teaches(peter,ai),follows(paul,ai))
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;teaches(peter,ai):-true
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/
</p>
<p class="programma AutoStyle49">
 :-follows(paul,ai)
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;follows(paul,ai):-true
</p>
<p class="programma AutoStyle49">
 &nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/
</p>
<p class="p-laatst">
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[]
</p>
<p class="sektie">
 Note that these are propositional proof trees, in the sense that all substitutions needed for the proof have already been applied. If we want to collect the uninstantiated program clauses in the proof tree then we should make a copy of each clause, before it is used in the proof:
</p>
<p class="pi-el">
 prove_p((A,B),[p((A,B),Clause)|Proof]):-!,<br>
 clause(A,C),<br>
 copy_term((A:-C),Clause),&nbsp;% make copy of the clause<br>
 conj_append(C,B,D),<br>
 prove_p(D,Proof)
</p>
<p class="tekst">
 The predicate <tt>copy_term/2</tt>&nbsp;makes a copy of a term, with all variables replaced by new ones. It is a built-in predicate in many Prolog interpreters, but could be defined by means of <tt>assert/2</tt> and <tt>retract/2</tt> (see Appendix A.2 for details).
</p>
<h3 id="a_methodology_of_prolog_programming">
 3.9&nbsp;&nbsp;&nbsp;A methodology of Prolog programming
</h3>
<p class="sektie1">
 At the end of this chapter, we spend a few words on the <i>methodology</i> of writing Prolog&nbsp;programs. Given a problem to solve, how do I obtain the program solving the problem? This is the fundamental problem of software engineering. Here, we can only scratch the surface of this question: we will concentrate on the subtask of writing relatively simple predicates which use no more than two other predicates.
</p>
<p class="sektie">
 Consider the following problem: define a predicate which, given a number <i>n</i>, partitions a list of numbers into two lists: one containing numbers smaller than <i>n</i>, and the other containing the rest. So we need a predicate <tt>partition/4</tt>:
</p>
<p class="oms-eerst AutoStyle45">
 % partition(L,N,Littles,Bigs) &lt;- Littles contains numbers<br>
 %&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in L smaller than N,<br>
 %&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Bigs contains the rest
</p>
<p class="tekst">
 Since the only looping structure of Prolog is recursion, simple predicates like this will typically be recursive. This means that
</p>
<p class="opsomming">
 (<i>i</i>)&nbsp;&nbsp;&nbsp;there is a <i>base case</i>, and one or more recursive clauses;
</p>
<p class="opsomming">
 (<i>ii</i>)&nbsp;&nbsp;there is a <i>recursion argument</i>&nbsp;distinguishing between the base case and the recursive clauses.
</p>
<p class="tekst">
 For list predicates, the recursion argument is typically a list, and the distinction is typically between empty and non-empty lists. For the <tt>partition/4</tt> predicate, the recursion argument is the first list. The base case is easily identified: the empty list is partitioned in two empty lists, no matter the value of <tt>N</tt>. This gives us the following <i>skeleton</i>:
</p>
<p class="pi-eerst">
 partition([],N,[],[]).
</p>
<p class="pi-laatst">
 partition([Head|Tail],N,?Littles,?Bigs):-<br>
 /* do something with Head */<br>
 partition(Tail,N,Littles,Bigs).
</p>
<p class="tekst">
 The question marks denote <i>output arguments</i>, whose relation to the variables in the recursive call still has to be decided. It should be noted that not all predicates are tail recursive, so it is not yet known whether the recursive call will be last indeed. Notice also that the output arguments in the recursive call have been given meaningful names, which is, in general, a good idea.
</p>
<p class="sektie">
 Once we have &lsquo;chopped off&rsquo; the first number in the list, we have to do something with it. Depending on whether it is smaller than <tt>N</tt> or not, it has to  be added to the <tt>Littles</tt> or the <tt>Bigs</tt>. Suppose <tt>Head</tt> is smaller than <tt>N</tt>:
</p>
<p class="pi-el">
 partition([Head|Tail],N,?Littles,?Bigs):-<br>
 Head &lt; N,<br>
 partition(Tail,N,Littles,Bigs)
</p>
<p class="tekst">
 Thus, <tt>Head</tt> must be added to <tt>Littles</tt>. In this case, it does not matter in which position it is added: obviously, the most simple way is to add it to the head of the list:
</p>
<p class="pi-el">
 ?Littles = [Head|Littles]
</p>
<p class="tekst">
 In such cases, where output arguments are simply constructed by unification, the unification is performed implicitly in the head of the clause (the fourth argument remains unchanged):
</p>
<p class="pi-el">
 partition([Head|Tail],N,[Head|Littles],Bigs):-<br>
 Head &lt; N,<br>
 partition(Tail,N,Littles,Bigs)
</p>
<p class="tekst">
 A second recursive clause is needed to cover the case that <tt>Head</tt> is larger than or equal to <tt>N</tt>, in which case it must be added to <tt>Bigs</tt>. The final program looks as follows:
</p>

<div class="extract swish" id="3.9.1">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.9.1" query-text="?-partition([1,9,6,3,5],5,Littles,Bigs). ?-partition([11,7,5],5,Littles,Bigs).">
% partition(L,N,Littles,Bigs) &lt;- Littles contains numbers 
%                                in L smaller than N, 
%                                Bigs contains the rest
partition([],_N,[],[]).
partition([Head|Tail],N,[Head|Littles],Bigs):-
	Head &lt; N,
	partition(Tail,N,Littles,Bigs).
partition([Head|Tail],N,Littles,[Head|Bigs]):-
	Head &gt;= N,
	partition(Tail,N,Littles,Bigs).
</pre>
</div>

<p class="sektie">
 The approach taken here can be formulated as a general strategy for writing Prolog predicates. The steps to be performed according to this strategy are summarised below:
</p>
<p class="opsomming AutoStyle50">
 (<i>i</i>)&nbsp;&nbsp;&nbsp;write down a declarative specification;
</p>
<p class="opsomming">
 (<i>ii</i>)&nbsp;&nbsp;identify the recursion argument, and the output arguments;
</p>
<p class="opsomming">
 (<i>iii</i>)&nbsp;write down a skeleton;
</p>
<p class="opsomming">
 (<i>iv</i>)&nbsp;complete the bodies of the clauses;
</p>
<p class="opsomming AutoStyle45">
 (<i>v</i>)&nbsp;&nbsp;fill in the output arguments.
</p>
<p class="tekst">
 Notice that step (<i>iv</i>) comprises most of the work, while the other steps are meant to make this work as easy as possible.
</p>
<div class="extract exercise" id="3.18">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 3.18.</i> Implement a predicate <tt>permutation/2</tt>, such that <tt>permutation(L,P)</tt> is true if <tt>P</tt> contains the same elements as the list <tt>L</tt> but (possibly) in a different order, following these steps. (One auxiliary predicate is needed.)
 </p>
</div>
</div>
<p class="sektie">
 As a second example, consider the problem of sorting a list&nbsp;of numbers. The declarative specification is as follows:
</p>
<p class="oms-eerst AutoStyle45">
 %mySort(L,S) &lt;- S is a sorted permutation of list L
</p>
<p class="tekst">
 Note that this specification can immediately be translated to Prolog:
</p>
<p class="pi-el">
 mySort(L,S):-<br>
 permutation(L,S),<br>
 sorted(S).
</p>
<p class="tekst">
 This program first guesses a permutation of <tt>L</tt>, and then checks if the permutation happens to be sorted. Declaratively, this program is correct; procedurally, it is extremely inefficent since there are <i>n</i>! different permutations of a list of length <i>n</i>. Thus, we have to think of a more efficient algorithm.
</p>
<p class="sektie">
 The recursion and output arguments are easily identified as the first and second argument, respectively. The base case states that the empty list is already sorted, while the recursive clause states that a non-empty list is sorted by sorting its tail separately:
</p>
<p class="pi-eerst">
 mySort([],[]).
</p>
<p class="pi-laatst">
 mySort([Head|Tail],?Sorted):-<br>
 /* do something with Head */<br>
 mySort(Tail,Sorted).
</p>
<p class="tekst">
 It remains to decide what the relation is between <tt>?Sorted</tt>, <tt>Head</tt> and <tt>Sorted</tt>. Obviously, <tt>Head</tt> cannot be simply added to the front of <tt>Sorted</tt>, but has to be inserted in the proper place. We thus need an auxiliary predicate <tt>insert/3</tt>, to add <tt>Head</tt> at the proper position in <tt>Sorted</tt>. Note that tail  recursion&nbsp;is not applicable in this case, since we have to insert <tt>Head</tt> in an already sorted list. We thus arrive at the following definition:
</p>

<div class="extract swish" id="3.9.2">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.9.2" query-text="?-mySort([3,6,2,8,1],Sorted). ?-mySort([6,5,4,3,2,1],Sorted)." source-text-end="
insert(X,[],[X]).
insert(X,[Head|Tail],[Head|Inserted]):-
	X &gt; Head,
	insert(X,Tail,Inserted).
insert(X,[Head|Tail],[X,Head|Tail]):-
	X =&lt; Head.">
mySort([],[]).
mySort([Head|Tail],WholeSorted):-
	mySort(Tail,Sorted),
	insert(Head,Sorted,WholeSorted).
</pre>
</div>

<p class="sektie">
 In order to implement <tt>insert/3</tt>, we follow the same steps. The second argument is the recursion argument, and the third is the output argument. This gives the following skeleton:
</p>
<p class="pi-eerst">
 insert(X,[],?Inserted).
</p>
<p class="pi-laatst">
 insert(X,[Head|Tail],?Inserted):-<br>
 /* do something with Head */<br>
 insert(X,Tail,Inserted).
</p>
<p class="tekst">
 The base case is simple: <tt>?Inserted = [X]</tt>. In the recursive clause, we have to compare <tt>X</tt> and <tt>Head</tt>. Suppose <tt>X</tt> is greater than <tt>Head</tt>:
</p>
<p class="pi-el">
 insert(X,[Head|Tail],?Inserted):-<br>
 X &gt; Head,<br>
 insert(X,Tail,Inserted)
</p>
<p class="tekst">
 We have to construct the output argument <tt>?Inserted</tt>. Since <tt>X</tt> has already been properly inserted to <tt>Tail</tt>, it remains to add <tt>Head</tt> to the front of <tt>Inserted</tt>:
</p>
<p class="pi-el">
 ?Inserted = [Head|Inserted]
</p>
<p class="tekst">
 A third clause is needed if <tt>X</tt> is not greater than <tt>Head</tt> (note that this clause, being non-recursive, is a second base case):
</p>
<p class="pi-el">
 insert(X,[Head|Tail],?Inserted):-<br>
 X =&lt; Head
</p>
<p class="tekst">
 In this case, <tt>X</tt> should be added before <tt>Head</tt>:
</p>
<p class="p-el">
 ?Inserted = [X,Head|Tail]
</p>
<p class="tekst">
 The complete program is given below:
</p>

<div class="extract swish" id="3.9.3">
<pre class="source swish AutoStyle03" data-variant-id="group-2" id="swish.3.9.3" query-text="?-insert(4,[2,3,5,7],Inserted). ?-insert(1,[2,3,5,7],Inserted). ?-insert(8,[2,3,5,7],Inserted).">
insert(X,[],[X]).
insert(X,[Head|Tail],[Head|Inserted]):-
	X &gt; Head,
	insert(X,Tail,Inserted).
insert(X,[Head|Tail],[X,Head|Tail]):-
	X =&lt; Head.
</pre>
</div>

<div class="extract exercise" id="3.19">
<div class="AutoStyle06">
 <p class="exercise AutoStyle07">
  <i>Exercise 3.19.</i> Implement an alternative to this sorting method by using the <tt>partition/4</tt> predicate.
 </p>
</div>
</div>
<h3 id="further_reading_3">
 Further reading
</h3>
<p class="sektie1">
 There are many introductory and advanced textbooks on Prolog programming. (Bratko, 1990) is a particularly practical introduction. (Sterling &amp; Shapiro, 1986) offers a slightly more advanced presentation. (Nilsson &amp; Maluszynski, 1990) is one of the few books dealing with both the theoretical and practical aspects of programming in Prolog. (Ross, 1989) and (O&rsquo;Keefe, 1990) discuss advanced issues in the practice of Prolog programming.
</p>
<p class="sektie">
 Those eager to learn more about the implementation of Prolog interpreters are referred to (Maier &amp; Warren, 1988). (Bowen &amp; Kowalski, 1982) is an early source on meta-programs in Logic Programming. The slogan Algorithm = Logic + Control&nbsp;was put forward by Kowalski (1979). A discussion of the relation between declarative and procedural programming can be found in (Kowalski, 1993).
</p>
<p class="referenties">
 <span class="AutoStyle41">
  K.A. Bowen &amp; R.A. Kowalski (
 </span>
 1982)
 <span class="AutoStyle41">
  ,
 </span>
 &lsquo;Amalgamating language and metalanguage in Logic Programming&rsquo;. In <i>Logic Programming</i>, K.L. Clark &amp; S. T&auml;rnlund (eds.), Academic Press.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  I. Bratko (
 </span>
 1990)
 <span class="AutoStyle41">
  ,
 </span>
 <i>Prolog Programming for Artificial Intelligence</i>, Addison-Wesley,<br>
 second edition.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  R.A. Kowalski (
 </span>
 1979)
 <span class="AutoStyle41">
  ,
 </span>
 &lsquo;Algorithm = Logic + Control&rsquo;, <i>Communications of the ACM</i> <b>22</b> (7): 424-436.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  R.A. Kowalski (
 </span>
 1993)
 <span class="AutoStyle41">
  ,
 </span>
 &lsquo;Logic Programming&rsquo;. In <i>Encyclopedia of Computer Science</i>,<br>
 A. Ralston &amp; E.D. Reilly (eds), pp. 778-783, Van Nostrand Reinhold,<br>
 third edition.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  D. Maier &amp; D.S. Warren (
 </span>
 1988)
 <span class="AutoStyle41">
  ,
 </span>
 <i>Computing with Logic: Logic Programming with Prolog</i>, Benjamin/Cummings.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  U. Nilsson &amp; J. Maluszynski (
 </span>
 1990)
 <span class="AutoStyle41">
  ,
 </span>
 <i>Logic, Programming and Prolog</i>, John Wiley.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  R.A. O&rsquo;Keefe (
 </span>
 1990)
 <span class="AutoStyle41">
  ,
 </span>
 <i>The Craft of Prolog</i>, MIT Press.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  P. Ross (
 </span>
 1989)
 <span class="AutoStyle41">
  ,
 </span>
 <i>Advanced Prolog: Techniques and Examples</i>, Addison-Wesley.
</p>
<p class="referenties">
 <span class="AutoStyle41">
  L.S. Sterling &amp; E.Y. Shapiro (
 </span>
 1986)
 <span class="AutoStyle41">
  ,
 </span>
 <i>The Art of Prolog</i>, MIT Press.
</p>
<div>
 <br clear="all">
  <hr align="left" size="1" width="33%">
   <div id="ftn1">
    <p class="MsoFootnoteText">
     <a href="#_ftnref1" name="_ftn1" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [1]
        </span>
       </span>
      </span>
     </a>
     If we take Prolog&rsquo;s procedural behaviour into account, there are alternatives to recursive loops such as the so-called <i>failure-driven loop</i> (see Exercise 7.5).
    </p>
   </div>
   <div id="ftn2">
    <p class="MsoFootnoteText">
     <a href="#_ftnref2" name="_ftn2" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [2]
        </span>
       </span>
      </span>
     </a>
     It is often more convenient to read a clause in the opposite direction:<br>
     &lsquo; <b>if</b> somebody is a man <b>and</b> an adult <b>then</b> he is married <b>or</b> a bachelor&rsquo;.
</p>
   </div>
   <div id="ftn3">
    <p class="MsoFootnoteText">
     <a href="#_ftnref3" name="_ftn3" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [3]
        </span>
       </span>
      </span>
     </a>
     <span class="AutoStyle11">
      □
     </span>
     is called the empty clause because it has empty body and head, and therefore it is not satisfiable by any interpretation.
    </p>
   </div>
   <div id="ftn4">
    <p class="MsoFootnoteText">
     <a href="#_ftnref4" name="_ftn4" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [4]
        </span>
       </span>
      </span>
     </a>
     In relational clausal logic, ground terms are necessarily constants. However, this is not the case in full clausal logic, as we will see in section 2.3.
    </p>
   </div>
   <div id="ftn5">
    <p class="MsoFootnoteText">
     <a href="#_ftnref5" name="_ftn5" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [5]
        </span>
       </span>
      </span>
     </a>
     We will have more to say about the generality of clauses in Chapter 9.
    </p>
   </div>
   <div id="ftn6">
    <p class="MsoFootnoteText">
     <a href="#_ftnref6" name="_ftn6" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [6]
        </span>
       </span>
      </span>
     </a>
     For definite clauses this method of bottom-up model construction always yields the unique minimal model of the program.
    </p>
   </div>
   <div id="ftn7">
    <p class="MsoFootnoteText AutoStyle51">
     <a href="#_ftnref7" name="_ftn7" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [7]
        </span>
       </span>
      </span>
     </a>
     The efficiency and completeness of search strategies will be discussed in Chapters 5 and 6.
    </p>
   </div>
   <div id="ftn8">
    <p class="MsoFootnoteText">
     <a href="#_ftnref8" name="_ftn8" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [8]
        </span>
       </span>
      </span>
     </a>
     Written this way to distinguish them from the arrows <tt>=&gt;</tt> and <tt>&lt;=</tt>.
    </p>
   </div>
   <div id="ftn9">
    <p class="MsoFootnoteText">
     <a href="#_ftnref9" name="_ftn9" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [9]
        </span>
       </span>
      </span>
     </a>
     This is not allowed by every Prolog interpreter.
    </p>
   </div>
   <div id="ftn10">
    <p class="MsoFootnoteText">
     <a href="#_ftnref10" name="_ftn10" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [10]
        </span>
       </span>
      </span>
     </a>
     Since efficiency is an implementation issue, it is suggested that <tt>not</tt> is replaced by <tt>!</tt> only in the final stage of program development.
    </p>
   </div>
   <div id="ftn11">
    <p class="MsoFootnoteText">
     <a href="#_ftnref11" name="_ftn11" title="">
      <span class="MsoFootnoteReference">
       <span class="AutoStyle13">
        <span class="AutoStyle14">
         [11]
        </span>
       </span>
      </span>
     </a>
     Recall the discussion about the order of a logic in section 2.5.
    </p>
   </div>
  </hr>
</div>
<h2>
 Additional material
</h2>
<h3>
 Section 3.1
</h3>

<div class="extract swish" id="plist">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="plist" query-text="?-plist(L).">
plist([]).
plist([H|T]):-p(H),plist(T).

p(1).
p(2).
</pre>
</div>

<h3>
 Section 3.6
</h3>

<div class="extract swish" id="fib">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="fib" query-text="?-fib(10,F). ?-fib(20,F). ?-fib(30,F). ?-fibn(30,F). ?-fibn(50,F). ?-fibn(100,F).">
% fib(N,F) &lt;- F is the N-th Fibonacci number
% inefficient doubly-recursive version
fib(1,1).
fib(2,1).
fib(N,F):-
	N&gt;2,N1 is N-1,N2 is N-2,
	fib(N1,F1),fib(N2,F2),
	F is F1+F2.

% We can get a more efficient version 
% by solving a more general problem!

% fibn(N,Na,Nb,F) &lt;- F is the N-th Fibonacci number
%                   in the sequence starting with Na, Nb
fibn(1,Na,_,Na).
fibn(2,_,Nb,Nb).
fibn(N,Na,Nb,F):-
	N&gt;2, N1 is N-1,
	Nc is Na+Nb,
	fibn(N1,Nb,Nc,F).

fibn(N,F):-
	fibn(N,1,1,F).
</pre>
</div>

<h3>
 Section 3.7
</h3>

<div class="extract swish" id="biglist">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="biglist" query-text="?-biglist(1,15,L).">
biglist(Low,High,L):-
    bagof(X,between(Low,High,X),L).
    
between(Low,_High,Low).
between(Low,High,Number):-
	Low &lt; High,
	NewLow is Low+1,
	between(NewLow,High,Number).
</pre>
</div>

<h3>
 Section 3.9
</h3>

<div class="extract swish" id="powerset">
<pre class="source swish AutoStyle03" data-variant-id="group-1" id="powerset" query-text="?-powerset([a,b,c,d,e],PS). ?-powerset1([a,b,c,d,e],PS). ?-powerset2([a,b,c,d,e],PS). ?-biglist(1,20,S),powerset(S,PS). ?-biglist(1,20,S),powerset1(S,PS). ?-biglist(1,20,S),powerset2(S,PS). " source-text-end="
%%% For testing
biglist(Low,High,L):-bagof(X,between(Low,High,X),L).">
%%% Good generator, but not tail-recursive 
powerset([],[[]]).
powerset([H|T],PowerSet):-
	powerset(T,PowerSetOfT),             % generator (GOOD) 
	extend_pset(H,PowerSetOfT,PowerSet). % not tail-recursive
	
extend_pset(_,[],[]).
extend_pset(H,[List|MoreLists],[List,[H|List]|More]):-
	extend_pset(H,MoreLists,More).
	
%%% Bad generator, tail-recursive
powerset1([],[[]]).
powerset1([H|T],PowerSet):-
	extend_pset(H,PowerSetOfT,PowerSet), % generator (BAD)
	powerset1(T,PowerSetOfT).            % tail-recursive

%%% Good generator, tail-recursive
powerset2([],PowerSet,PowerSet).
powerset2([H|T],Acc,PowerSet):-
	extend_pset(H,Acc,Acc1),             % generator (GOOD) 
	powerset2(T,Acc1,PowerSet).          % tail-recursive

powerset2(Set,PowerSet):-powerset2(Set,[[]],PowerSet).
</pre>
</div>

<script>
 $(function() { $(".swish").LPN({swish:"{{ site.swish }}"}); });
</script>