What mistake am I making within this logic resolution problem?

Question

I'm given the following statements:

$$M_1\implies O$$$$\neg M_1 \implies Z$$$$(O\lor Z)\implies H$$$$H\implies M_2$$

Then the question is, can you prove whether H is true? Followed up by, now answer the same question via logical resolution.

My solution:

Consider case $M_1$: $$ \nonumber M_1\implies O \implies H $$ Case $\neg M_1$: $$ \neg M_1 \implies Z\implies H. $$ So that $H$ is a tautology.

With resolution:

First, let us rewrite to CNF: \begin{align*} &(\neg O \lor M) \land (\neg Z \lor \neg M_1) \land (\neg H \lor M_1 \lor Z) \land (\neg M_2\lor H) \end{align*} Then for $H$, we simply add the clause $\neg H$ and see if this is satisfiable: \begin{align*} &(\neg O \lor M_1) \land (\neg Z \lor \neg M_1) \land (\neg H \lor M_1 \lor Z) \land (\neg M_2 \lor H)\land \neg H\\ \implies&(\neg O \lor \neg Z) \land (\neg H \lor M_1 \lor Z) \land \neg M_2\\ \implies&(\neg O \lor \neg H \lor M_1) \land \neg M_2\\ \end{align*} This is satisfiable, so $H$ is not a tautology.

But this is of course a contradiction so hence my question: What am I doing wrong?

Answer 1

The clauses must be:

1) $\lnot M \lor O$

2) $M \lor Z$

For: >$\lnot (O \lor Z) \lor H$, that is: $(\lnot O \land \lnot Z) \lor H$ that is: $(\lnot O \lor H) \land (\lnot Z \lor H)$. Thus:

3) $\lnot O \lor H$

4) $\lnot Z \lor H$

5) $\lnot H \lor N$.

---

In order to apply Resolution, you have to add to the set of premises the negation of the conclusion, i.e.

6) $\lnot H$.

Resolution:

7) $O \lor Z$ --- from 1) and 2)

8) $Z \lor H$ --- from 7) and 3)

9) $H$ --- from 8) and 4)

$\square$ (the empty clause) --- from 9) and 6).

---

As you can see, the last premise is inessential for the proof.