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