2

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?

Mitchell Faas
  • 1,588
  • 13
  • 26
  • 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
  • 1
    @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

1 Answers1

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.

Mauro ALLEGRANZA
  • 94,169
  • 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