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