Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

Derivation

F ∨ (¬(q → p) ↔ (¬s ∨ (r ↔ s) ∨ ¬s))

⇒ logic.propositional.defimpl

F ∨ (¬(¬q ∨ p) ↔ (¬s ∨ (r ↔ s) ∨ ¬s))

⇒ logic.propositional.demorganor

F ∨ ((¬¬q ∧ ¬p) ↔ (¬s ∨ (r ↔ s) ∨ ¬s))

⇒ logic.propositional.falsezeroor

(¬¬q ∧ ¬p) ↔ (¬s ∨ (r ↔ s) ∨ ¬s)

⇒ logic.propositional.notnot

(q ∧ ¬p) ↔ (¬s ∨ (r ↔ s) ∨ ¬s)

⇒ logic.propositional.defequiv

(q ∧ ¬p) ↔ (¬s ∨ (r ∧ s) ∨ (¬r ∧ ¬s) ∨ ¬s)

⇒ logic.propositional.absorpor

(q ∧ ¬p) ↔ (¬s ∨ (r ∧ s) ∨ ¬s)

⇒ logic.propositional.oroverand

(q ∧ ¬p) ↔ (((¬s ∨ r) ∧ (¬s ∨ s)) ∨ ¬s)

⇒ logic.propositional.complor

(q ∧ ¬p) ↔ (((¬s ∨ r) ∧ T) ∨ ¬s)

⇒ logic.propositional.truezeroand

(q ∧ ¬p) ↔ (¬s ∨ r ∨ ¬s)

⇒ logic.propositional.defequiv

(q ∧ ¬p ∧ (¬s ∨ r ∨ ¬s)) ∨ (¬(q ∧ ¬p) ∧ ¬(¬s ∨ r ∨ ¬s))

⇒ logic.propositional.demorganand

(q ∧ ¬p ∧ (¬s ∨ r ∨ ¬s)) ∨ ((¬q ∨ ¬¬p) ∧ ¬(¬s ∨ r ∨ ¬s))

⇒ logic.propositional.genandoveror

(q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ ((¬q ∨ ¬¬p) ∧ ¬(¬s ∨ r ∨ ¬s))

⇒ logic.propositional.notnot

(q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ ((¬q ∨ p) ∧ ¬(¬s ∨ r ∨ ¬s))

⇒ logic.propositional.gendemorganor

(q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ ((¬q ∨ p) ∧ ¬¬s ∧ ¬r ∧ ¬¬s)

⇒ logic.propositional.notnot

(q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ ((¬q ∨ p) ∧ s ∧ ¬r ∧ ¬¬s)

⇒ logic.propositional.notnot

(q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ ((¬q ∨ p) ∧ s ∧ ¬r ∧ s)

⇒ logic.propositional.andoveror

(q ∧ ¬p ∧ ¬s) ∨ (q ∧ ¬p ∧ r) ∨ (q ∧ ¬p ∧ ¬s) ∨ (¬q ∧ s ∧ ¬r ∧ s) ∨ (p ∧ s ∧ ¬r ∧ s)