|a formula g the formula g denotes the sentence obtained by applying the substitution 6 to the fc nple, if g = Likes(?x, ?y) then applying the above substitution gives us the sentence g = Lil ier for two formulas a and B is a substitution that makes the two formulas identical. We say that a unr er unifies a set of formulas {a, aa, ..., an} if, a,0= a=... =ayO= 9 all the common reduced form as the factor. Given a formula a and a formula B > 6 we can modus ponens rule as follows. If a and B have a unifier 6 then infer 58 from a and (B D 6) if a = (Sport(tennis) A Likes(Aditi, tennis))

B > 0= (Sport(?y) A Likes(?x, ?y)) D Watches(?x, ?y) 1 unifies with B with the substitution 6 = {?x = Aditi, 2y = tennis} given above, and one can infer 60 = Watches(?x, ?y) = Watches(Aditi, tennis) times there is a choice between several unifiers. Consider, for example if we had the rule that if a n or equal to another, then the other is larger than or equal to the former. Assuming that in our d umbers everything is a number (and we dont need a category number) we could express it in sk ollows.

SmallerOrEqualThan(?x, ?y) D GreaterOrEqualThan(?y, ?x) Jiven the following fact what are the inferences one can make? SmallerOrEqualThan(0, ?z) niild wea the ciuihetititinn wo f9y N Pv 7 27 = 71 tn infer CreaterOrEqialThan(7 N\ We ern In the following discussion predicate symbols, logical operators, function symbols are all tr s, in the sense that they must match exactly. A variable, on the other hand, is one that can be subs g else (a term). We assume a function /ength is available to determine the length of a list. Two lists d if they have the same length. The following algorithm is along the lines of the version pres k and McDermott, 1985).

) then return VarUnify(list,, list,, theta) if Var(list;) then return VarUnify(list.,, list,, theta) if Constant (list,) then if list, = list, then return theta else return FAIL if constant (list,) then return FAIL if list, = list, = ( ) then return theta if Length(list,) # Length(list,) then return FAIL else return Append( SubUnify(Head(list,), Head(list,), th SubUnify(Rest(list,), Rest(list.), th