Question

Perform resolution. What can you conclude about this set of clauses?

1. W v ~X v ~Y v Z

2. ~W v ~X v ~Y v Z

3. X v Y v Z

4. W v ~Z

5. ~W

'~' denotes negation and 'v' denotes union

Given these clauses in CNF, perform resolution

Answer 1

ANS:

1. W v ~X v ~Y v Z

2. ~W v ~X v ~Y v Z

3. X v Y v Z

4. W v ~Z

5. ~W

On Applying Resolution on 4 and 5:

we get:

~Z -(6)

On Applying Resolution on 3 and 6:

we get:

X v Y -(7)

On Applying Resolution on 1, 5 and 6:

we get:

~X v ~Y -(8)

On Applyinf resolution on 7 and 8,

we get:

(~X ^ Y) v (X ^ ~Y) -(9)

So : All the conclusions are as follows:

(~W), (~Z), (~X ^ Y) v (X ^ ~Y)

In simple terms we can say that

1. Negation W is TRUE

2. Negation Z is TRUE

3. Either of  (X is True and Y is False) or (X is False and Y is True) is TRUE