Skip to content
Snippets Groups Projects
Commit 86446f5c authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add SLD tree for circuit example 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent e5892e1e
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
logic_programming/5_SLD.ipynb
+ 353
− 13
View file @ 86446f5c
%% Cell type:markdown id:9eb5530a tags: %% Cell type:markdown id:9eb5530a tags:
# Linear Resolution and SLD Resolution # Linear Resolution and SLD Resolution
```Horn clauses``` are clauses (i.e., disjunctions of literals) with at most one positive literal. ```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 ```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. 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 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```: two non-Horn clauses ```B ∨ A``` and ```C ∨ A```:
``` ```
{¬A ∨ ¬B ∨ ¬C, B ∨ A, C ∨ A, ¬B ∨ A, ¬A ∨ B} {¬A ∨ ¬B ∨ ¬C, B ∨ A, C ∨ A, ¬B ∨ A, ¬A ∨ B}
``` ```
Note that Prolog programs are automatically Horn clauses in CNF. Note that Prolog programs are automatically Horn clauses in CNF.
For example, the Prolog clause For example, the Prolog clause
``` ```
wet :- rains, outside. wet :- rains, outside.
``` ```
corresponds to the Horn clause: corresponds to the Horn clause:
``` ```
wet ∨ ¬rains ∨ ¬outside wet ∨ ¬rains ∨ ¬outside
``` ```
The head of a Prolog clause is a positive literal. The calls in the body correspond to negative literals. 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. Querys are not Prolog program clauses but stem from the Prolog console.
%% Cell type:markdown id:1eb3920b tags: %% Cell type:markdown id:1eb3920b tags:
Let us now encode a simple Prolog program using the representation from the previous notebook: Let us now encode a simple Prolog program using the representation from the previous notebook:
%% Cell type:code id:964ebd52 tags: %% Cell type:code id:964ebd52 tags:
``` prolog ``` prolog
:- discontiguous program/3. :- discontiguous program/3.
:- dynamic program/3. :- dynamic program/3.
program(1,'weather', program(1,'weather',
[ [pos(wet),neg(rains),neg(outside)], [ [pos(wet),neg(rains),neg(outside)],
[pos(rains)], [pos(rains)],
[pos(outside)] ]). [pos(outside)] ]).
negate(pos(A),neg(A)). negate(pos(A),neg(A)).
negate(neg(A),pos(A)). negate(neg(A),pos(A)).
``` ```
%% Cell type:markdown id:a4dc903e tags: %% Cell type:markdown id:a4dc903e tags:
For simplicity we will assume that the positive literal is always the first literal in a clause. 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: Let us now perform resolution with a negative literal:
%% Cell type:code id:26e0221b tags: %% Cell type:code id:26e0221b tags:
``` prolog ``` prolog
resolve_literal(neg(Prop),Clauses,Resolvent) :- resolve_literal(neg(Prop),Clauses,Resolvent) :-
member([pos(Prop)|Body],Clauses), % find a clause with a corresponding positive literal member([pos(Prop)|Body],Clauses), % find a clause with a corresponding positive literal
Resolvent=Body. Resolvent=Body.
``` ```
%% Cell type:markdown id:fc6823ad tags: %% Cell type:markdown id:fc6823ad tags:
This can be used like this: This can be used like this:
%% Cell type:code id:152289b6 tags: %% Cell type:code id:152289b6 tags:
``` prolog ``` prolog
?- program(1,_,P),resolve_literal(neg(wet),P,Resolvent). ?- program(1,_,P),resolve_literal(neg(wet),P,Resolvent).
``` ```
%% Output %% Output
%% Cell type:markdown id:68fd6059 tags: %% Cell type:markdown id:68fd6059 tags:
Here we find a contradiction: Here we find a contradiction:
%% Cell type:code id:2c3dd1bf tags: %% Cell type:code id:2c3dd1bf tags:
``` prolog ``` prolog
?- program(1,_,P),resolve_literal(neg(rains),P,Resolvent). ?- program(1,_,P),resolve_literal(neg(rains),P,Resolvent).
``` ```
%% Output %% Output
%% Cell type:markdown id:07785e91 tags: %% Cell type:markdown id:07785e91 tags:
We can extend this code to work with a complete denial, rather than single negative literal: We can extend this code to work with a complete denial, rather than single negative literal:
%% Cell type:code id:33fc6271 tags: %% Cell type:code id:33fc6271 tags:
``` prolog ``` prolog
resolve_query(Query,Clauses,Resolvent) :- resolve_query(Query,Clauses,Resolvent) :-
selection_rule(Query,SelectedLiteral,RestQuery), selection_rule(Query,SelectedLiteral,RestQuery),
resolve_literal(SelectedLiteral,Clauses,Body), resolve_literal(SelectedLiteral,Clauses,Body),
append(Body,RestQuery,Resolvent). append(Body,RestQuery,Resolvent).
selection_rule([LeftmostLiteral|Rest],LeftmostLiteral,Rest). selection_rule([LeftmostLiteral|Rest],LeftmostLiteral,Rest).
``` ```
%% Cell type:markdown id:1d426bb1 tags: %% 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: 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: %% Cell type:code id:f2a8b4a4 tags:
``` prolog ``` prolog
?- program(1,_,P),resolve_query([neg(wet)],P,Resolvent). ?- program(1,_,P),resolve_query([neg(wet)],P,Resolvent).
``` ```
%% Output %% Output
%% Cell type:markdown id:cba18c66 tags: %% Cell type:markdown id:cba18c66 tags:
As you can see, the resolvent is again a query consisting only of negative literals. As you can see, the resolvent is again a query consisting only of negative literals.
We can apply resolution again: We can apply resolution again:
%% Cell type:code id:06aa608c tags: %% Cell type:code id:06aa608c tags:
``` prolog ``` prolog
?- program(1,_,P),resolve_query([neg(rains),neg(outside)],P,Resolvent). ?- program(1,_,P),resolve_query([neg(rains),neg(outside)],P,Resolvent).
``` ```
%% Output %% Output
%% Cell type:markdown id:4c71d8af tags: %% Cell type:markdown id:4c71d8af tags:
As you can see, the resolvent is again a query consisting only of negative literals. As you can see, the resolvent is again a query consisting only of negative literals.
We can apply resolution again: We can apply resolution again:
%% Cell type:code id:a76d8b5d tags: %% Cell type:code id:a76d8b5d tags:
``` prolog ``` prolog
?- program(1,_,P),resolve_query([neg(outside)],P,Resolvent). ?- program(1,_,P),resolve_query([neg(outside)],P,Resolvent).
``` ```
%% Output %% Output
%% Cell type:markdown id:4d9ecefc tags: %% Cell type:markdown id:4d9ecefc tags:
We have now reached the empty clause, i.e., a contradiction. 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. This means that the original proposition wet is a logical consequence of our logic program.
%% Cell type:markdown id:e67981b4 tags: %% Cell type:markdown id:e67981b4 tags:
We can now try to encode the search for a contradiction systematically as follows: We can now try to encode the search for a contradiction systematically as follows:
%% Cell type:code id:d7a0cc62 tags: %% Cell type:code id:d7a0cc62 tags:
``` prolog ``` prolog
prove(Proposition,Clauses) :- prove(Proposition,Clauses) :-
find_contradiction([neg(Proposition)],Clauses). find_contradiction([neg(Proposition)],Clauses).
find_contradiction([],_). % empty clause found find_contradiction([],_). % empty clause found
find_contradiction(Query,Clauses) :- find_contradiction(Query,Clauses) :-
resolve_query(Query,Clauses,NewQuery), resolve_query(Query,Clauses,NewQuery),
find_contradiction(NewQuery,Clauses). find_contradiction(NewQuery,Clauses).
``` ```
%% Cell type:markdown id:2b2ea192 tags: %% Cell type:markdown id:2b2ea192 tags:
Let us now check whether wet is a logical consequence of program 1: Let us now check whether wet is a logical consequence of program 1:
%% Cell type:code id:78163b60 tags: %% Cell type:code id:78163b60 tags:
``` prolog ``` prolog
?- program(1,_,Clauses), prove(wet,Clauses). ?- program(1,_,Clauses), prove(wet,Clauses).
``` ```
%% Output %% Output
%% Cell type:markdown id:a70dbafb tags: %% Cell type:markdown id:a70dbafb tags:
There are a few important observations: There are a few important observations:
- negative literals always come from the query - negative literals always come from the query
- positive literals always come from the program clauses - positive literals always come from the program clauses
- the resolve_literal predicate can have multiple solutions - the resolve_literal predicate can have multiple solutions
- the clauses in the logic program (```Clauses``` above) are never changed. - 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. 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 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. 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```. 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. This one selects the next literal chosen for resolution in the query.
- it is a function: no backtracking is needed - 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 - 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 - 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: The procedure we have implemente is called SLD-resolution:
- Selection rule driven - Selection rule driven
- Linear resolution for - Linear resolution for
- Definite clauses - Definite clauses
(Definite clauses are clauses without using Prolog's negation operator. We will return to this later.) (Definite clauses are clauses without using Prolog's negation operator. We will return to this later.)
%% Cell type:markdown id:4759110b tags: %% Cell type:markdown id:4759110b tags:
Let us augment the above procedure with a few print statements: Let us augment the above procedure with a few print statements:
%% Cell type:code id:9d3fbd1a tags: %% Cell type:code id:9d3fbd1a tags:
``` prolog ``` prolog
trace_prove(Prop,Clauses) :- trace_find_contradiction([neg(Prop)],Clauses,1). 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([],_,Nr) :- format(' ~w: [] (contradiction)~n',[Nr]). % empty clause found
trace_find_contradiction(Query,Clauses,Nr) :- trace_find_contradiction(Query,Clauses,Nr) :-
format(' ~w: ~w~n',[Nr,Query]), N1 is Nr+1, format(' ~w: ~w~n',[Nr,Query]), N1 is Nr+1,
resolve_query(Query,Clauses,NewQuery), resolve_query(Query,Clauses,NewQuery),
trace_find_contradiction(NewQuery,Clauses,N1). trace_find_contradiction(NewQuery,Clauses,N1).
``` ```
%% Cell type:code id:a8ba5814 tags: %% Cell type:code id:a8ba5814 tags:
``` prolog ``` prolog
?- program(1,_,Clauses), trace_prove(wet,Clauses). ?- program(1,_,Clauses), trace_prove(wet,Clauses).
``` ```
%% Output %% Output
%% Cell type:markdown id:6cdeade5 tags: %% Cell type:markdown id:6cdeade5 tags:
The above sequence of denials is also called an ```SLD-derivation```. The above sequence of denials is also called an ```SLD-derivation```.
An SLD-derivation which ends in a contradiction is called an ```SLD-refutation```. An SLD-derivation which ends in a contradiction is called an ```SLD-refutation```.
%% Cell type:markdown id:d32921c9 tags: %% Cell type:markdown id:d32921c9 tags:
Let us examine a more complicated example corresponding to the Prolog program Let us examine a more complicated example corresponding to the Prolog program
``` ```
p :- q,r. p :- q,r.
q :- t. q :- t.
q :- s. q :- s.
r. r.
s. s.
``` ```
%% Cell type:code id:26924712 tags: %% Cell type:code id:26924712 tags:
``` prolog ``` prolog
program(2,'Backtracking',[ program(2,'Backtracking',[
[pos(p),neg(q),neg(r)], [pos(p),neg(q),neg(r)],
[pos(q),neg(t)], [pos(q),neg(t)],
[pos(q),neg(s)], [pos(q),neg(s)],
[pos(r)], [pos(r)],
[pos(s)] [pos(s)]
]) :- true. ]) :- true.
``` ```
%% Cell type:markdown id:17dd1525 tags: %% 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: 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: %% Cell type:code id:7d90c4ad tags:
``` prolog ``` prolog
?- program(2,_,Clauses), trace_prove(p,Clauses). ?- program(2,_,Clauses), trace_prove(p,Clauses).
``` ```
%% Output %% Output
%% Cell type:markdown id:b4b28da4 tags: %% 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. 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
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment