Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.truezeroand(~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.notnot(~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.truezeroand(~(~(~q /\ q) /\ ~(p /\ ~q /\ T)) /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.compland(~(~F /\ ~(p /\ ~q /\ T)) /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.notfalse(~(T /\ ~(p /\ ~q /\ T)) /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.truezeroand(~~(p /\ ~q /\ T) /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.notnot(p /\ ~q /\ T /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.truezeroand(p /\ ~q /\ q) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.compland(p /\ F) || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.falsezeroandF || (~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r)
⇒ logic.propositional.falsezeroor~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ T /\ ~r
⇒ logic.propositional.truezeroand~~~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ ~r
⇒ logic.propositional.notnot~(~(~q /\ q) /\ ~(p /\ ~q /\ T) /\ T) /\ ~r
⇒ logic.propositional.truezeroand~(~(~q /\ q) /\ ~(p /\ ~q /\ T)) /\ ~r
⇒ logic.propositional.compland~(~F /\ ~(p /\ ~q /\ T)) /\ ~r
⇒ logic.propositional.notfalse~(T /\ ~(p /\ ~q /\ T)) /\ ~r
⇒ logic.propositional.truezeroand~~(p /\ ~q /\ T) /\ ~r
⇒ logic.propositional.notnotp /\ ~q /\ T /\ ~r
⇒ logic.propositional.truezeroandp /\ ~q /\ ~r