Artificial intelligence

​

UNIT-3

RESOLUTION

KVSM, Dept of CSE , SRKREC

Department of Computer Science and Engineering

S R K R Engineering College,

Bhimavaram-534204

KVSM, Dept of CSE , SRKREC

Resolution

Resolution algorithm is used prove sentences in propositional and predicate logic.

​

Resolution produces proof by Refutation, i.e in order to prove the statement P , first we assume that Negation P is correct and proceed further to get the contradiction, so our assumption is wrong and hence the sentence P is proved.

​

In Resolution is a technique of producing a new clause by resolving two clauses that contain a complimentary literal and 

KVSM, Dept of CSE , SRKREC

Resolution Propositional logic

1. Convert all the propositions to WFF then to clause form.

2. Consider the sentence to prove P, Negate P and convert to clause form.

Add this clause to the set of clauses obtained in 1.

​

3. Repeat the following until either a contradiction is found or no progress can be made:

a. Select two clauses. Call these the parent clauses.

b. Resolve them together. The resulting clause, called the resolvent, will be the disjunction of all of the literals of both of the parent clauses

c. If the resolvent is the empty clause, then a contradiction has been found.

If it is not a contradiction , then add it to the set of classes available to the procedure.

KVSM, Dept of CSE , SRKREC

Resolution in propositional logic example

Suppose we are given the following axioms.

1. b ∧ c → a

2. b

3. d ∧ e → c

4. e ∨ f

5. d ∧ ⌐f

We want to prove ‘a’ from these axioms using Resolution.

​

Resolution in propositional logic example

First convert the above propositions in WFF to clause form.

Consider b ∧ c → a

After eliminating 🡪 in step 1 we get ⌐ (b ∧ c) ∨ a

After reducing the scope of negation to single term in step 2 we get ⌐ b ∨ ⌐ c ∨ a

After applying associative law in step 7 we get a U ⌐b ∨ ⌐c ( this is clause form)

The clause form for b is b

Consider d ∧ e → c

After eliminating 🡪 in step 1 we get ⌐ (d ∧ e ) ∨ c

After reducing the scope of negation to single term in step 2 we get ⌐ d ∨ ⌐ e ∨ c

After applying associative law in step 7 we get c ∨ ⌐d ∨ ⌐e ( this is clause form)

Consider e ∨ f this is already in clause form

Consider d ∧ ⌐f

After creating a separate clause for each conjunct in step 8 we get

d ⌐f ( these two are in clause form)

Resolution in propositional logic example

We get the following clauses.

• a U ⌐b U ⌐c
• b
• c U ⌐d U ⌐e
• e U f
• d
• ⌐f

The goal is to prove : a

it is negated and added to the clause set.

Now we have the following clauses :

• a U ⌐b U ⌐c
• b
• c U ⌐d U ⌐e
• e U f
• d
• ⌐f
• ⌐a ( this is our assumption)

The empty clause at the end of the process indicates contradiction.

so our assumption ⌐a is wrong. Hence a is proved.

KVSM, Dept of CSE , SRKREC

Resolution example in propositional logic

Well formed formulas :

(P V Q) ∧ (P V R)

Q 🡪 R

P 🡪 S

(R V S)

⌐ S

Prove R using resolution.

Following are the Clauses

1a. (P V Q) 1b. (P V R)

2. ⌐ Q V R

3. ⌐ P V S

4. R V S

5. ⌐ S

Consider ⌐ R

The empty clause at the end of the process indicates contradiction.

so our assumption ⌐R is wrong. Hence R is proved.

KVSM, Dept of CSE , SRKREC

Resolution in predicate logic

1.Convert all the statements to WFF and then convert to clause form.

2. Consider the sentence to prove P, Negate P and convert to clause form.

Add this clause to the set of clauses obtained in 1.

​

3. Repeat the following until a contradiction found or no progress can be made , or a predetermined amount of effort(time) is reached.

a. Select two clauses, Call these as parent clauses.

b. Resolve them together. The resolvent will be the disjunction of all the literals of both parent clauses with appropriate substitutions suggested by the unification algorithm to create the resolvent.

c. If the resolvent is an empty clause, then a contradiction has found.

If it is not a contradiction , then add it to the set of classes available.

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

Consider the following facts:

1. Marcus was a man.

2. Marcus was a Pompeian.

