Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.truezeroand

~((q || p) /\ ~q /\ (q || ~r)) -> F

⇒ logic.propositional.andoveror

~(((q /\ ~q) || (p /\ ~q)) /\ (q || ~r)) -> F

⇒ logic.propositional.compland

~((F || (p /\ ~q)) /\ (q || ~r)) -> F

⇒ logic.propositional.falsezeroor

~(p /\ ~q /\ (q || ~r)) -> F

⇒ logic.propositional.gendemorganand

(~p || ~~q || ~(q || ~r)) -> F

⇒ logic.propositional.notnot

(~p || q || ~(q || ~r)) -> F

⇒ logic.propositional.demorganor

(~p || q || (~q /\ ~~r)) -> F

⇒ logic.propositional.notnot

(~p || q || (~q /\ r)) -> F

⇒ logic.propositional.oroverand

(~p || ((q || ~q) /\ (q || r))) -> F

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

(~p || q || r) -> F

⇒ logic.propositional.defimpl

~(~p || q || r) || F

⇒ logic.propositional.falsezeroor

~(~p || q || r)

⇒ logic.propositional.gendemorganor

~~p /\ ~q /\ ~r

⇒ logic.propositional.notnot

p /\ ~q /\ ~r