Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivations
1.
~(q -> r) || q || r
⇒ logic.propositional.defimpl~(~q || r) || q || r
⇒ logic.propositional.demorganor(~~q /\ ~r) || q || r
⇒ logic.propositional.notnot(q /\ ~r) || q || r
⇒ logic.propositional.absorporq || r
2.
(~q /\ ~(p -> q)) -> p
⇒ logic.propositional.defimpl~(~q /\ ~(p -> q)) || p
⇒ logic.propositional.demorganand~~q || ~~(p -> q) || p
⇒ logic.propositional.notnotq || ~~(p -> q) || p
⇒ logic.propositional.notnotq || (p -> q) || p
⇒ logic.propositional.defimplq || ~p || q || p
3.
(q || ~r) /\ (q || p) /\ ~q
⇒ logic.propositional.andoveror(q || ~r) /\ ((q /\ ~q) || (p /\ ~q))
⇒ logic.propositional.compland(q || ~r) /\ (F || (p /\ ~q))
⇒ logic.propositional.falsezeroor(q || ~r) /\ p /\ ~q
⇒ logic.propositional.andoveror(q /\ p /\ ~q) || (~r /\ p /\ ~q)
4.
~p <-> (p /\ q)
⇒ logic.propositional.defequiv(~p /\ p /\ q) || (~~p /\ ~(p /\ q))
⇒ logic.propositional.compland(F /\ q) || (~~p /\ ~(p /\ q))
⇒ logic.propositional.falsezeroandF || (~~p /\ ~(p /\ q))
⇒ logic.propositional.falsezeroor~~p /\ ~(p /\ q)
⇒ logic.propositional.notnotp /\ ~(p /\ q)
⇒ logic.propositional.demorganandp /\ (~p || ~q)
⇒ logic.propositional.andoveror(p /\ ~p) || (p /\ ~q)
⇒ logic.propositional.complandF || (p /\ ~q)
⇒ logic.propositional.falsezeroorp /\ ~q
5.
(p || q) /\ (r <-> p)
⇒ logic.propositional.defequiv(p || q) /\ ((r /\ p) || (~r /\ ~p))
⇒ logic.propositional.andoveror((p || q) /\ r /\ p) || ((p || q) /\ ~r /\ ~p)
⇒ logic.propositional.andoveror(p /\ r /\ p) || (q /\ r /\ p) || ((p || q) /\ ~r /\ ~p)
⇒ logic.propositional.andoveror(p /\ r /\ p) || (q /\ r /\ p) || (p /\ ~r /\ ~p) || (q /\ ~r /\ ~p)