Exercise

Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

Final term is not finished

((T /\ ~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

((~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

((~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.compland

((~(~F /\ ~~(~(p /\ ~q) /\ T)) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.notfalse

((~(T /\ ~~(~(p /\ ~q) /\ T)) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

((~~~(~(p /\ ~q) /\ T) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.notnot

((~(~(p /\ ~q) /\ T) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

((~~(p /\ ~q) /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.notnot

((p /\ ~q /\ q) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.compland

((p /\ F) || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.falsezeroand

(F || (~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T)) /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.falsezeroor

~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ T /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ ~r /\ T /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

~(T /\ ~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T)) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.compland

~(~F /\ ~~(~(p /\ ~q) /\ T)) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.notfalse

~(T /\ ~~(~(p /\ ~q) /\ T)) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

~~~(~(p /\ ~q) /\ T) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.notnot

~(~(p /\ ~q) /\ T) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.truezeroand

~~(p /\ ~q) /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))

⇒ logic.propositional.notnot

p /\ ~q /\ ~r /\ ~(~(q /\ ~q) /\ ~~(~(p /\ ~q) /\ T))