Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

~~~(~~(q -> r) /\ ~q /\ ~r)

⇒ logic.propositional.notnot

~~~((q -> r) /\ ~q /\ ~r)

⇒ logic.propositional.defimpl

~~~((~q || r) /\ ~q /\ ~r)

⇒ logic.propositional.absorpand

~~~(~q /\ ~r)