Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
T /\ ((q /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T))) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T))))
⇒ logic.propositional.truezeroand(q /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T))) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.notnot(q /\ ~~((p /\ ~q) || (q /\ ~q /\ T))) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.notnot(q /\ ((p /\ ~q) || (q /\ ~q /\ T))) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.compland(q /\ ((p /\ ~q) || (F /\ T))) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.falsezeroand(q /\ ((p /\ ~q) || F)) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.falsezeroor(q /\ p /\ ~q) || (~r /\ ~~~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.notnot(q /\ p /\ ~q) || (~r /\ ~~((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.notnot(q /\ p /\ ~q) || (~r /\ ((p /\ ~q) || (q /\ ~q /\ T)))
⇒ logic.propositional.compland(q /\ p /\ ~q) || (~r /\ ((p /\ ~q) || (F /\ T)))
⇒ logic.propositional.falsezeroand(q /\ p /\ ~q) || (~r /\ ((p /\ ~q) || F))
⇒ logic.propositional.falsezeroor(q /\ p /\ ~q) || (~r /\ p /\ ~q)