Exercise logic.propositional.cnf.unicode

Description
Proposition to CNF (unicode support)

Derivation

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

⇒ logic.propositional.truezeroand

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

⇒ logic.propositional.defequiv

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.idempand

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

⇒ logic.propositional.complor

(¬r ∨ ¬T) ∧ T

⇒ logic.propositional.nottrue

(¬r ∨ F) ∧ T

⇒ logic.propositional.falsezeroor

¬r ∧ T