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