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.
Best Answer
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!