Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

Derivation

Final term is not finished

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.falsezeroor

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.defequiv

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

⇒ logic.propositional.demorganor

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.notnot

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

⇒ logic.propositional.absorpand

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

⇒ logic.propositional.demorganand

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

⇒ logic.propositional.andoveror

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

⇒ logic.propositional.compland

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

⇒ logic.propositional.falsezeroor

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