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