Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

(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.complor

T /\ (~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.compland

F || (~(p /\ q) /\ p)

⇒ logic.propositional.demorganand

F || ((~p || ~q) /\ p)

⇒ logic.propositional.andoveror

F || (~p /\ p) || (~q /\ p)

⇒ logic.propositional.compland

F || F || (~q /\ p)

⇒ logic.propositional.falsezeroor

F || (~q /\ p)

⇒ logic.propositional.falsezeroor

~q /\ p