- No function symbols.
- No existential quantifiers.
- All sentences have the form
"{ forall(VARS) } ATOMIC-FORM" or

"{ forall(VARS) } [ATOMIC-FORM ^ ATOMIC-FORM ^ ... ^ ATOMIC-FORM] => ATOMIC-FORM"

Thus, all sentences have either the form.

1. PRED(TERM ... TERM); orwhere all the TERM's are either variables or constants.

2. [PRED(TERM ... TERM) ^ PRED(TERM ... TERM) ^ ... ^ PRED(TERM ... TERM)] =>

PRED(TERM ... TERM)

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.

The following sentences in predicate calculus1. parent(X,Y) ^ male(X) => father(X,Y). Rules

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. child(X,Y,Z) => parent(Y,X).

8. child(X,Y,Z) => parent(Z,X).

9. son(X,Y,Z) => child(X,Y,Z).

10. son(X,Y,Z) => male(X).

11. male(X) ^ child(X,Y,Z) => son(X,Y,Z).

12. daughter(X,Y,Z) => child(X,Y,Z).

13. daughter(X,Y,Z) => female(X).

14. female(X) ^ child(X,Y,Z) => daughter(X,Y,Z).

15. male(philip). Facts

16. female(elizabeth).

17. son(charles,philip,elizabeth).

18. daughter(anne,philip,elizabeth).

19. son(andrew,philip,elizabeth).

20. son(edward,philip,elizabeth).

21. son(william,charles,diana).

22. son(harry,charles,diana).

- forall(X) exists(Y,Z) child(X,Y,Z). (Datalog doesn't deal with exists)
- forall(X) male(X) V female(X). (nor with disjunction)
- forall(X) not(male(X) ^ female(X)) (nor with negation).

I. **Modus Ponens.** From the sentences

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

P.

Q.

R.

S.

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)Then we can proceed as follows:

2. man(socrates).

- First, use universal instantiation to replace "X" in (1) by "socrates"
giving
3. "man(socrates) => mortal(socrates)"

- Second, apply modus ponens to (2) and (3), and infer "mortal(socrates)".

- V is a variable.
- W is either a variable or a constant.
- No variable appears on the left hand side of two different pairs.
- No variable appears on the left hand side of one pair and the right hand side of a different pair.

** Example: ** The set { X -> a, Y -> a, Z -> b, P -> Q, M -> Q}
is a substitution.
(Again, variables are upper-case; constants are lower case.)

** Non-examples.** The set {X -> a, X -> b, Y -> z} is not valid because
X is on the left hand of two different pairs. The set
{X -> a, b -> a, Y -> b} is not valid because the constant b appears on
the left hand of a pair. The set { X -> a, Y -> X, Z -> b } is not valid
because X appears on both the left and right side of a pair.
appears in two sets). The collection {{X,a,b}, {Y}} is not a valid

** Example **
Let U be the substitution
{ X -> a, Y -> a, Z -> b, P -> Q, M -> Q}.

Let S be the sentence
f(X,Y,c) ^ g(Y,Z,W) ^ h(P,c,X) => h(X,c,Q)

The result of applying U to S is then

f(a,a,c) ^ g(a,b,W) ^ h(Q,c,a) => h(a,c,Q)

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

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; } B := emptyset; for (S in C) { if (S has more than one element) { if (S contains constant symbol X) /* S contains at most one constant */ for (each variable Q in S) add Q -> X to B; else { X = some variable in S; for (Q != X in S) add Q -> X to B; } } }This can be made very efficient using 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}} First loop: 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} } Second loop: B = { U -> a, X -> a, V -> a, T -> b, W -> b, Y -> c}.Note that apply(C,F1) = apply(C,F2) = "p(a,a,b,a,c,b)"

Example: Suppose you start with the following knowledge base (a subset of the knowledge base at the start of these notes: hence the gappy numbering).

We can proceed as follows:1. parent(X,Y) ^ male(X) => father(X,Y). Rules

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. child(X,Y,Z) => parent(Y,X).

8. child(X,Y,Z) => parent(Z,X).

9. son(X,Y,Z) => child(X,Y,Z).

10. son(X,Y,Z) => male(X).

11. male(X) ^ child(X,Y,Z) => son(X,Y,Z).

15. male(philip). Facts

16. female(elizabeth).

17. son(charles,philip,elizabeth).

Combining rule (9) with fact (17) with substitution {X -> charles, Y -> philip, Z -> elizabeth}, infer (23) child(charles,philip,elizabeth)Combining rule (10) with fact (17) with substitution {X -> charles, Y -> philip, Z -> elizabeth}, infer (24) male(charles).

Combining rule (7) with fact (23) with substitution {X -> charles, Y -> philip, Z -> elizabeth}, infer (25) parent(philip,charles)

Combining rule (8) with fact (23) with substitution {X -> charles, Y -> philip, Z -> elizabeth}, infer (26) parent(elizabeth,charles)

Combining rule (1) with facts (15) and (25) with substitution {X -> philip, Y -> charles} infer (27) father(philip,charles).

