# Simple propositional logic proof

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.

• How exactly is your 'resolution' rule defined? Oct 23 '20 at 16:19
• 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. Oct 23 '20 at 16:28
• 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? Oct 23 '20 at 16:30
• Also, what is going on with that X at the beginning? Oct 23 '20 at 16:33
• 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$ Oct 23 '20 at 16:35

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!