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
-
1$\begingroup$ Hint: construct truth-table for this and look if formulas are equal. $\endgroup$ – rus9384 Sep 6 '17 at 11:10
-
$\begingroup$ You're allowed to do whatever you want as long as it's mathematically valid. $\endgroup$ – Yuval Filmus Sep 6 '17 at 11:15
$\begingroup$
$\endgroup$
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.
-
$\begingroup$ Resolution rule can change formula. It is used for satisfiability, not for minimizing. $\endgroup$ – rus9384 Sep 6 '17 at 18:09
-
$\begingroup$ 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. $\endgroup$ – cody Sep 6 '17 at 19:24