Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
(q || ~r) /\ (p || q) /\ ~q /\ ~q /\ (p || q)
⇒ logic.propositional.idempand(q || ~r) /\ (p || q) /\ ~q /\ (p || q)
⇒ logic.propositional.andoveror(q || ~r) /\ (p || q) /\ ((~q /\ p) || (~q /\ q))
⇒ logic.propositional.compland(q || ~r) /\ (p || q) /\ ((~q /\ p) || F)
⇒ logic.propositional.falsezeroor(q || ~r) /\ (p || q) /\ ~q /\ p
⇒ logic.propositional.andoveror(((q || ~r) /\ p) || ((q || ~r) /\ q)) /\ ~q /\ p
⇒ logic.propositional.absorpand(((q || ~r) /\ p) || q) /\ ~q /\ p
⇒ logic.propositional.andoveror((q /\ p) || (~r /\ p) || q) /\ ~q /\ p
⇒ logic.propositional.genandoveror(q /\ p /\ ~q /\ p) || (~r /\ p /\ ~q /\ p) || (q /\ ~q /\ p)
⇒ logic.propositional.compland(q /\ p /\ ~q /\ p) || (~r /\ p /\ ~q /\ p) || (F /\ p)
⇒ logic.propositional.falsezeroand(q /\ p /\ ~q /\ p) || (~r /\ p /\ ~q /\ p) || F
⇒ logic.propositional.falsezeroor(q /\ p /\ ~q /\ p) || (~r /\ p /\ ~q /\ p)