Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
q || ((r || ~(q -> r)) /\ (r || ~(q -> r) || F))
⇒ logic.propositional.defimplq || ((r || ~(q -> r)) /\ (r || ~(~q || r) || F))
⇒ logic.propositional.demorganorq || ((r || ~(q -> r)) /\ (r || (~~q /\ ~r) || F))
⇒ logic.propositional.falsezeroorq || ((r || ~(q -> r)) /\ (r || (~~q /\ ~r)))
⇒ logic.propositional.notnotq || ((r || ~(q -> r)) /\ (r || (q /\ ~r)))