Inference in Datalog

Datalog: The subset of the predicate calculus consisting of sentences with Since all variables are universally quantified, with a scope of the entire sentence, there is no need to actually write down the quantifiers, as long as there is some convention about which symbols are variables and which are constants. Here, I will use upper case for variables and lower case for constants.

Thus, all sentences have either the form.

1. PRED(TERM ... TERM); or
2. [PRED(TERM ... TERM) ^ PRED(TERM ... TERM) ^ ... ^ PRED(TERM ... TERM)] =>
PRED(TERM ... TERM)
where all the TERM's are either variables or constants.

Sentences of form (1) are called "facts"; sentences of form (2) are called "rules". The formula on the right hand of the implication of a rule is called the "head" of the rule; the formulas on the left hand are the "tail" of the rule.

Example

The following is a Datalog knowledge base describing a family tree and rules for relations:
Rules
1. parent(X,Y) ^ male(X) => father(X,Y).
2. father(X,Y) => parent(X,Y).
3. father(X,Y) => male(X).
4. parent(X,Y) ^ female(X) => mother(X,Y).
5. mother(X,Y) => parent(X,Y).
6. mother(X,Y) => female(X).
7. parent(Y,X) ^ parent(Z,X) => child(X,Y,Z).
8. child(X,Y,Z) => parent(Y,X).
9. child(X,Y,Z) => parent(Z,X).
10. son(X,Y,Z) => child(X,Y,Z). 11. son(X,Y,Z) => male(X). 12. male(X) ^ child(X,Y,Z) => son(X,Y,Z).
13. daughter(X,Y,Z) => child(X,Y,Z).
14. daughter(X,Y,Z) => female(X).
15. female(X) ^ child(X,Y,Z) => daughter(X,Y,Z).

Facts
16. male(philip).
17. female(elizabeth).
18. son(charles,philip,elizabeth).
19. daughter(anne,philip,elizabeth).
20. son(andrew,philip,elizabeth).
21. son(edward,philip,elizabeth).
22. son(william,charles,diana).
23. son(harry,charles,diana).
The following sentences in predicate calculus cannot be expressed in Datalog:

Inference

The method of inference we will discuss is a mixture of two ideas:

I. Modus Ponens. From the sentences

[P^Q^R^S] => W.
P.
Q.
R.
S.
you can infer W.

II. (Universal instantiation) From the sentence "forall(X) P(X)" you may infer P(T) for any term T.

Now, suppose we have the sentences

1. forall(X) man(X) => mortal(X). (All men are mortal)
2. man(socrates).
Then we can proceed as follows: The question is, how did we know to replace X in (1) by "socrates" rather than, say "eiffel_tower" or anything else? The answer is that we chose to replace X by socrates in order to make possible the use of modus ponens. This is done by unifying the atomic formula "man(X)" in (1) with the formula "man(socrates)" in (2).

Substitution and Unification in Datalog

A substitution in Datalog is a collection of disjoint sets of variable symbols and constant symbols such that each component set contains no more than one constant symbol.

Example: The collection { {X.Y.a}, {Z,b}, {W}, {P,Q}, {c}} is a valid substitution. (Again, variables are upper-case; constants are lower case.)

Non-examples. The collection {{X,Y,a}, {X,b}} is not a valid substitution (X appears in two sets). The collection {{X,a,b}, {Y}} is not a valid substitution (the first set contains two constant symbols.)

Applying substitution U to sentence S = PRED(T1 ... Tk)

1. For each set E in U, choose a representative element R(E). If E contains a constant symbol, then R(E) must be that constant; otherwise, it can be any of the variable symbols.

2. For each term Ti, if Ti is a variable, then replace Ti in S by the representative of the set that contains Ti.

Example Let U be the collection { {X.Y.a}, {Z,b}. {W}, {P,Q}, {c}} and let S be the sentence
f(X,Y,c) ^ g(Y,Z,W) ^ h(P,c,X) => h(X,c,Q)

1. We may choose the representatives a,b,W,Q,c.
2. The result of applying the substitution to the sentence is then f(a,a,c) ^ g(a,b,W) ^ h(Q,c,a) => h(a,c,Q)

Unifying two atomic formulas

