Open Mind Tree

Horn clause logic

• A rule: 1 positive literal, at least 1 negative literal. A rule has the form "~P1 V ~P2 V ... V ~Pk V Q". This is logically equivalent to "[P1^P2^ ... ^Pk] => Q"; thus, an if-then implication with any number of conditions but one conclusion. Examples: "~man(X) V mortal(X)" (All men are mortal); "~parent(X,Y) V ~ancestor(Y,Z) V ancestor(X,Z)" (If X is a parent of Y and Y is an ancestor of Z then X is an ancestor of Z.)
• A fact or unit: 1 positive literal, 0 negative literals. Examples: "man(socrates)", "parent(elizabeth,charles)", "ancestor(X,X)" (Everyone is an ancestor of themselves (in the trivial sense).)
• A negated goal : 0 positive literals, at least 1 negative literal. In virtually all implementations of Horn clause logic, the negated goal is the negation of the statement to be proved; the knowledge base consists entirely of facts and goals. The statement to be proven, therefore, called the goal, is therefore a single unit or the conjuction of units; an existentially quantified variable in the goal turns into a free variable in the negated goal. E.g. If the goal to be proven is "exists (X) male(X) ^ ancestor(elizabeth,X)" (show that there exists a male descendent of Elizabeth) the negated goal will be "~male(X) V ~ancestor(elizabeth,X)".
• The null clause: 0 positive and 0 negative literals. Appears only as the end of a resolution proof.

   ~Phi resolves with C1 from Gamma, generating negated goal P2
    P2 resolves with C2 from Gamma, generating negated goal P3
   ...
    Pk resolves with C2 from Gamma, generating the null clause.

• A state is a negated goal.
• A operator on negated goal P is to resolve it with a clause C from Gamma.
• The start state is ~Phi
• The goal state is the null clause.

Backward Chaining

bc(in P0 : negated goal;
      GAMMA : set of facts and rules;)
{ if P0 = null then succeed;
  pick a literal L in P0;
  choose a clause C in GAMMA whose head resolves with L;
  P := resolve(P0,GAMMA);
  bc(P,GAMMA)
}

Prolog

• The clauses in Gamma are ordered by the programmer, and the state space search above is carried out in depth-first search order.
• The negative literals in each clause are ordered by the programmer. When negative goal P is resolved with clause C, the negative literals in C are placed in order at the start of P.
• The "pick" operation picks the first literal in P. Thus, P is implemented as a LIFO stack.

• There are additional functionalities besides theorem proving, such as functions to assert statements, functions to do arithmetic, functions to do I/O.
• The "cut" operator allows the user to prune branches of the search tree.
• The unification routine is not quite correct, in that it does not check for circular bindings e.g. X -> Y, Y -> f(X).)

 
1. ancestor(X,X).
2. ancestor(X,Z) :- parent(X,Y), ancestor(Y,Z).
3. parent(george,sam).
4. parent(george,andy).
5. parent(andy,mary).
6. male(george).
7. male(sam).
8. male(andy).
9. female(mary).

G0:  ~ancestor(george,Q) V ~female(Q).   Resolve with 1: Q=X1=george.
  G1: ~female(george)                   Fail. Return to G0.
G0:  ~ancestor(george,Q) V ~female(Q).   Resolve with 2: X2=george. Z2=Q.
  G2:  ~parent(george,Y2) V ~ancestor(Y2,Q) V ~female(Q).   
                                         Resolve with 3: Y2=sam. 
    G3: ~ancestor(sam,Q) V ~female(Q).   Resolve with 1: Q=X3=sam. 
       G4: ~female(sam).                 Fail. Return to G3. 
    G3: ~ancestor(sam,Q) V ~female(Q).   Resolve with 2: X4=sam, Z4=Q
       G5: ~parent(sam,Y2) V ~ancestor(Y2,Q) V ~female(Q).   
                                         Fail. Return to G3.
    G3: ~ancestor(sam,Q) V ~female(Q).   Fail. Return to G2.
  G2: ~parent(george,Y2) V ~ancestor(Y2,Q) V ~female(Q).   
                                         Resolve with 4: Y2=andy. 
    G6: ~ancestor(andy,Q) V ~female(Q).  Resolve with 1: X5=Q=andy
       G7: ~female(andy).                Fail. Return to G6.
    G6: ~parent(andy,Y6) V ~ancestor(Y6,Q) V ~female(Q).  
                                         Resolve with 5: Y6=mary.
       G8: ~ancestor(mary,Q) V ~female(mary). Resolve with 1: X7=Q=mary.
          G9: ~female(mary)              Resolve with 9.
             Null.

Forward chaining

procedure add_fact(in F; in out GAMMA) 
   /* adds fact F to knowledge base GAMMA and forward chains */
if F is not in GAMMA then {
   GAMMA := GAMMA union {F};
   for each rule R in GAMMA do {
      let ~L be the first negative literal in R;
      if L unifies with F then
       then { resolve R with F to get C;
              if C is a fact then add_fact(C,GAMMA)
              else /* C is a rule */ add_rule(C,GAMMA)
            }
      }
   }
end add_fact.

procedure add_rule(in R; in out GAMMA) 
   /* adds rule R to knowledge base GAMMA and forward chains */
if R is not in GAMMA then {
   GAMMA := GAMMA union {R};
   let ~L be the first negative literal in R;
   for each fact F in GAMMA do 
     if L unifies with F 
       then { resolve R with F to get C;
              if C is a fact then add_fact(C,GAMMA)
              else /* C is a rule */ add_rule(C,GAMMA)
            }
   }
end add_fact.

procedure answer_query(in Q, GAMMA) return boolean /* Success or failure */
{ QQ := {Q} /* A queue of queries
  while QQ is non-empty do {
      Q1 := pop(QQ);
      L1 := the first literal in Q1;
      for each fact F in GAMMA do 
        if F unifies with L
          then { resolve F with Q1 to get Q2;
                 if Q2=null then return(true)
                            else add Q2 to QQ;
               }
      }
  return(false)

Choice between forward and backward chaning

animal(X) :- sponge(X).
animal(X) :- arthopod(X).
animal(X) :- vertebrate(X).
...
vertebrate(X) :- fish(X).
vertebrate(X) :- mammal(X)
...
mammal(X) :- carnivore(X)
...
carnivore(X) :- dog(X).
carnivore(X) :- cat(X).
...

breathes(X) :- animal(X).
...
backbone(X) :- vertebrate(X).
has(X,brain) :- vertebrate(X).
...
furry(X) :- mammal(X).
warm_blooded(X) :- mammal(X).
...

Constrained AND/OR tree