cancel out parts of a formula in CNF (conjunctive normal form)
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.