Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

~(T /\ ~(T /\ q /\ ~q) /\ ~(p /\ ~q)) /\ (q || (T /\ ~r))

⇒ logic.propositional.compland

~(T /\ ~(T /\ F) /\ ~(p /\ ~q)) /\ (q || (T /\ ~r))

⇒ logic.propositional.falsezeroand

~(T /\ ~F /\ ~(p /\ ~q)) /\ (q || (T /\ ~r))

⇒ logic.propositional.notfalse

~(T /\ T /\ ~(p /\ ~q)) /\ (q || (T /\ ~r))

⇒ logic.propositional.truezeroand

~(T /\ ~(p /\ ~q)) /\ (q || (T /\ ~r))

⇒ logic.propositional.demorganand

~(T /\ (~p || ~~q)) /\ (q || (T /\ ~r))

⇒ logic.propositional.notnot

~(T /\ (~p || q)) /\ (q || (T /\ ~r))