Combining rule (4) with facts (16) and (26) with with substitution {X -> elizabeth, Y -> charles} infer (28) 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);A trace of the subroutine "consequences" for a reasonably complicated example is given here

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

and the goal is "mother(elizabeth,charles)". Backward chaining proceeds as follows:1. parent(X,Y) ^ male(X) => father(X,Y). Rules

2. parent(X,Y) ^ female(X) => mother(X,Y).

3. child(X,Y,Z) => parent(Y,X).

4. child(X,Y,Z) => parent(Z,X).

5. male(X) ^ child(X,Y,Z) => son(X,Y,Z).

6. female(X) ^ child(X,Y,Z) => daughter(X,Y,Z).

7. male(philip). Facts

8. female(elizabeth).

9. child(charles,philip,elizabeth).

10. child(anne,philip,elizabeth).

11. male(charles).

12. female(anne).

Goal G0: mother(elizabeth,charles). Unify G0 with the head of rule (1) with substitution {X1->elizabeth, Y1->charles}} Subgoals: G1 = "parent(elizabeth,charles)", G2="female(elizabeth)". Goal G1: parent(elizabeth,charles) Unify G1 with the head of rule (3) with substitution X2 -> charles, Y2 -> elizabeth Subgoal G3 = "child(charles,elizabeth,Z2") No fact or rule unifies with G3. Fail G3 Try again with G1. Unify G1 with the head of rule (4) with substitution X2 -> charles, Y2 -> elizabeth Subgoal G3 = "child(charles,Y3,elizabeth)" G3 unifies with fact (9) with substitution Y3=elizabeth. G3 succeeds. G1 succeeds. Goal G2: female(elizabeth) G2 unifies with fact 8. 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 9, under substitution {J->philip, K->elizabeth}. G0 succeeds with J=philip and K=elizabeth.Another example: if the goal is "daughter(J,K,L)" (find J,K,L such that J is the daughter of K and L) then backward chaining proceeds as follows:

Goal G0: daughter(J,K,L) G0 unifies with rule 6 under the substitution {X1->J, Y1->K, Z1->L} Subgoals: G1="female(J)", G2="child(J,K,L)" Goal G1: female(J). Unify G1 with fact 8, 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 12, with binding J=anne. G1 succeeds with binding J=anne. Goal G2: child(anne,K,L) G2 unifies with fact 10 with binding K->philip, L->elizabeth. 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:

- Responsibility of the knowledge base designer to set up the rules so that this doesn't happen. (Prolog)
- Repeated goal detection: If goal Gi is a subgoal of Gj (direct or indirect) and Gi is identical to Gj, then fail Gi.

(A) forall(X,Z) [exists(Y) parent(X,Y) ^ parent(Y,Z)] => grandparent(X,Z).In that form, this does not satisfy the conditions on Datalog because of the existential quantifier. However, it is logically equivalent to

(B) forall(X,Y,Z) parent(X,Y) ^ parent(Y,Z) => grandparent(X,Z)which is valid Datalog.

Let me give two arguments for this equivalence: an intuitive argument and a formal argument.

** Intuitive argument:**

Sentence (A) means "For any X and Z that we choose, if we can find a Y
such that parent(X,Y) and parent(Y,Z) then grandparent(X,Z)." Now suppose
that Elizabeth is a parent of Charles and Charles is a parent of William,
thus satisfying the condition of (B).
Then the condition of (A) is satisfied for X=Elizabeth and Z=William
we can choose a Y such that parent(elizabeth,Y) and
parent(Y,william); namely, Charles.
Conversely, suppose that Jesse and Solomon satisfy
the condition for (B). That is, there exists some particular Y1 such that
Jesse is a parent of Y1 and Y1 is a parent of Solomon. Therefore, the
condition in (A) is satisfied with X=Jesse, Y=Y1, and Z=Solomon. Thus, (A) and
(B) are equivalent.

** Formal argument:**

(A) forall(X,Z) [exists(Y) parent(X,Y) ^ parent(Y,Z)] => grandparent(X,Z)

is equivalent to

(C) forall(X,Z) ~[exists(Y) parent(X,Y) ^ parent(Y,Z)] V grandparent(X,Z)

which is equivalent to

(D) forall(X,Z) [forall(Y) ~[parent(X,Y) ^ parent(Y,Z)]] V grandparent(X,Z)

which is equivalent to

(E) forall(X,Z) [forall(Y) ~[parent(X,Y) ^ parent(Y,Z)] V grandparent(X,Z)]

which is equivalent to

(B) forall(X,Z) [forall(Y) [parent(X,Y) ^ parent(Y,Z)] => grandparent(X,Z)

(A) is equivalent to (C) and (E) is equivalent to (B)
because P=>Q is always equivalent to ~P V Q.

(C) is equivalent to (D) because ~exists(X) P(X) is always equivalent to
forall(X) ~P(X). (If there does not exists anything satisfying P, then nothing
satisfies P.)

(D) is equivalent to (C) because [forall(X) P(X)] V Q is equivalent to
[forall(X) P(X) V Q] if variable X does not occur in Q.