Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
~~(p || ~(~q /\ ~(p -> q)))
⇒ logic.propositional.notnotp || ~(~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