Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(F /\ (r || ~~p || q)) || (q /\ (r || ~~p || q)) || (~~(T /\ p) /\ (r || ~~p || q))
⇒ logic.propositional.absorpand(F /\ (r || ~~p || q)) || q || (~~(T /\ p) /\ (r || ~~p || q))
⇒ logic.propositional.falsezeroandF || q || (~~(T /\ p) /\ (r || ~~p || q))
⇒ logic.propositional.falsezeroorq || (~~(T /\ p) /\ (r || ~~p || q))
⇒ logic.propositional.notnotq || (T /\ p /\ (r || ~~p || q))
⇒ logic.propositional.truezeroandq || (p /\ (r || ~~p || q))
⇒ logic.propositional.notnotq || (p /\ (r || p || q))
⇒ logic.propositional.genandoverorq || (p /\ r) || (p /\ p) || (p /\ q)
⇒ logic.propositional.idempandq || (p /\ r) || p || (p /\ q)
⇒ logic.propositional.absorporq || (p /\ r) || p
⇒ logic.propositional.absorporq || p