Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
p || ~(~q /\ ~(p -> q))
⇒ logic.propositional.demorganandp || ~~q || ~~(p -> q)
⇒ logic.propositional.notnotp || q || ~~(p -> q)
⇒ logic.propositional.notnotp || q || (p -> q)
⇒ logic.propositional.defimplp || q || ~p || q