Question on using the Resolution Rule with an and statement after converting to CNF

Question

So I need to show p ⊢ q → (p ∧ q) using the resolution rule. I converted into CNF to get q ^ ¬p, however in the answer it simply says:

1 p

2 q

3 ¬p

4 {}1,3

I know what the resolution rule is but I don't understand how that gets you to this point.

Answer 1

You need to go through the following steps:

I) Negate the conclusion, and put all statements into CNF:

$$\neg (q \rightarrow (p \land q)) \Leftrightarrow$$

$$q \land \neg (p \land q) \Leftrightarrow$$

$$q \land (\neg p \lor \neg q)$$

premise $p$ is already in CNF

II) Create clauses:

1. $$\{ p \}$$

2. $$\{ q \}$$

3. $$\{ \neg p, \neg q \}$$

III). And now resolve:

4. $$\{ \neg q \} \quad (1.3)$$

5. $$\{ \} \quad (2,4)$$

... which is indeed different from what you indicated was given as the answer ... so I can see how you didn't understand the given answer ... it is incorrect!