Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~p /\ ~p /\ ~~(p /\ T /\ q) /\ ~~(p /\ T /\ q)) || (T /\ ~(~p || (p /\ q))) || F
⇒ logic.propositional.falsezeroor(~p /\ ~p /\ ~~(p /\ T /\ q) /\ ~~(p /\ T /\ q)) || (T /\ ~(~p || (p /\ q)))
⇒ logic.propositional.idempand(~p /\ ~~(p /\ T /\ q) /\ ~~(p /\ T /\ q)) || (T /\ ~(~p || (p /\ q)))
⇒ logic.propositional.idempand(~p /\ ~~(p /\ T /\ q)) || (T /\ ~(~p || (p /\ q)))
⇒ logic.propositional.notnot(~p /\ p /\ T /\ q) || (T /\ ~(~p || (p /\ q)))
⇒ logic.propositional.compland(F /\ T /\ q) || (T /\ ~(~p || (p /\ q)))
⇒ logic.propositional.falsezeroandF || (T /\ ~(~p || (p /\ q)))
⇒ logic.propositional.falsezeroorT /\ ~(~p || (p /\ q))
⇒ logic.propositional.truezeroand~(~p || (p /\ q))
⇒ logic.propositional.oroverand~((~p || p) /\ (~p || q))
⇒ logic.propositional.complor~(T /\ (~p || q))
⇒ logic.propositional.truezeroand~(~p || q)
⇒ logic.propositional.demorganor~~p /\ ~q
⇒ logic.propositional.notnotp /\ ~q