Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.falsezeroor

p /\ p /\ ~q

⇒ logic.propositional.idempand

p /\ ~q