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?

  • $\begingroup$ No, they are different. It's an unfortunate naming scheme. I'll change quickly adapt it for clarity. $\endgroup$ – Mitchell Faas Feb 15 '18 at 14:51
  • $\begingroup$ 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$. $\endgroup$ – Mauro ALLEGRANZA Feb 15 '18 at 14:54
  • $\begingroup$ This does not mean that $H$ is a tautology : it is not. It means that 1), 2) and 3) (and 4)) imply $H$. $\endgroup$ – Mauro ALLEGRANZA Feb 15 '18 at 14:56
  • $\begingroup$ Where is the mistake ? As you can see in the answer below, the clauses are wrongly written. $\endgroup$ – Mauro ALLEGRANZA Feb 15 '18 at 15:03
  • 1
    $\begingroup$ @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. $\endgroup$ – 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$.


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.

  • $\begingroup$ 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? $\endgroup$ – Mitchell Faas Feb 15 '18 at 15:42
  • $\begingroup$ @MitchellFaas - In that case you have to remove 6) $\lnot H$ and add 6') $\lnot M_2$ (for me: $\lnot N$). $\endgroup$ – Mauro ALLEGRANZA Feb 15 '18 at 18:44
  • $\begingroup$ 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 :) $\endgroup$ – Mitchell Faas Feb 15 '18 at 19:05
  • $\begingroup$ @MitchellFaas - the proof is similar; from 9) $H$ with 5) we get $N$ that conclude with 6') $\lnot N$. $\endgroup$ – Mauro ALLEGRANZA Feb 15 '18 at 19:23
  • $\begingroup$ Resolution is developed for automatic theorem proving: it's an algorithm. Check all combinations. When used by humans, use insight. $\endgroup$ – Mauro ALLEGRANZA Feb 15 '18 at 19:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.