Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
(r || ~(q -> r) || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.defimpl(r || ~(~q || r) || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.demorganor(r || (~~q /\ ~r) || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.notnot(r || (q /\ ~r) || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.absorpor(r || q) /\ (~(q -> r) || q || r)