Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.nottrue

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

⇒ logic.propositional.falsezeroor

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