Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.defimpl

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.demorganand

~(~q || r) || ~~q || ~~r || ~(~q || r) || ~~q || ~~r

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.absorpor

~~q || ~~r || ~(~q || r) || ~~q || ~~r

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.absorpor

~~q || ~~r || ~~q || ~~r

⇒ logic.propositional.idempor

~~q || ~~r

⇒ logic.propositional.notnot

q || ~~r

⇒ logic.propositional.notnot

q || r