# cancel out parts of a formula in CNF (conjunctive normal form)

In this image there is a given formula in DNF and CNF. When I check it on Wolfram Alpha I see that it cancel out (E or D) because of (not A or A) which is colored in red. My question is if it is allowed to cancel out (not A or D) because of (not E or E) which is colored in green instead. THX • Hint: construct truth-table for this and look if formulas are equal. – rus9384 Sep 6 '17 at 11:10
• You're allowed to do whatever you want as long as it's mathematically valid. – Yuval Filmus Sep 6 '17 at 11:15

It's probably useful to note that the resolution rule can be used to figure out exactly which literals (things like $\neg A\vee D$) may be deduced from the others.
In this case, the resolution rule applied to the clauses $\neg A\vee \neg E$ and $E\vee D$ results in the clause $\neg A\vee D$, which shows that that clause is redundant.
• The resolution rule is actually used for solving, or unsatisfiablility. In the above case, resolving $\neg A\vee\neg E$ with $E\vee D$ results in $\neg A\vee D$, proving that that clause is redundant. – cody Sep 6 '17 at 19:24