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