12.2.1 Resolution Principle (1) : - Resolution Refutation Proves A Theorem by
12.2.1 Resolution Principle (1) : - Resolution Refutation Proves A Theorem by
12.2.1 Resolution Principle (1) : - Resolution Refutation Proves A Theorem by
1 Resolution Principle(1)
4
Resolution Theorem Proving
12.2.1 Resolution Principle(4)
4. ¬die(fido) ¬die(fido)
{fido/Y}
die(fido) ¬die(fido)
q Skolemization
Ü Skolem constant
Ø ( X)(dog(X)) may be replaced by dog(fido) where the name fido
is picked from the domain of definition of X to represent that
individual X.
Ü Skolem function
Ø If the predicate has more than one argument and the
existentially quantified variable is within the scope of universally
quantified variables, the existential variable must be a function
of those other variables.
Ø ( X)( Y)(mother(X,Y)) ( X)mother(X,m(X))
Ø ( X)( Y)( Z)( W)(foo (X,Y,Z,W))
( X)( Y)( W)(foo(X,Y,f(X,Y),w))
f ¬f
q “Lucky student”
1. Anyone passing his history exams and winning the lottery is
happy
Ø X(pass(X,history) win(X,lottery) → happy(X))
2. Anyone who studies or is lucky can pass all his exams.
Ø X Y(study(X) lucky(X) → pass(X,Y))
3. John did not study but he is lucky
Ø ¬study(john) lucky(john)
4. Anyone who is lucky wins the lottery.
Ø X(lucky(X) → win(X,lottery))
{U/X}
¬pass(U, history) happy(U) ¬lucky(U) ¬happy(john)
{john/U}
lucky(john) ¬pass(john,history) ¬lucky(join)
{}
¬pass(john,history) ¬lucky(V) pass(V,W)
{john/V,history/W}
¬lucky(john) lucky(john)
{}
q “Exciting Life”
1. All people who are not poor and are smart are happy.
Ø X(¬poor(X) smart(X) → happy(X))
2. Those people who read are not stupid.
Ø Y(read(Y) → smart(Y))
Ø {assume X(smart(X) ¬stupid(X))}
3. John can read and is wealthy.
Ø read(john) ¬poor(john)
Ø {assume Y(wealthy(Y) ¬poor(Y))}
4. Happy people have exciting lives.
Ø Z(Happy(Z) → exciting(Z))
5. Negate the conclusion.
Ø “Can anyone be found with an exciting life?”
Ø X(exciting(W))
{Z/W}
¬happy(Z) poor(X) ¬smart(X) happy(X)
{X/Z}
poor(X) ¬smart(X) ¬read(Y) smart(Y)
{Y/X}
¬poor(john) poor(Y) ¬read(Y)
{john/Y}
¬read(john) read(john)
{}
{Z/X}
¬read(Y) smart(Y) exciting(Z) poor(Z) ¬smart(Z)
{Y/Z}
¬read(Y) exciting(Y) poor(Y) ¬poor(john)
{john/Y}
read(john) ¬read(john) exciting(john)
{}
exciting(john) ¬exciting(W)
{}
q Strategies
Ü Breadth-First Strategy
Ü Set of Support Strategy
Ü Unit Preference Strategy
Ü Linear Input Form Strategy
{X/Z}
{library/X}
at(fido, library)
{Z/W} {Z/W}
exciting(Z)
¬happy(Z) poor(X) ¬smart(X) happy(X)
{X/Z} {X/Z}
poor(X) ¬smart(X)
¬read(Y) smart(Y)
exciting(X)
{Y/X}
{Y/X}
¬poor(john) poor(Y) ¬read(Y)
exciting(Y)
{john/Y} {john/Y}
{} {}
exciting(john)
Resolution Theorem Proving 32