Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ T /\ q) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.truezeroand(~~(T /\ ~~((p || q) /\ ~q)) /\ T /\ q) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.truezeroand(~~(T /\ ~~((p || q) /\ ~q)) /\ q) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.notnot(T /\ ~~((p || q) /\ ~q) /\ q) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.truezeroand(~~((p || q) /\ ~q) /\ q) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.notnot((p || q) /\ ~q /\ q) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.compland((p || q) /\ F) || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.falsezeroandF || (T /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r)
⇒ logic.propositional.falsezeroorT /\ ~~(T /\ ~~((p || q) /\ ~q)) /\ ~r
⇒ logic.propositional.truezeroand~~(T /\ ~~((p || q) /\ ~q)) /\ ~r
⇒ logic.propositional.notnotT /\ ~~((p || q) /\ ~q) /\ ~r
⇒ logic.propositional.truezeroand~~((p || q) /\ ~q) /\ ~r
⇒ logic.propositional.notnot(p || q) /\ ~q /\ ~r
⇒ logic.propositional.andoveror((p /\ ~q) || (q /\ ~q)) /\ ~r
⇒ logic.propositional.compland((p /\ ~q) || F) /\ ~r
⇒ logic.propositional.falsezeroorp /\ ~q /\ ~r