Let F1 and F2 be two atomic formulas with no variables in common. A substitution U unifies formulas F1 and F2 if the result of apply(U,F1) = apply(U,F2).

Let F1 be the formula "P(T1 ... Tk)" and let F2 be the formula "Q(V1 ... Vm)"

unify(F1,F2) : returns either a unifying substitution, or NIL if there is no
               unifying substitution

{ if (P != Q or k != m) then return(NIL);
  C = collection containing each of the symbols in different sets;
  for i = 1 to k do {
    let E(Ti) and E(Vi) be the sets in C containing Ti and Vi;
    if E(Ti) and E(Vi) each contain a constant (necessarily different) 
       then return(NIL);
    if (Ti != Vi) then merge Ti with Vi in C;
    } 
  return(C);
}
(Application of the "UNION-FIND" or "MERGE-FIND" algorithm.)

Example: To unify the formula F1="p(a,X,b,X,Y,W)" with F2="p(U,U,T,V,c,T)":

Since both formulas have predicate "p" and 6 arguments,
Initialize C to be {{a}, {b}, {c}, {T}, {U}, {V}, {W}, {X}, {Y}}
Step 1: T1="a", V1="U". Merge {a} with {X}.
C  = {{a,U}, {b}, {c}, {T}, {V}, {W}, {X}, {Y}}
Step 2: T2="X", V2="U". Merge {X} with {a,U} 
C  = {{a,U,X}, {b}, {c}, {T}, {V}, {W}, {Y}}
Step 3: T3="b", V3="T". Merge {b} with {T} 
C  = {{a,U,X}, {b,T}, {c}, {V}, {W}, {Y}}
Step 4: T4="X", V4="V". Merge {a,U,X} with {V} 
C  = {{a,U,X,V}, {b,T}, {c}, {W}, {Y}}
Step 5: T5="Y", V5="c". Merge {Y} with {c} 
C  = {{a,U,X,V}, {b,T}, {c,Y}, {W}} 
Step 6: T6="W", V6="T". Merge {W} with {b,T}
C = {{a,U,X,V}, {b,T,W}, {c,Y} }
Note that apply(C,F1) = apply(C,F2) = "p(a,a,b,a,c,b)"

Forward Chaining

The basic idea in forward chaining is this: You look for unifications that will match each of the formulas in the left hand side of a known rule to known facts. You can then infer the right hand side of the rule under the specified substitution. This is a fact that you can add to the knowledge base. You keep doing this until there is nothing new to be derived, then stop.

Example: Suppose you start with the following knowledge base.

Rules
1. parent(X,Y) ^ male(X) => father(X,Y).
2. father(X,Y) => parent(X,Y).
3. father(X,Y) => male(X).
4. parent(X,Y) ^ female(X) => mother(X,Y).
5. mother(X,Y) => parent(X,Y).
6. mother(X,Y) => female(X).
7. parent(Y,X) ^ parent(Z,X) => child(X,Y,Z).
8. child(X,Y,Z) => parent(Y,X).
9. child(X,Y,Z) => parent(Z,X).
Facts
16. male(philip).
17. female(elizabeth).
18. son(charles,philip,elizabeth).
We can proceed as follows:
Combining rule (8) with fact (18) with substitution {{X,charles},{Y,elizabeth}, {Z,philip}}, infer (24) parent(elizabeth,charles)

Combining rule (9) with fact (18) with substitution {{X,charles},{Y,elizabeth}, {Z,philip}}, infer (25) parent(philip,charles)

Combining rule (1) with facts (16) and (25) with substitution {{X, philip}. {Y, charles}} infer (26) father(philip,charles).

Combining rule (4) with facts (17) and (24) with substitution {{X, elizabeth}. {Y, charles}} infer (27) mother(elizabeth,charles).

No further facts can be derived.

IMPORTANT NOTE: Each time you are trying to unify a fact with a set of rules, you must rename the variables so that no two of the sentences use the same variable names.

Here is some pseudo-code to do forward chaining exhaustively. I am not going to go through this in detail.

fc(RR : set of rules; FF: set of facts) return set of facts. {
repeat { NEW_FACT := false;
         for each rule R = "T1 ^ T2 ^ ... ^ Tk => H" do {
           for each fact F1 in consequences(R,FF) do {
             if (F1 is not in FF)  then
               { NEW_FACT := true;
                 FF := add F1 to FF;
                 }
            }
         }
        }
  until not(NEW_FACT);
}

