Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.defimpl

~~q || q || ~~p

⇒ logic.propositional.notnot

q || q || ~~p

⇒ logic.propositional.idempor

q || ~~p

⇒ logic.propositional.notnot

q || p