add trace output

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

add trace output
833d9579 · Michael Leuschel · 86446f5c · 833d9579
Commit 833d9579 authored 2 years ago by Michael Leuschel
--- a/logic_programming/5_SLD.ipynb
+++ b/logic_programming/5_SLD.ipynb
@@ -547,6 +547,28 @@
    "?- program(2,_,Clauses), trace_prove(p,Clauses)."
   ]
  },
+  {
+   "cell_type": "markdown",
+   "id": "b59dd776",
+   "metadata": {},
+   "source": [
+    "When you step through the corresponding Prolog program using the Prolog debugger you will get an output like this one (after declaring t/0 as dynamic to avoid error messages):\n",
+    "```\n",
+    "| ?-      p.\n",
+    "        1      1 Call: p ? \n",
+    "        2      2 Call: q ? \n",
+    "        3      3 Call: t ? \n",
+    "        3      3 Fail: t ? \n",
+    "        4      3 Call: s ? \n",
+    "        4      3 Exit: s ? \n",
+    "        2      2 Exit: q ? \n",
+    "        5      2 Call: r ? \n",
+    "        5      2 Exit: r ? \n",
+    "        1      1 Exit: p ? \n",
+    "yes\n",
+    "```"
+   ]
+  },
  {
   "cell_type": "markdown",
   "id": "b4b28da4",

 %% Cell type:markdown id:9eb5530a tags:

 # Linear Resolution and SLD Resolution

 ```Horn clauses``` are clauses (i.e., disjunctions of literals) with at most one positive literal.
 A ```query``` or denial is a Horn clause without positive literal.
 A ```fact``` is a Horn clause consisting of one positive literal and no negative literals.

 Note that the CNF of our knights and knaves puzzle, contains one query, no facts and
 two non-Horn clauses ```B ∨ A``` and ```C ∨ A```:
 ```
 {¬A ∨ ¬B ∨ ¬C,  B ∨ A,  C ∨ A,  ¬B ∨ A,  ¬A ∨ B}
 ```

 Note that Prolog programs are automatically Horn clauses in CNF.
 For example, the Prolog clause
 ```
 wet :- rains, outside.
 ```

 corresponds to the Horn clause:

 ```
 wet ∨ ¬rains ∨ ¬outside
 ```

 The head of a Prolog clause is a positive literal. The calls in the body correspond to negative literals.

 Querys are not Prolog program clauses but stem from the Prolog console.

 %% Cell type:markdown id:1eb3920b tags:

 Let us now encode a simple Prolog program using the representation from the previous notebook:

 %% Cell type:code id:964ebd52 tags:

 ``` prolog
 :- discontiguous program/3.
 :- dynamic program/3.
 program(1,'weather',
   [ [pos(wet),neg(rains),neg(outside)],
     [pos(rains)],
     [pos(outside)] ]).
 negate(pos(A),neg(A)).
 negate(neg(A),pos(A)).
 ```

 %% Cell type:markdown id:a4dc903e tags:

 For simplicity we will assume that the positive literal is always the first literal in a clause.

 Let us now perform resolution with a negative literal:

 %% Cell type:code id:26e0221b tags:

 ``` prolog
 resolve_literal(neg(Prop),Clauses,Resolvent) :-
     member([pos(Prop)|Body],Clauses), % find a clause with a corresponding positive literal
     Resolvent=Body.
 ```

 %% Cell type:markdown id:fc6823ad tags:

 This can be used like this:

 %% Cell type:code id:152289b6 tags:

 ``` prolog
 ?- program(1,_,P),resolve_literal(neg(wet),P,Resolvent).
 ```

 %% Output


 %% Cell type:markdown id:68fd6059 tags:

 Here we find a contradiction:

 %% Cell type:code id:2c3dd1bf tags:

 ``` prolog
 ?- program(1,_,P),resolve_literal(neg(rains),P,Resolvent).
 ```

 %% Output


 %% Cell type:markdown id:07785e91 tags:

 We can extend this code to work with a complete denial, rather than single negative literal:

 %% Cell type:code id:33fc6271 tags:

 ``` prolog
 resolve_query(Query,Clauses,Resolvent) :-
     selection_rule(Query,SelectedLiteral,RestQuery),
     resolve_literal(SelectedLiteral,Clauses,Body),
     append(Body,RestQuery,Resolvent).

 selection_rule([LeftmostLiteral|Rest],LeftmostLiteral,Rest).
 ```

 %% Cell type:markdown id:1d426bb1 tags:

 The above predicate uses the predicate ```select/3``` from ```library(lists)```, which can be used to select an element from a list and returns a modified list with the element removed:

 %% Cell type:code id:f2a8b4a4 tags:

 ``` prolog
 ?- program(1,_,P),resolve_query([neg(wet)],P,Resolvent).
 ```

 %% Output


 %% Cell type:markdown id:cba18c66 tags:

 As you can see, the resolvent is again a query consisting only of negative literals.
 We can apply resolution again:

 %% Cell type:code id:06aa608c tags:

 ``` prolog
 ?- program(1,_,P),resolve_query([neg(rains),neg(outside)],P,Resolvent).
 ```

 %% Output


 %% Cell type:markdown id:4c71d8af tags:

 As you can see, the resolvent is again a query consisting only of negative literals.
 We can apply resolution again:

 %% Cell type:code id:a76d8b5d tags:

 ``` prolog
 ?- program(1,_,P),resolve_query([neg(outside)],P,Resolvent).
 ```

 %% Output


 %% Cell type:markdown id:4d9ecefc tags:

 We have now reached the empty clause, i.e., a contradiction.
 This means that the original proposition wet is a logical consequence of our logic program.

 %% Cell type:markdown id:e67981b4 tags:

 We can now try to encode the search for a contradiction systematically as follows:

 %% Cell type:code id:d7a0cc62 tags:

 ``` prolog
 prove(Proposition,Clauses) :-
    find_contradiction([neg(Proposition)],Clauses).

 find_contradiction([],_). % empty clause found
 find_contradiction(Query,Clauses) :-
    resolve_query(Query,Clauses,NewQuery),
    find_contradiction(NewQuery,Clauses).
 ```

 %% Cell type:markdown id:2b2ea192 tags:

 Let us now check whether wet is a logical consequence of program 1:

 %% Cell type:code id:78163b60 tags:

 ``` prolog
 ?- program(1,_,Clauses), prove(wet,Clauses).
 ```

 %% Output


 %% Cell type:markdown id:a70dbafb tags:

 There are a few important observations:
 - negative literals always come from the query
 - positive literals always come from the program clauses
 - the resolve_literal predicate can have multiple solutions
 - the clauses in the logic program (```Clauses``` above) are never changed.
 The last point means that there is no exponential growth of the number of clauses during execution and it means we can precompile the logic program to find clauses for the given positive literals.

 This procedure is called linear resolution, as the pool of clauses remains of constant size
 and we "forget" earlier denials, except for backtracking when no contradiction is found.

 The above code also contains a so-called selection rule/function ```selection_rule```.
 This one selects the next literal chosen for resolution in the query.
 - it is a function: no backtracking is needed
 - there is an important property, called "independence of the selection function" which stipulates that it is correct to not backtrack
 - Prolog's execution engine uses the leftmost literal by default; we have done the same above

 The procedure we have implemente is called SLD-resolution:
 - Selection rule driven
 - Linear resolution for
 - Definite clauses

 (Definite clauses are clauses without using Prolog's negation operator. We will return to this later.)

 %% Cell type:markdown id:4759110b tags:

 Let us augment the above procedure with a few print statements:

 %% Cell type:code id:9d3fbd1a tags:

 ``` prolog
 trace_prove(Prop,Clauses) :- trace_find_contradiction([neg(Prop)],Clauses,1).
 trace_find_contradiction([],_,Nr) :- format(' ~w: [] (contradiction)~n',[Nr]). % empty clause found
 trace_find_contradiction(Query,Clauses,Nr) :-
    format(' ~w: ~w~n',[Nr,Query]), N1 is Nr+1,
    resolve_query(Query,Clauses,NewQuery),
    trace_find_contradiction(NewQuery,Clauses,N1).
 ```

 %% Cell type:code id:a8ba5814 tags:

 ``` prolog
 ?- program(1,_,Clauses), trace_prove(wet,Clauses).
 ```

 %% Output



 %% Cell type:markdown id:6cdeade5 tags:

 The above sequence of denials is also called an ```SLD-derivation```.
 An SLD-derivation which ends in a contradiction is called an ```SLD-refutation```.

 %% Cell type:markdown id:d32921c9 tags:

 Let us examine a more complicated example corresponding to the Prolog program

 ```
 p :- q,r.
 q :- t.
 q :- s.
 r.
 s.
 ```

 %% Cell type:code id:26924712 tags:

 ``` prolog
 program(2,'Backtracking',[
      [pos(p),neg(q),neg(r)],
      [pos(q),neg(t)],
      [pos(q),neg(s)],
      [pos(r)],
      [pos(s)]
       ]) :- true.
 ```

 %% Cell type:markdown id:17dd1525 tags:

 If we now try to prove that ```p``` is a logical consequence of program 2 we will see that backtracking is required:

 %% Cell type:code id:7d90c4ad tags:

 ``` prolog
 ?- program(2,_,Clauses), trace_prove(p,Clauses).
 ```

 %% Output



+%% Cell type:markdown id:b59dd776 tags:
+
+When you step through the corresponding Prolog program using the Prolog debugger you will get an output like this one (after declaring t/0 as dynamic to avoid error messages):
+```
+| ?-      p.
+        1      1 Call: p ?
+        2      2 Call: q ?
+        3      3 Call: t ?
+        3      3 Fail: t ?
+        4      3 Call: s ?
+        4      3 Exit: s ?
+        2      2 Exit: q ?
+        5      2 Call: r ?
+        5      2 Exit: r ?
+        1      1 Exit: p ?
+yes
+```
+
 %% Cell type:markdown id:b4b28da4 tags:

 By putting the above queries into a tree we obtain a so-called ```SLD-tree``` for the program and top-level query under consideration.

 %% Cell type:markdown id:29e3d513 tags:

 Below is some code to display this SLD-tree graphically in Jupyter:

 %% Cell type:code id:cdfb419b tags:

 ``` prolog
 sld_node(Query,[shape/S,color/C],InitialQuery,ProgNr) :- sub_goal(InitialQuery,ProgNr,Query),
  (Query=[] -> S=rect,C=green ; sld_edge(Query,_,ProgNr,_) ->  S=egg, C=blue ; S=ellipse, C=red).

 sub_goal(Q,_,Q).
 sub_goal(Q,ProgNr,SubG) :- sld_edge(Q,_,ProgNr,NewQuery),
  sub_goal(NewQuery,ProgNr,SubG).

 sld_edge(Q,Lit,ProgNr,NewQuery) :- selection_rule(Q,neg(Lit),_),
   program(ProgNr,_,Clauses), resolve_query(Q,Clauses,NewQuery).
 ```

 %% Cell type:code id:8f652455 tags:

 ``` prolog
 ?- sld_node(Q,L,[neg(p)],2).
 ```

 %% Output


 %% Cell type:code id:bc5e2d49 tags:

 ``` prolog
 jupyter:show_graph(sld_node(_,_,[neg(p)],2),sld_edge(_,_,2,_))
 ```

 %% Output




 %% Cell type:code id:64f06b8f tags:

 ``` prolog
 ?-sld_edge([neg(p)],L,NQ,2).
 ```

 %% Output


 %% Cell type:code id:a847a9b7 tags:

 ``` prolog
 program(3,'circuit', [
    % Die Belegung von der Aufgabe:
 [pos(a)], [pos(not_b)], [pos(c)],[pos(not_d)], [pos(e)],
 % Schaltungen der ersten Ebene
 [pos(and11) , neg(a),neg(b)],
 [pos(or11) , neg(b)],
 [pos(or11) , neg(c)],
 [pos(and12) , neg(c),neg(d)],
 [pos(not1) , neg(not_e)],
 % Schaltungen der zweiten Ebene
 [pos(or21) , neg(and11)],
 [pos(or21) , neg(not1)],
 [pos(and2) , neg(or11),neg(not1)],
 [pos(or22) , neg(and12)],
 [pos(or22) , neg(not1)],
 [pos(not2) , neg(e)],  % \+ not1)],
 % Schaltungen der dritten Ebene
 [pos(and3) , neg(or21),neg(and2)],
 [pos(or3) , neg(or22)],
 [pos(or3) , neg(not2)],
 % Schaltungen der vierten Ebene
 [pos(or4) , neg(and3)],
 [pos(or4) , neg(or3)],
 [pos(and4) , neg(or3),neg(not2)],
 % Letzte Ebene
 [pos(and5) , neg(and4),neg(or4)],
 [pos(output) , neg(and5)]
 ]) :- true.
 ```

 %% Cell type:code id:e46506a9 tags:

 ``` prolog
 ?- program(3,_,Clauses), trace_prove(output,Clauses).
 ```

 %% Output



 %% Cell type:code id:9d979ec6 tags:

 ``` prolog
 jupyter:show_graph(sld_node(_,_,[neg(output)],3),sld_edge(_,_,3,_))
 ```

 %% Output




 %% Cell type:code id:fe797463 tags:

 ``` prolog
 ```