Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished(((T /\ ~T /\ r) || (T /\ ~T /\ r)) /\ T /\ T) || ~~~(~(q /\ T) /\ ~~~p /\ ~~~F)
⇒ logic.propositional.compland(((F /\ r) || (T /\ ~T /\ r)) /\ T /\ T) || ~~~(~(q /\ T) /\ ~~~p /\ ~~~F)
⇒ logic.propositional.compland(((F /\ r) || (F /\ r)) /\ T /\ T) || ~~~(~(q /\ T) /\ ~~~p /\ ~~~F)
⇒ logic.propositional.falsezeroand((F || (F /\ r)) /\ T /\ T) || ~~~(~(q /\ T) /\ ~~~p /\ ~~~F)
⇒ logic.propositional.absorpor(F /\ T /\ T) || ~~~(~(q /\ T) /\ ~~~p /\ ~~~F)