Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~~q /\ T /\ ~~~(q /\ q) /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.idempand(~~q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.idempand(~~q /\ T /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.truezeroand(~~q /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.notnot(q /\ ~~~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.notnot(q /\ ~(q /\ q)) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.idempand(q /\ ~q) || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.complandF || (T /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q))
⇒ logic.propositional.falsezeroorT /\ ~~(p /\ ~r) /\ T /\ ~~~(q /\ q)
⇒ logic.propositional.truezeroand~~(p /\ ~r) /\ T /\ ~~~(q /\ q)
⇒ logic.propositional.truezeroand~~(p /\ ~r) /\ ~~~(q /\ q)
⇒ logic.propositional.notnotp /\ ~r /\ ~~~(q /\ q)
⇒ logic.propositional.notnotp /\ ~r /\ ~(q /\ q)
⇒ logic.propositional.idempandp /\ ~r /\ ~q