Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
T /\ (~(q -> r) || r || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.truezeroand(~(q -> r) || r || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.defimpl(~(~q || r) || r || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.demorganor((~~q /\ ~r) || r || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.notnot((q /\ ~r) || r || q) /\ (~(q -> r) || q || r)
⇒ logic.propositional.defimpl((q /\ ~r) || r || q) /\ (~(~q || r) || q || r)
⇒ logic.propositional.demorganor((q /\ ~r) || r || q) /\ ((~~q /\ ~r) || q || r)
⇒ logic.propositional.notnot((q /\ ~r) || r || q) /\ ((q /\ ~r) || q || r)
⇒ logic.propositional.absorpor((q /\ ~r) || r || q) /\ (q || r)
⇒ logic.propositional.genandoveror(q /\ ~r /\ (q || r)) || (r /\ (q || r)) || (q /\ (q || r))
⇒ logic.propositional.absorpand(q /\ ~r /\ (q || r)) || r || (q /\ (q || r))
⇒ logic.propositional.absorpand(q /\ ~r /\ (q || r)) || r || q
⇒ logic.propositional.andoveror(q /\ ~r /\ q) || (q /\ ~r /\ r) || r || q
⇒ logic.propositional.absorpor(q /\ ~r /\ q) || r || q