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