Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
![](http://ideas.cs.uu.nl/images/external.png)
(F || ~p || (~~p /\ ~(p /\ q))) /\ ((p /\ q) || (~~p /\ ~(p /\ q)))
⇒ logic.propositional.falsezeroor(~p || (~~p /\ ~(p /\ q))) /\ ((p /\ q) || (~~p /\ ~(p /\ q)))
⇒ logic.propositional.notnot(~p || (p /\ ~(p /\ q))) /\ ((p /\ q) || (~~p /\ ~(p /\ q)))
⇒ logic.propositional.notnot(~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