Exercise logic.propositional.dnf.unicode
Description
Proposition to DNF (unicode support)
Derivations
1.
¬(q → r) ∨ q ∨ r
⇒ logic.propositional.defimpl¬(¬q ∨ r) ∨ q ∨ r
⇒ logic.propositional.demorganor(¬¬q ∧ ¬r) ∨ q ∨ r
⇒ logic.propositional.notnot(q ∧ ¬r) ∨ q ∨ r
⇒ logic.propositional.absorporq ∨ r
2.
(¬q ∧ ¬(p → q)) → p
⇒ logic.propositional.defimpl¬(¬q ∧ ¬(p → q)) ∨ p
⇒ logic.propositional.demorganand¬¬q ∨ ¬¬(p → q) ∨ p
⇒ logic.propositional.notnotq ∨ ¬¬(p → q) ∨ p
⇒ logic.propositional.notnotq ∨ (p → q) ∨ p
⇒ logic.propositional.defimplq ∨ ¬p ∨ q ∨ p
3.
(q ∨ ¬r) ∧ (q ∨ p) ∧ ¬q
⇒ logic.propositional.andoveror(q ∨ ¬r) ∧ ((q ∧ ¬q) ∨ (p ∧ ¬q))
⇒ logic.propositional.compland(q ∨ ¬r) ∧ (F ∨ (p ∧ ¬q))
⇒ logic.propositional.falsezeroor(q ∨ ¬r) ∧ p ∧ ¬q
⇒ logic.propositional.andoveror(q ∧ p ∧ ¬q) ∨ (¬r ∧ p ∧ ¬q)
4.
¬p ↔ (p ∧ q)
⇒ logic.propositional.defequiv(¬p ∧ p ∧ q) ∨ (¬¬p ∧ ¬(p ∧ q))
⇒ logic.propositional.compland(F ∧ q) ∨ (¬¬p ∧ ¬(p ∧ q))
⇒ logic.propositional.falsezeroandF ∨ (¬¬p ∧ ¬(p ∧ q))
⇒ logic.propositional.falsezeroor¬¬p ∧ ¬(p ∧ q)
⇒ logic.propositional.notnotp ∧ ¬(p ∧ q)
⇒ logic.propositional.demorganandp ∧ (¬p ∨ ¬q)
⇒ logic.propositional.andoveror(p ∧ ¬p) ∨ (p ∧ ¬q)
⇒ logic.propositional.complandF ∨ (p ∧ ¬q)
⇒ logic.propositional.falsezeroorp ∧ ¬q
5.
(p ∨ q) ∧ (r ↔ p)
⇒ logic.propositional.defequiv(p ∨ q) ∧ ((r ∧ p) ∨ (¬r ∧ ¬p))
⇒ logic.propositional.andoveror((p ∨ q) ∧ r ∧ p) ∨ ((p ∨ q) ∧ ¬r ∧ ¬p)
⇒ logic.propositional.andoveror(p ∧ r ∧ p) ∨ (q ∧ r ∧ p) ∨ ((p ∨ q) ∧ ¬r ∧ ¬p)
⇒ logic.propositional.andoveror(p ∧ r ∧ p) ∨ (q ∧ r ∧ p) ∨ (p ∧ ¬r ∧ ¬p) ∨ (q ∧ ¬r ∧ ¬p)