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