Lecture 8
Resolution
Dr. Firas Omari
Resolution Theorem Proving
is a technique for proving theorems in the predicate logic using the resolution by
refutation algorithm. The resolution refutation proof procedure answers a query or
deduces a new result by reducing the set of clauses to a contradiction.
The Resolution by RefutationAlgorithm includes the following steps:-
a) Convert the statements to predicate calculus (predicate logic).
b) Convert the statements from predicate calculus to clause form.
c) Add the negation of what is to be proved to the clause form.
d) Resolve the clauses to producing new clauses and producing a
contradiction by generating the empty clause.
Clause Form
The statements that produced from predicate calculus method are
nested and very complex to understand, so this will lead to more
complexity in resolution stage, therefore the following steps are used to
convert the predicate calculus to clause form:-
1. Eliminate (→) by replacing each instance of the form (P → Q) by
expression (ךP˅Q)
2. Reduce the scope of negation.
➢ ך(ךa) ≡ a
➢ (ךa^b) ≡ךa ˅ךb
➢ (ךa˅b) ≡ךa ˄ךb
3. Standardize variables: rename all variables so that each
quantifier has its own unique variable name. For example,
➢ ∀X a(X) ˅ ∀X b(X) ≡ ∀X a(X) ˅ ∀Y b(Y)
4. Move all quantifiers to the left without changing their order.
For example,
➢ ∀X a(X) ˅ ∀Y b(Y) ≡ ∀X ∀Y a(X) ˅ b(Y )
5. Eliminate existential quantification by using the equivalent
function. For example,
➢ ∀X ∃Y mother(X,Y) ≡ ∀X mother(X,m(X))
➢ ∀X ∀Y ∃Z p(X,Y,Z) ≡ ∀X ∀Y p(X,Y, f(X,Y))
6. Remove universal quantification symbols. For example,
➢ ∀X ∀Y p(X,Y, f(X,Y)) ≡ p(X,Y, f(X,Y))
7. Use the associative and distributive properties to get a
conjunction of disjunctions called conjunctive Normal (CNF) Form
. For example,
➢ a˅(b˅c)≡(a˅b)˅c
➢ a^(b^c)≡(a^b)^c
➢ a˅(b^c)≡(a˅b)^(a˅c)
➢ a^(b˅c)≡(a^b)˅(a^c)
8. Split each conjunct into a separate clause. For example,
➢ (ךa(X)˅ ךb(X)˅e(W)) ^ (ךb(X)˅ךd(X,f(X))˅e(W))
✓ ךa(X)˅ ךb(X)˅e(W)
✓ ךb(X)˅ךd(X,f(X))˅e(W)
9. Standardize variables again so that each clause contains
variable names that do not occur in any other clause. For
example,
➢ (ךa(X)˅ ךb(X)˅e(W)) 𝖠 (ךb(X)˅ךd(X,f(X))˅e(W))
✓ ךa(X)˅ךb(X)˅e(W)
✓ ךb(Y)˅ךd(Z,f(Z))˅e(V)
Example1: Use the Resolution Algorithm for proving that
John is happy with regard the following story:
Everyone passing his AI exam and winning the lottery is happy.
But everyone who studies or lucky can pass all his exams. John
did not study but he is lucky. Everyone who is lucky wins the
lottery.
Solution:
A. Convert all statements to predicate calculus.
• ∀X pass((X,ai_exam)^win(X,lottery)(→happy(X)
• ∀X ((study(X) ˅ lucky(X))→ ∀E pass(X,E)
• ךstudy(john) ^ lucky(john)
• ∀X lucky(X) →win(X,lottery)
• happy (john) Required to prove it
B. Convert the statements from predicate calculus to clause
form.
1. Remove (→)
• ∀X (ךpass(X,ai_exam) ^ win(X,lottery))˅ happy(X)
• ∀X (ךstudy(X)˅lucky(X)) ˅ ∀E pass(X,E)
• ךstudy(john) ^ lucky(john)
• ∀X (ךlucky(X))˅ win(X,lottery)
2. Reduce ך
• ∀X (ךpass(X,ai_exam) ˅ ךwin(X,lottery)) ˅ happy(X)
• ∀X (ךstudy(X)^^ךlucky(X)) ˅ ∀E pass(X,E)
• ךstudy(john) ^lucky(john)
• ∀X ךlucky(X)˅win(X,lottery)
3. Standardize Variables
• ∀X (ךpass(X,ai_exam)˅ךwin(X,lottery))˅ happy(X)
• ∀Y (ךstudy(Y)^ךlucky(Y))˅ ∀E pass(Y,E)
• ךstudy(john) ^lucky(john)
• ∀Z ךlucky(Z)˅win(Z,lottery)
4. Move all quantifiers to the left
• ∀X (ךpass(X,ai_exam)˅ךwin(X,lottery))˅ happy(X)
• ∀Y ∀E (ךstudy(Y)^ךlucky(Y))˅ pass(Y,E)
• ךstudy(john)^lucky(john)
• ∀Z ךlucky(Z)˅win(Z,lottery)
5. Remove ∃
• Nothing to do here.
6. Remove ∀
• (ךpass(X,ai_exam) ˅ךwin(X,lottery))˅ happy(X)
• (ךstudy(Y)^ךlucky(Y)) ˅ pass(Y,E)
• ךstudy(john) ^ lucky(john)
• ךlucky(Z) ˅ win(Z,lottery)
7. CNF
• ךpass(X,ai_exam)˅ךwin(X,lottery)˅ happy(X)
•(ךstudy(Y)^ךlucky(Y))˅ pass(Y,E) ≡ The second
statement becomes:
pass(Y,E)˅ךstudy(Y)^pass(Y,E)˅ךlucky(Y)
• ךstudy(john)^lucky(john)
• ךlucky(Z)˅win(Z,lottery)
8. Split 𝖠
• ךpass(X,ai_exam)˅ךwin(X,lottery)˅ happy(X)
• pass(Y,E)˅ךstudy(Y)
• pass(Y,E)˅ךlucky(Y)
• ךstudy(john)
• lucky(john)
• ךlucky(Z)˅win(Z,lottery)
9. Standardize Variables
• ךpass(X,ai_exam)˅ךwin(X,lottery)˅ happy(X)
• pass(Y,E)˅ךstudy(Y)
• pass(M,G)˅ךlucky(M)
• ךstudy(john)
• lucky(john)
• ךlucky(Z)˅win(Z,lottery)
C. Add the negation of what is to be proved to the clause form.
• ךhappy(john).
added it to the other six clauses and shown below:
• ךpass(X,ai_exam)˅ךwin(X,lottery)˅happy(X)
• pass(Y,E)˅ךstudy(Y)
• pass(M,G)˅ךlucky(M)
• ךstudy(john)
• lucky(john)
• ךlucky(Z)˅win(Z,lottery)
• ךhappy(john).
D. Resolve the clauses to producing new clauses and producing
a contradiction by generating the empty clause.
• There are two types of resolution, the first one is backward resolution
and the second is forward resolution.
d_1) Backward Resolution
The proving for happy(john) using Backward Resolution is shown as follows:
d_2) Forward Resolution
The proving for happy(john) using Forward Resolution is shown as
follows:
Example2: Given the following Predicate logic statements, prove
∃W¬ s(W) using Backward resolution:
(1) ∀X[ (∀Y s(Y) ^ v(X, Y)) ⇒ ((∃Z ¬ t(X, Z)) ^ v(X, X)) ]
(2) ∀X∀Y s(Y) ⇒ t(X,Y) ^v (X,Y)
B. Convert the predicate logic statements to clause form:
Solution:
(1) ∀X[ (∀Y s(Y) ^ v(X, Y)) ⇒ ((∃Z ¬ t(X, Z)) ^ v(X, X)) ]
1-1) Remove ⇒: ∀X [¬(∀Y s(Y) ^ v(X,Y)) ∨ ((∃Z ¬ t(X,Z)) ^ v(X,X)) ]
1-2) Reduce ¬: ∀X [ (∃Y ¬s(Y) ∨ ¬v(X,Y)) ∨ ((∃Z ¬t(X,Z)) ^ v(X,X)) ]
1-3) Standardize Variables: Nothing to do here.
1-4) Move quantifiers: ∀X ∃Y ∃Z [ (¬s(Y) ∨ ¬v(X,Y)) ∨ (¬t(X,Z) ^v(X,X))]
1-5) Remove ∃:∀X [(¬s(f1(X)) ∨ ¬v(X,f1(X))) ∨ (¬ t(X,f2(X)) ^ v(X,X)) ]
1-6) Remove ∀: (¬s(f1(X)) ∨ ¬v(X,f1(X))) ∨ (¬t(X,f2(X))^ v(X,X))
1-7) CNF: (¬s(f1(X)) ∨ ¬v(X,f1(X)) ∨ ¬ t(X,f2(X))) ^(¬s(f1(X)) ∨
¬v(X,f1(X)) ∨ v(X,X))
1-8) Split ^: ¬s(f1(X))
∨ ¬v(X,f1(X)) ∨ ¬ t(X,f2(X))
¬s(f1(X)) ∨ ¬v(X,f1(X)) ∨v(X,X)
1-9) Standardize Variables:
¬s(f1(X)) ∨ ¬v(X,f1(X)) ∨ ¬ t(X,f2(X))
¬s(f3(X3)) ∨ ¬v(X3,f3(X3)) ∨ v(X3,X3)
(2) ∀N∀M s(M) ⇒ t(N, M) ^ v(N, M)
2-1) Remove ⇒: ∀N∀M ¬s(M) ∨ (t(N, M) ^ v(N, M))
2-2) 2-3)2-4)2-5) Nothing to do here
2-6) Remove ∀: ¬s(M) ∨ (t(N, M) ^ v(N, M))
2-7) CNF: (¬s(M) ∨ t(N, M))^ (¬s(M) ∨ v(N, M))
2-8) Split 𝖠: ¬s(M) ∨ t(N, M)
¬s(M) ∨ v(N, M)
2-9) Standardize Variables:
¬s(M) ∨ t(N, M)
¬s(M1) ∨ v(N1, M1)
After applying the clause form method, the two sentences
become four clauses as follows:
• ¬s(f1(X)) ∨ ¬v(X,f1(X)) ∨ ¬ t(X,f2(X))
• ¬s(f3(X3)) ∨ ¬v(X3,f3(X3)) ∨ v(X3,X3)
• ¬s(M) ∨ t(N, M)
• ¬s(M1) ∨ v(N1, M1)
C. Add the negation of what is to be proved ∃W ¬ s(W)
Thus, ∃W ¬ s(W) become s(W) because ¬(∃W ¬ s(W) ) = ∀W
s(W) = s(W). Now we have a new clause (5. s(W).)
added to the other four clauses and shown below:
• ¬s(f1(X)) ∨ ¬v(X,f1(X)) ∨ ¬ t(X,f2(X))
• ¬s(f3(X3)) ∨ ¬v(X3,f3(X3)) ∨ v(X3,X3)
• ¬s(M) ∨ t(N, M)
• ¬s(M1) ∨ v(N1, M1)
• s(W)
D. Backward Resolution
