Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

Derivation

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.defequiv

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.oroverand

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

⇒ logic.propositional.complor

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.defequiv

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.genandoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroand

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

⇒ logic.propositional.absorpor

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

⇒ logic.propositional.falsezeroor

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