Exercise logic.propositional.cnf.unicode

Description
Proposition to CNF (unicode support)

Derivation

Final term is not finished

F ∨ ((¬((r ↔ r) ∧ T) ∨ ¬r) ∧ T)

⇒ logic.propositional.truezeroand

F ∨ ((¬(r ↔ r) ∨ ¬r) ∧ T)

⇒ logic.propositional.defequiv

F ∨ ((¬((r ∧ r) ∨ (¬r ∧ ¬r)) ∨ ¬r) ∧ T)

⇒ logic.propositional.idempand

F ∨ ((¬(r ∨ (¬r ∧ ¬r)) ∨ ¬r) ∧ T)

⇒ logic.propositional.idempand

F ∨ ((¬(r ∨ ¬r) ∨ ¬r) ∧ T)

⇒ logic.propositional.complor

F ∨ ((¬T ∨ ¬r) ∧ T)

⇒ logic.propositional.nottrue

F ∨ ((F ∨ ¬r) ∧ T)

⇒ logic.propositional.falsezeroor

F ∨ (¬r ∧ T)