Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
F || (((T /\ ~(r /\ T)) || (T /\ q /\ T)) /\ ~(~(q /\ ~q) /\ ~(p /\ ~q)))
⇒ logic.propositional.complandF || (((T /\ ~(r /\ T)) || (T /\ q /\ T)) /\ ~(~F /\ ~(p /\ ~q)))
⇒ logic.propositional.notfalseF || (((T /\ ~(r /\ T)) || (T /\ q /\ T)) /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroandF || ((~(r /\ T) || (T /\ q /\ T)) /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroandF || ((~r || (T /\ q /\ T)) /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroandF || ((~r || (q /\ T)) /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroandF || ((~r || q) /\ ~(T /\ ~(p /\ ~q)))
⇒ logic.propositional.truezeroandF || ((~r || q) /\ ~~(p /\ ~q))
⇒ logic.propositional.notnotF || ((~r || q) /\ p /\ ~q)
⇒ logic.propositional.andoverorF || (~r /\ p /\ ~q) || (q /\ p /\ ~q)