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