Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.idempor

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.falsezeroor

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