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