Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
T /\ (~~(T /\ q) || ~r) /\ (~(~F /\ ~(p /\ ~(q /\ T))) || ~T)
⇒ logic.propositional.notfalseT /\ (~~(T /\ q) || ~r) /\ (~(T /\ ~(p /\ ~(q /\ T))) || ~T)
⇒ logic.propositional.nottrueT /\ (~~(T /\ q) || ~r) /\ (~(T /\ ~(p /\ ~(q /\ T))) || F)
⇒ logic.propositional.falsezeroorT /\ (~~(T /\ q) || ~r) /\ ~(T /\ ~(p /\ ~(q /\ T)))
⇒ logic.propositional.truezeroandT /\ (~~(T /\ q) || ~r) /\ ~~(p /\ ~(q /\ T))
⇒ logic.propositional.notnotT /\ (~~(T /\ q) || ~r) /\ p /\ ~(q /\ T)
⇒ logic.propositional.truezeroandT /\ (~~(T /\ q) || ~r) /\ p /\ ~q