- 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. 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).

16. male(philip). Facts

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).

- 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)".

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.)

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)

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)"

Example: Suppose you start with the following knowledge base.

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. 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).

16. male(philip). Facts

17. female(elizabeth).

18. son(charles,philip,elizabeth).

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);

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

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

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).

16. male(philip). Facts

17. female(elizabeth).

18. child(charles,philip,elizabeth).

19. child(anne,philip,elizabeth).

24. male(charles). 25. female(anne).

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:

- 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.