0
$\begingroup$

I am a beginner of propositional logic. I am trying to prove the below. Only resolution, modus ponens and and-elimination methods are allowed.

Problem

$X \Rightarrow(A \land B) \lor (C \land D) \lor (E \land F) \lor (G \land H)$

$ X, \neg A, \neg C $

Prove $E \lor G$

Solution:

If I apply Modus Ponens, I get:

$(A \land B) \lor (C \land D) \lor (E \land F) \lor (G \land H)$

After this point, I can't apply and-elimination because the "and"s are in brackets.

Modus Ponens isn't relevant here.

So the only other option left is resolution. But I can't see how I could apply that.

I tried to convert this to CNF by distributing $\vee$ over $\wedge$ but that ends up being too long to be practical as below:

$ ((A\vee C) \wedge (A\vee D)\wedge (B\vee C) \wedge (B\vee D)) \vee ((E\vee G) \wedge (E\vee H)\wedge (F\vee G) \wedge (F\vee H))$

I am stuck here. As I am only allowed to use resolution, modus ponens and and-elimination methods, I am not sure how to carry on.

$\endgroup$
10
  • $\begingroup$ How exactly is your 'resolution' rule defined? $\endgroup$
    – Bram28
    Oct 23 '20 at 16:19
  • $\begingroup$ if $ \neg A$ and $A \vee C$ then $ \neg A$ resolves A and C is left as the resolvant. I hope I have managed to explain it. $\endgroup$
    – Miles-can
    Oct 23 '20 at 16:28
  • $\begingroup$ Hmmm, so yes, you can;t apply that to your statement as is. Putting it into CNF does seem to be the thing to do, even as that gets really long .. but at least then you can do and-elimination to get individual disjunctions on which you can then apply this resolution rule. Thing is .. do you have rules for putting the statement into CNF? $\endgroup$
    – Bram28
    Oct 23 '20 at 16:30
  • $\begingroup$ Also, what is going on with that X at the beginning? $\endgroup$
    – Bram28
    Oct 23 '20 at 16:33
  • $\begingroup$ I have eliminated the X at the beginning with Modus Ponens. The method I need to use for converting to CNF are eliminating $ \Rightarrow $ by converting into disjunction, moving $\neg$ inwards which doesn't apply here, and distributing $ \vee $ over $ \wedge $ $\endgroup$
    – Miles-can
    Oct 23 '20 at 16:35
0
$\begingroup$

You just need to expoand further into full CNF. That is, with the Distribution equivalence you can go from

$(A \land B) \lor (C \land D) \lor (E \land F) \lor (G \land H)$

to

$ ((A\vee C) \wedge (A\vee D)\wedge (B\vee C) \wedge (B\vee D)) \vee ((E\vee G) \wedge (E\vee H)\wedge (F\vee G) \wedge (F\vee H))$

but then you apply Distribution again to get

$(A \lor C \lor E \lor G) \land (A \lor C \lor E \lor H) \land ....$

(you'll get 16 terms, each with 4 literals)

Now you can pull those apart using and-Elimination.

In fact, that very term is $A \lor C \lor E \lor G$, and so with resolution twice using $\neg A$ and $\neg C$ you're there!

$\endgroup$

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.