Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~p || (p /\ ~(p /\ q))) /\ (p || (p /\ ~(p /\ q))) /\ (q || (p /\ ~(p /\ q)))
⇒ logic.propositional.absorpor(~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.demorganand(~p || ~p || ~q) /\ p /\ (q || (p /\ ~(p /\ q)))
⇒ logic.propositional.idempor(~p || ~q) /\ p /\ (q || (p /\ ~(p /\ q)))
⇒ logic.propositional.demorganand(~p || ~q) /\ p /\ (q || (p /\ (~p || ~q)))
⇒ logic.propositional.andoveror(~p || ~q) /\ p /\ (q || (p /\ ~p) || (p /\ ~q))
⇒ logic.propositional.compland(~p || ~q) /\ p /\ (q || F || (p /\ ~q))
⇒ logic.propositional.falsezeroor(~p || ~q) /\ p /\ (q || (p /\ ~q))
⇒ logic.propositional.oroverand(~p || ~q) /\ p /\ (q || p) /\ (q || ~q)
⇒ logic.propositional.absorpand(~p || ~q) /\ p /\ (q || ~q)
⇒ logic.propositional.complor(~p || ~q) /\ p /\ T
⇒ logic.propositional.truezeroand(~p || ~q) /\ p
⇒ logic.propositional.andoveror(~p /\ p) || (~q /\ p)
⇒ logic.propositional.complandF || (~q /\ p)
⇒ logic.propositional.falsezeroor~q /\ p