Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.compland((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(~F /\ ~(p /\ ~q)))
⇒ logic.propositional.notfalse((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.notnot((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.compland((~(~F /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.notfalse((~(T /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~~~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.notnot((~(T /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~(~(q /\ ~q) /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.compland((~(T /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~(~F /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.notfalse((~(T /\ ~(p /\ ~q)) /\ q) || ~r) /\ ((~(T /\ ~(p /\ ~q)) /\ q) || ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.absorpor((~(T /\ ~(p /\ ~q)) /\ q) || ~r) /\ ~(T /\ ~(p /\ ~q))
⇒ logic.propositional.truezeroand((~~(p /\ ~q) /\ q) || ~r) /\ ~(T /\ ~(p /\ ~q))
⇒ logic.propositional.notnot((p /\ ~q /\ q) || ~r) /\ ~(T /\ ~(p /\ ~q))
⇒ logic.propositional.compland((p /\ F) || ~r) /\ ~(T /\ ~(p /\ ~q))
⇒ logic.propositional.falsezeroand(F || ~r) /\ ~(T /\ ~(p /\ ~q))
⇒ logic.propositional.falsezeroor~r /\ ~(T /\ ~(p /\ ~q))
⇒ logic.propositional.truezeroand~r /\ ~~(p /\ ~q)
⇒ logic.propositional.notnot~r /\ p /\ ~q