Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~(p /\ T) || (p /\ ~(p /\ ~~q))) /\ ((p /\ q) || (p /\ ~(p /\ ~~q))) /\ ((p /\ q /\ T) || (p /\ ~(p /\ ~~q)))
⇒ logic.propositional.notnot(~(p /\ T) || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ ~~q))) /\ ((p /\ q /\ T) || (p /\ ~(p /\ ~~q)))
⇒ logic.propositional.notnot(~(p /\ T) || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ q))) /\ ((p /\ q /\ T) || (p /\ ~(p /\ ~~q)))
⇒ logic.propositional.notnot(~(p /\ T) || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ q))) /\ ((p /\ q /\ T) || (p /\ ~(p /\ q)))
⇒ logic.propositional.truezeroand(~p || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ q))) /\ ((p /\ q /\ T) || (p /\ ~(p /\ q)))
⇒ logic.propositional.truezeroand(~p || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ q)))
⇒ logic.propositional.idempand(~p || (p /\ ~(p /\ q))) /\ ((p /\ q) || (p /\ ~(p /\ q)))
⇒ logic.propositional.oroverand(~p || p) /\ (~p || ~(p /\ q)) /\ ((p /\ q) || (p /\ ~(p /\ q)))
⇒ logic.propositional.complorT /\ (~p || ~(p /\ q)) /\ ((p /\ q) || (p /\ ~(p /\ q)))
⇒ logic.propositional.truezeroand(~p || ~(p /\ q)) /\ ((p /\ q) || (p /\ ~(p /\ q)))
⇒ logic.propositional.oroverand(~p || ~(p /\ q)) /\ ((p /\ q) || p) /\ ((p /\ q) || ~(p /\ q))
⇒ logic.propositional.absorpor(~p || ~(p /\ q)) /\ p /\ ((p /\ q) || ~(p /\ q))
⇒ logic.propositional.complor(~p || ~(p /\ q)) /\ p /\ T
⇒ logic.propositional.truezeroand(~p || ~(p /\ q)) /\ p
⇒ logic.propositional.andoveror(~p /\ p) || (~(p /\ q) /\ p)
⇒ logic.propositional.complandF || (~(p /\ q) /\ p)
⇒ logic.propositional.demorganandF || ((~p || ~q) /\ p)
⇒ logic.propositional.andoverorF || (~p /\ p) || (~q /\ p)
⇒ logic.propositional.complandF || F || (~q /\ p)
⇒ logic.propositional.falsezeroorF || (~q /\ p)
⇒ logic.propositional.falsezeroor~q /\ p