3. All Pompeians were Romans.

4. Caesar was a ruler.

5. All romans were either loyal to Caesar or hated him.

6. Everyone is loyal to someone.

7. People only try to assassinate rulers they are not loyal to.

• Marcus tried to assassinate Caesar.

Now prove marcus hates caesar using resolution.

​

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

Solution : The following are given facts and their wff representation:

​

1. Marcus was a man.

Wff : man(Marcus)

Clause : man(Marcus)

​

2. Marcus was a Pompeian.

Wff : Pompeian(Marcus)

Clause : Pompeian(Marcus)

​

3. All Pompeians were Romans.

Wff: ∀x: Pompeian(x) → Roman(x)

Clause : ⌐ Pompeian(x1) ∨ Roman(x1)

​

4. Caesar was a ruler.

Wff: ruler(Caesar)

Clause : ruler(Caesar)

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

5. All romans were either loyal to Caesar or hated him.

Wff : ∀x: Roman(x) → loyalto(x, Caesar) ∨ hate(x, Caesar)

Clause : Roman(x2) ∨ loyalto(x2, Caesar) ∨ hate(x2, Caesar)

� 6. Everyone is loyal to someone.

Wff: ∀x: ∃y: loyalto (x, y)

Clause : loyalto (x3, y1)

​

7. People only try to assassinate rulers they are not loyal to.

Wff : ∀x: ∀y: person(x) ∧ ruler(y) ∧ tryassassinate(x, y) → ¬loyalto(x, y)

Clause : ¬ person(x4) ∨ ¬ ruler(y2) ∨ ¬ tryassassinate(x4, y2) ∨ ¬loyalto(x4, y2)

8. Marcus tried to assassinate Caesar.

Wff : tryassassinate(Marcus, Caesar)

Clause : tryassassinate(Marcus, Caesar)

​

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

Now we need to prove marcus hates caesar, so negate it convert to clause form.

9. assume that marcus hates caesar is wrong

​

Wff : ¬ hate ( marcus, caesar)

​

Clause : ¬ hate ( marcus, caesar)

​

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

The empty clause at end which indicates contradiction, so our assumption is wrong

So ¬ hate ( marcus, caesar) is wrong

So hate ( marcus, caesar)

is proved.

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

The following are given facts :

• John likes all kind of food.
• Apples are food
• Chicken is food.
• Anything any one eats and is not killed is food.
• Bill eats peanuts and is still alive.
• Sue eats everything that bill eats
• One is alive means not killed by some thing.

​

Prove by resolution that:

John likes peanuts.

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

The following are wff of the given facts

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

The following are clauses of the given facts

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

We need to prove john likes peanuts.

So we assume : ¬ likes ( john, peanuts )

The empty clause at end which indicates contradiction.

so our assumption is wrong

So ¬ likes (john, peanuts ) is wrong

So likes (john, peanuts )

is proved.

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

Consider the following knowledge base:

• Gita likes all kinds of food.
• Mango and chapati are food.
• Gita eats almond and is still alive.
• Anything eaten by anyone and is still alive is food.

Goal: Gita likes almond.

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

Solution: Convert the given sentences into FOPL as:

∀x: food(x) → likes(Gita,x)

food(Mango),food(chapati)

∀x∀y: eats(x,y) Ʌ ¬ killed(x → food(y)

eats(Gita, almonds) Ʌ alive(Gita)

∀x: ¬killed(x) → alive(x)

∀x: alive(x) →  ¬killed(x)

Goal: likes(Gita, almond)

Negated goal: ¬likes(Gita, almond)

Now, rewrite in Clause form:

¬food(x) V likes(Gita, x)

food(Mango),food(chapati)

¬eats(x, y) V killed(x) V food(y)

eats(Gita, almonds), alive(Gita)

killed(x) V alive(x)

¬alive(x) V ¬killed(x)

​

KVSM, Dept of CSE , SRKREC

Resolution example in predicate logic

The empty clause at end which indicates contradiction.

so our assumption is wrong

So ¬likes(Gita, almond)

is wrong

So likes(Gita, almond)

is proved.

KVSM, Dept of CSE , SRKREC

21

​

Thank you

​

KVS MURTHY

Assistant Professor

Department of CSE

SRKR Engineering College

9848290433

kvssr.murthy@srkrec.edu.in

kvssr.murthy@srkrec.edu.in