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