Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.notfalse

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.notnot

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