Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.idempor

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.falsezeroor

~q /\ p /\ ~q /\ p

⇒ logic.propositional.idempand

~q /\ p