Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
![](http://ideas.cs.uu.nl/images/external.png)
(p || q) /\ ~(F || ~(r <-> p))
⇒ logic.propositional.defequiv(p || q) /\ ~(F || ~((r /\ p) || (~r /\ ~p)))
⇒ logic.propositional.demorganor(p || q) /\ ~(F || (~(r /\ p) /\ ~(~r /\ ~p)))
⇒ logic.propositional.demorganand(p || q) /\ ~(F || (~(r /\ p) /\ (~~r || ~~p)))
⇒ logic.propositional.falsezeroor(p || q) /\ ~(~(r /\ p) /\ (~~r || ~~p))
⇒ logic.propositional.notnot(p || q) /\ ~(~(r /\ p) /\ (r || ~~p))
⇒ logic.propositional.notnot(p || q) /\ ~(~(r /\ p) /\ (r || p))
⇒ logic.propositional.demorganand(p || q) /\ ~((~r || ~p) /\ (r || p))
⇒ logic.propositional.andoveror(p || q) /\ ~(((~r || ~p) /\ r) || ((~r || ~p) /\ p))
⇒ logic.propositional.andoveror(p || q) /\ ~((~r /\ r) || (~p /\ r) || ((~r || ~p) /\ p))
⇒ logic.propositional.andoveror(p || q) /\ ~((~r /\ r) || (~p /\ r) || (~r /\ p) || (~p /\ p))
⇒ logic.propositional.compland(p || q) /\ ~(F || (~p /\ r) || (~r /\ p) || (~p /\ p))
⇒ logic.propositional.compland(p || q) /\ ~(F || (~p /\ r) || (~r /\ p) || F)
⇒ logic.propositional.falsezeroor(p || q) /\ ~((~p /\ r) || (~r /\ p) || F)
⇒ logic.propositional.falsezeroor(p || q) /\ ~((~p /\ r) || (~r /\ p))