1
$\begingroup$

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

enter image description here

| cite | improve this question | |
$\endgroup$
  • 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
1
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\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

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.