Question

Consider the following clauses in a knowledge base:

1. A v ~B
2. ~W v B
3. ~A
4. W v B v M

Using this knowledge-base of clauses,

1. Show by a resolution-refutation proof that proposition M is true.
2. Show by resolution inference and the direct proof method that the proposition M is true.

Answer 1

The following clauses in knowledge base is given:

1. A v ~B
2. ~W v B
3. ~A
4. W v B v M

For Understanding: If A is true than ~A is false and if ~A is true then A is false.

Note: Consider Clause numbers separately in both the methods.

(1) Show by resolution-refutation proof that proposition M is true.

Consider the following clauses in a knowledge base:

Clause-1: A v ~B

Clause-2: ~W v B

Clause-3: ~A

Clause-4: W v B v M

In resolution-refutation proof, we use proof by contradiction metohd to achieve conclusion,

In proof by contradiction method, we assume opposite of the conclusion is true and then we show that the assumption would lead to contradiction.

Here, Conculsion is: M is true.

We assume opposite: i.e. M is false. ( ~M is true) We will add new clause, Clause-5: ~M

Step-1:

From Clause-1: A v ~B and Clause-3: ~A,

We can apply disjunctive syllogism and can derive new clause, Clause-6: ~B

Explanation: A v ~B is true iff at least one of them is true. but acoording to clause-3 A is false, so ~B must be true.

Step-2:

From Clause-2: ~W v B and Clause-6: ~B,

We can apply disjunctive syllogism and can derive new clause, Clause-7: ~W

Explanation: ~W v B is true iff at least one of them is true. but acoording to clause-6 B is false, so ~W must be true.

Step-3:

From Clause-4: W v B v M, Clause-5: ~M and Clause-6: ~B,

We can apply disjunctive syllogism and can derive new clause, Clause-8: W

Explanation: W v B v M is true iff at least one of them is true. but acoording to clause-5. M is false and according to clause-6, B is false, so W must be true.

Step-4:

As we can see that, Clause-7: ~W and Clause-8: W, contradict each other.

So, Our assumption that M is false is wrong.

Hence, M is True,

(2) Show by resolution inference and the direct proof method that the proposition M is true.

Consider the following clauses in a knowledge base:

Clause-1: A v ~B

Clause-2: ~W v B

Clause-3: ~A

Clause-4: W v B v M

Here, Conculsion is: M is true.

In resolution inference and the direct proof method, we will apply various rules of inference (like Modus Ponen, Disjunctive syllogism, Transitivity etc.) to derive new clauses and ultimately to derive conclusion.

Step-1:

From Clause-1: A v ~B and Clause-3: ~A,

We can apply disjunctive syllogism and can derive new clause, Clause-5: ~B

Explanation: A v ~B is true iff at least one of them is true. but acoording to clause-3 A is false, so ~B must be true.

Step-2:

From Clause-2: ~W v B and Clause-6: ~B,

We can apply disjunctive syllogism and can derive new clause, Clause-6: ~W

Explanation: ~W v B is true iff at least one of them is true. but acoording to clause-6 B is false, so ~W must be true.

Step-3:

From Clause-4: W v B v M, Clause-5: ~B and Clause-6: ~W,

We can apply disjunctive syllogism and can derive new clause, Clause-7: M.

Explanation: W v B v M is true iff at least one of them is true. but acoording to clause-5, B is false and according to clause-6, W is false, so M must be true.

Hence, we can derive conclusion: M is true, from the given clauses using resolution inference and direct proof method.