Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

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

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

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

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

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

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

p /\ ~(p /\ q)

p /\ (~p || ~q)

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

F || (p /\ ~q)

p /\ ~q