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