What mistake am I making within this logic resolution problem?

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?

• No, they are different. It's an unfortunate naming scheme. I'll change quickly adapt it for clarity. – Mitchell Faas Feb 15 '18 at 14:51
• The first part is right: $M \lor \lnot M$ holds and thus, from 1) and 2) we get: $O \lor Z$. Thus, from 3) we derive: $H$. – Mauro ALLEGRANZA Feb 15 '18 at 14:54
• This does not mean that $H$ is a tautology : it is not. It means that 1), 2) and 3) (and 4)) imply $H$. – Mauro ALLEGRANZA Feb 15 '18 at 14:56
• Where is the mistake ? As you can see in the answer below, the clauses are wrongly written. – Mauro ALLEGRANZA Feb 15 '18 at 15:03
• @MauroALLEGRANZA Conjunctive Normal Form. The V is for the Dutch variant, forgot to take it out :) Here a tautology means: a tautology within the model where all given clauses are necessarily true. Perhaps it's the wrong term, but I found it most resembled what I was trying to say. – Mitchell Faas Feb 15 '18 at 15:05

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.

• I'm supposed to do the same with $m$ ($M_2$) now, but I can't seem to resolve this one without also adding $H$ or $\neg M$ as clause. Are you allowed to do that, or do you just have to keep searching until you find a way? What are some good resolution finding strategies? – Mitchell Faas Feb 15 '18 at 15:42
• @MitchellFaas - In that case you have to remove 6) $\lnot H$ and add 6') $\lnot M_2$ (for me: $\lnot N$). – Mauro ALLEGRANZA Feb 15 '18 at 18:44
• Yeah, that's what I did. But with doing that, I still didn't manage to find the solution. Is there some trick to finding the right one? My idea was that I wanted to find a way to work away $\neg H \lor N$, but I couldn't do it. EDIT: And just now I found it.. Thanks :) – Mitchell Faas Feb 15 '18 at 19:05
• @MitchellFaas - the proof is similar; from 9) $H$ with 5) we get $N$ that conclude with 6') $\lnot N$. – Mauro ALLEGRANZA Feb 15 '18 at 19:23
• Resolution is developed for automatic theorem proving: it's an algorithm. Check all combinations. When used by humans, use insight. – Mauro ALLEGRANZA Feb 15 '18 at 19:24