lec9

Resolution and Unification : 

11/28/2008 1 Resolution and Unification CIS 479/579 Bruce R. Maxim UM-Dearborn

Resolution : 

11/28/2008 2 Resolution Proves statements are true by refutation If you negate the statement to be proved you get a contradiction to statements already known to be true The resolution procedure is an iterative process such that at each step of the process two clauses are combined to produce a new clause

Propositional Calculus Resolution Algorithm : 

11/28/2008 3 Propositional Calculus Resolution Algorithm Convert all propositions of F to clause form Negate P and convert result to clause form and the result to the clauses obtained in step 1. Repeat until either a contradiction occurs or no progress can be made: Select two clauses call these parent clauses Resolve the clauses using disjunction if any pairs of literal L or ~L occur in the two parent clauses pick one and eliminate it from the result If the result is empty then the contradiction has been found otherwise add the result to the set of clauses

Example : 

11/28/2008 4 Example Suppose you have two clauses winter or summer ~winter or cold Using resolution we get winter or summer or ~winter or cold We pick winter and get summer or cold This is not a contradiction so we would need to continue or give up

Conversion to Clause Form : 

11/28/2008 5 Conversion to Clause Form Suppose we know that all Romans who know Marcus either hate Caesar or think that anyone who hates anyone is crazy As a wff (well formed formula) x:[Roman(x)  know(x,Marcus)]  [hate(x,Caesar)  (y: z : hate(y, z)  thinkcrazy(x, y))] In conjunctive normal or clause form ~Roman(x)  ~know(x,Marcus)  hate(x,Caesar) ~hate(y,z)  thinkcrazy(x,z)

Algorithm to Convert to Clause Form : 

11/28/2008 6 Algorithm to Convert to Clause Form Eliminate  using “a  b” is same as ~a  b Reduce scope of ~ to a single term using deMorgan’s laws (e.g. ~(a  b) is ~a  ~b) Standardize variables so each quantifier binds a unique variable (e.g. x : P(x)  x: Q(x) becomes P(x)  y: Q(y)) Move all quantifiers to the left without changing their relative order Eliminate all existential quantifiers Since all remaining variables universally quantified drop the  prefix

Algorithm to Convert to Clause Form : 

11/28/2008 7 Algorithm to Convert to Clause Form Use distributive property to convert expression into conjunction of disjuncts (e.g. this makes (a  b)  c become (a  c)  (b  c) ) Create separate clause corresponding to each conjunct (each of which must be true) Standardize apart the variables in the clauses generated by the previous step so that no two clauses reference the same two variables

Unification in Predicate Calculus : 

11/28/2008 8 Unification in Predicate Calculus It is easy to see that two literal cannot be both true and false in propositional calculus It is harder to see in predicate calculus since man(John) and ~man(John) is a contradiction man(John) and ~man(Spot) is not Basic idea behind unification of two literals is to check their predicate symbol for a match and then see if we can find a consistent set of substitutions that work (like we did in Prolog)

Example : 

11/28/2008 9 Example These two literals hate(x, y) hate(Marcus, z) can be unified using any of these substitutions Marcus = x z = y Marcus = x y = z Marcus = x Caesar = y Caesar = z Marcus = x Polonius = y Polonius = z

Unification Algorithm : 

11/28/2008 10 Unification Algorithm Unify(L1, L2) If L1 or L2 are both variables or constants then If L1 and L2 are identical then return NIL If L1 is a variable then if L1 occurs in L2 then return FAIL else return substituting L2 for L1 If L2 is a variable then if L2 occurs in L1 then return FAIL else return substituting L1 for L2 Return FAIL If the initial predicate symbols in L1 and L2 are not identical then return FAIL

Unification Algorithm : 

11/28/2008 11 Unification Algorithm If L1 and L2 have different numbers of arguments then return FAIL Set SUBST to NIL For I = 1 to number of arguments in L1 Call Unify with ith argument of L1 and ith argument of L2 and store result in S If S = FAIL then return FAIL If S <> NIL then Apply S to remainder of L1 and L2 SUBST = Append(S, SUBST) Return SUBST

Resolution in Predicate Calculus : 

11/28/2008 12 Resolution in Predicate Calculus We now are able to determine when two literals are contradictory They are contradictory when one of them can be unified with the negation of the other

Predicate Resolution : 

11/28/2008 13 Predicate Resolution Given set of statements F and statement to prove P Convert all statements of F to clause form Negate P, convert result to clause form, and add it to set of clauses from step 1 Repeat until either a contradiction is found, no progress can be made, or predefined is expended Select two clauses call them parent clauses Resolve the two parent clauses If resultant is empty then contradiction has been found otherwise add result to set of clauses and continue process

Natural Deduction : 

11/28/2008 14 Natural Deduction Depends on uniform representation Can lead to ambiguous interpretation of clauses People don’t think using resolution (so this is a computational process not psychological model)