2

Consider the following sentence: $$[(F \implies P)\vee(D \implies P)] \implies [(F \wedge D) \implies P]$$

I am not too familiar with how to prove by resolution, from what I found online, I need to negate the conclusion and convert it to CNF, and I came up with the following: $$(\neg F \vee \neg D \vee P) \wedge (F \wedge D \wedge \neg P) $$ above is what I obtained after applying negation to the whole sentence, and I am assuming it would yield a empty set since one of them has to be false, but this is the right way of doing it?

Bango
  • 21
  • oops sorry, I fixed the error. – Bango Apr 10 '16 at 19:52
  • 1
    Exactly; after having applied the "transformation", if you reach teh empty set (or empty clause) this means that the formula is unsatisfiable. But, being it the negation of the original formula, this means that the original formula is a tautology (because $\varphi$ is taut iff $\lnot \varphi$ is unsat). – Mauro ALLEGRANZA Apr 10 '16 at 19:55

1 Answers1

1

This is right. You can further transform the second formula to a set of clauses:

$$\{ \{\neg F, \neg D, P \}, \{ F\}, \{ D\}, \{ \neg P\} \}.$$

Theses clauses can be used for resoultion (two at a time):

$$\{\underline{\neg F}, \neg D, P \}\quad\{ F\}$$ $$\{\underline{\neg D}, P \}\quad\{ D\}$$ $$\{\underline{P}\}\quad\{ \neg P\}$$ $$\square$$

Since you can derive the empty clause, the original (not negated) formula is a tautology.

Sven Hohenstein
  • 159