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