Horn clause logic

Non-deterministic algorithm for backward chaining over Horn clauses.

bc(G : negated goal (purely negative clause); 
   A : set of rules and facts)

loop pick a literal L in G;                                  /* Line 1 */
     choose R in A such that the head of R unifies with L;   /* Line 2 */
     G := resolve G with R                                   /* Line 3 */
  until G is the null clause when succeed
endloop.

Prolog

Pure Prolog is this algorithm, implemented so that:

We use Prolog notation:
P :- Q1, Q2, Q3 means (Q1^Q2^Q3) => P.
?- Z means that Z is a goal; i.e. (not Z) is a negated goal.

Sample rule base

% X is the sister-in-law of Y

sister_in_law(X,Y) :- sibling(X,Z), married(Z,Y), female(X).  % Rule 1
sister_in_law(X,Y) :- wife(X,Z), sibling(Z,Y).                % Rule 2
sister_in_law(X,Y) :- wife(X,W), sibling(W,Z), married(Z,X).  % Rule 3

/* Note this definition admits the case X=Y.  That leads to
   some strange sisters_in_law. */
sibling(X,Z) :- parent(Y,X), parent(Y,Z).                     % Rule 4

married(X,Y) :- wife(X,Y).                                    % Rule 5
married(X,Y) :- wife(Y,X).                                    % Rule 6


parent(mary,sam).                                             % Fact 7
parent(leslie,rachel).                                        % Fact 8
parent(mark,rachel).                                          % Fact 9
parent(mark,sam).                                             % Fact 10
parent(leslie,nick)                                           % Fact 11

wife(jennifer,sam)                                            % Fact 12
wife(rachel,leo).                                             % Fact 13

female(rachel).                                               % Fact 14
female(jennifer).                                             % Fact 15

DFS

G1: ?- sister_in_law(rachel,jennifer).    Resolve with Rule 1
G2: ?- sibling(rachel,Z1), married(Z1,jennifer), female(rachel). 
                                                     Resolve with Rule 4.
G3: ?- parent(Y2,rachel), parent(Y2,Z1), married(Z1,jennifer), female(rachel). 
                                                     Resolve with Fact 8.
G4: ?- parent(leslie,Z1),married(Z1,jennifer), female(rachel).
                                                     Resolve with Fact 8
G5: ?- married(rachel,jennifer), female(rachel).     Resolve with Rule 5
G6: ?- wife(rachel,jennifer), female(rachel).     
                    Fail.  Backtrack to G5. Resolve G5 with Rule 6
G7: ?- wife(jennifer,rachel), female(rachel).     
                    Fail.  Backtrack to G3. Resolve G3 with Fact 9
G8: ?- parent(mark,Z1),married(Z1,jennifer), female(rachel).
                                                     Resolve with Fact 9
G9: ?- married(rachel,jennifer), female(rachel).  Resolve with Rule 5
G10: ?- wife(rachel,jennifer), female(rachel).     
                    Fail.  Backtrack to G9. Resolve G9 with Rule 6
G11: ?- wife(jennifer,rachel), female(rachel).     
                    Fail.  Backtrack to G8. Resolve G8 with Fact 10
G12: ?- married(sam,jennifer), female(rachel).    Resolve with Rule 5.
G13: ?- wife(sam,jennifer), female(rachel).     
                    Fail.  Backtrack to G12. Resolve G12 with Rule 6.
G13: ?- wife(jennifer,sam), female(rachel).     Resolve with Fact 12.
G14: ?- female(rachel).    Resolve with fact 14.
G15: Null

And/Or tree

N1 : AND: sister_in_law(rachel,jennifer)
N2 : OR: sister_in_law(rachel,jennifer)
N3:  AND: sibling(rachel,Z1), married(Z1,jennifer), female(rachel). 
N4:  AND: wife(rachel,Z1), sibling(Z1,jennifer).
N5:  AND: wife(rachel,W1), sibling(W1,Z1), married(Z1,jennifer).  
N6:  OR: sibling(rachel,Z1).
N7:  OR: married(Z1,jennifer)
N8:  OR: female(rachel)
N9:  AND: parent(Y2,rachel), parent(Y2,Z1).
N10: AND: wife(Z1,jennifer)
N11: AND: wife(jennifer,Z1).
N12: OR: parent(Y2,rachel)
N13: OR: parent(Y2,Z1).

Suggested exercise (Not required): Construct a similar section of the state-space and the constrained AND-OR tree for the goal "sister_in_law(jennifer,rachel)