Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
T /\ ~q /\ ~(~q /\ ~~r /\ T) /\ (~~p || q) /\ T /\ T
⇒ logic.propositional.idempandT /\ ~q /\ ~(~q /\ ~~r /\ T) /\ (~~p || q) /\ T
⇒ logic.propositional.truezeroand~q /\ ~(~q /\ ~~r /\ T) /\ (~~p || q) /\ T
⇒ logic.propositional.truezeroand~q /\ ~(~q /\ ~~r /\ T) /\ (~~p || q)
⇒ logic.propositional.notnot~q /\ ~(~q /\ ~~r /\ T) /\ (p || q)
⇒ logic.propositional.truezeroand~q /\ ~(~q /\ ~~r) /\ (p || q)
⇒ logic.propositional.notnot~q /\ ~(~q /\ r) /\ (p || q)
⇒ logic.propositional.demorganand~q /\ (~~q || ~r) /\ (p || q)
⇒ logic.propositional.notnot~q /\ (q || ~r) /\ (p || q)
⇒ logic.propositional.andoveror~q /\ (((q || ~r) /\ p) || ((q || ~r) /\ q))
⇒ logic.propositional.absorpand~q /\ (((q || ~r) /\ p) || q)
⇒ logic.propositional.andoveror(~q /\ (q || ~r) /\ p) || (~q /\ q)
⇒ logic.propositional.andoveror(~q /\ ((q /\ p) || (~r /\ p))) || (~q /\ q)
⇒ logic.propositional.andoveror(~q /\ q /\ p) || (~q /\ ~r /\ p) || (~q /\ q)
⇒ logic.propositional.compland(F /\ p) || (~q /\ ~r /\ p) || (~q /\ q)
⇒ logic.propositional.compland(F /\ p) || (~q /\ ~r /\ p) || F
⇒ logic.propositional.falsezeroandF || (~q /\ ~r /\ p) || F
⇒ logic.propositional.falsezeroor(~q /\ ~r /\ p) || F
⇒ logic.propositional.falsezeroor~q /\ ~r /\ p