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