/* "consequences" recurs down the formulas in the tail of rule R */
consequences(R : rule or fact; FF : set of facts) return set of facts;
{ if (R is a fact) then return(R); /* Base case of the recursion */
  T1 := the first literal in the tail of R;
  NEW_FACTS = empty set;
  for each fact (F in FF) {
     rename the variables in F so as not to conflict with the variables in R;
     U = unify(T1,F);
     if (U != NIL) then {
       R1 := drop T1 from R;
       R1 := apply(U,R1);
       NEW_FACTS = NEW_FACTS union consequences(R1,FF)
      }
    }
  return(NEW_FACTS);

Backward Chaining

In backward chaining you start with a goal , a statement that you want to prove, in addition to the knowledge base, and you look for derivations that allow you to prove the goal. You look for a rule R or a fact F. whose head unifies with the goal, and then recursively try to prove all the formulas in the tail of R.

For instance, suppose that you start with the following knowledge base,

Rules
1. parent(X,Y) ^ male(X) => father(X,Y).
4. parent(X,Y) ^ female(X) => mother(X,Y).
8. child(X,Y,Z) => parent(Y,X).
9. child(X,Y,Z) => parent(Z,X).
12. male(X) ^ child(X,Y,Z) => son(X,Y,Z).
15. female(X) ^ child(X,Y,Z) => daughter(X,Y,Z).

Facts
16. male(philip).
17. female(elizabeth).
18. child(charles,philip,elizabeth).
19. child(anne,philip,elizabeth).
24. male(charles). 25. female(anne).
and the goal is "father(philip,charles)". Backward chaining proceeds as follows:
Goal G0: father(philip,charles).
  Unify G0 with the head of rule (1) with substitution {{X1,philip},{Y1,charles}}
  Subgoals: G1 = "parent(philip,charles)", G2="male(philip)".
    Goal G1: parent(philip,charles)
      Unify G1 with the head of rule (8) with substitution {{X2,charles}, {Y2,philip}, {Z2}} 
      Subgoal G3 = "child(charles,philip,Z2")
         No fact or rule unifies with G3.
         Fail G3
      Try again with G1.
      Unify G1 with the head of rule (9) with substitution {{X3,charles}, {Y3}, {Z3,philip}} 
      Subgoal G3 = "child(charles,Y3,philip)"
         G3 unifies with fact (18) with substitution Y3=elizabeth.
         G3 succeeds.
      G1 succeeds.
    Goal G2: male(philip)
       G2 unifies with fact 16.
       G2 succeeds
G0 succeeds.
If you have a variable in the goal in backward chaining, then the goal is to find _some_ value of the variable that satisfies the formula. For example, if the goal is "child(charles,J,K)", that means "find J and K such that charles is the child of J and K. Backward chaining in that case proceeds as follows.
G0: child(charles,J,K)
  G0 unifies with fact 18, under substitution J=philip, K=elizabeth.
G0 succeeds with J=philip and K=elizabeth.
Another example, suppose the knowledge base is the first one in this file, and the goal is "daughter(J,K)" (Find someone J who is the daughter of someone else K). Backward chaining proceeds as follows:
Goal G0: daughter(J,K,L)
   G0 unifies with rule 15 under the binding J=X, K=Y, Z=L.
   Subgoals: G1="female(J)", G2="child(J,K,L)"

   Goal G1: female(J).
     G1 unifies, either with fact 17 or with fact 25.
     Try unifying G1 with fact 17, with binding J=elizabeth.
     G1 succeeds with binding J=elizabeth

   Goal G2: child(elizabeth,K,L)
     G2 does not unify with any fact or rule.
     G2 fails

   Return to G1 (last point where there was a choice).
     Try unifying G1 with fact 25, with binding J=anne.
     G1 succeeds with binding J=anne.

   Goal G2: child(anne,K,L)
      G2 unifies with fact 19 with binding K=elizabeth, L=philip.
   
   G0 succeeds with J=anne, K=elizabeth, L=philip.
Unlike forward chaining, backward chaining can potentially go into an infinite loop. There are two ways to avoid this: In Datalog, repeated goal detection is sufficient to remove all infinite loops.