Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
((~(~(q /\ ~q) /\ ~(~q /\ p)) /\ ~(r /\ T)) || (~(~(q /\ ~q) /\ ~(~q /\ p)) /\ q)) /\ T
⇒ logic.propositional.truezeroand(~(~(q /\ ~q) /\ ~(~q /\ p)) /\ ~(r /\ T)) || (~(~(q /\ ~q) /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.compland(~(~F /\ ~(~q /\ p)) /\ ~(r /\ T)) || (~(~(q /\ ~q) /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.compland(~(~F /\ ~(~q /\ p)) /\ ~(r /\ T)) || (~(~F /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.notfalse(~(T /\ ~(~q /\ p)) /\ ~(r /\ T)) || (~(~F /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.notfalse(~(T /\ ~(~q /\ p)) /\ ~(r /\ T)) || (~(T /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.truezeroand(~~(~q /\ p) /\ ~(r /\ T)) || (~(T /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.notnot(~q /\ p /\ ~(r /\ T)) || (~(T /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.truezeroand(~q /\ p /\ ~r) || (~(T /\ ~(~q /\ p)) /\ q)
⇒ logic.propositional.truezeroand(~q /\ p /\ ~r) || (~~(~q /\ p) /\ q)
⇒ logic.propositional.notnot(~q /\ p /\ ~r) || (~q /\ p /\ q)