Exercise logic.propositional.cnf.unicode
Description
Proposition to CNF (unicode support)
Derivations
1.
¬((q → r) → ¬q)
⇒ logic.propositional.defimpl¬(¬(q → r) ∨ ¬q)
⇒ logic.propositional.demorganor¬¬(q → r) ∧ ¬¬q
⇒ logic.propositional.notnot(q → r) ∧ ¬¬q
⇒ logic.propositional.defimpl(¬q ∨ r) ∧ ¬¬q
⇒ logic.propositional.notnot(¬q ∨ r) ∧ q
2.
(¬q ∧ ¬(p → q)) → p
⇒ logic.propositional.defimpl¬(¬q ∧ ¬(p → q)) ∨ p
⇒ logic.propositional.demorganand¬¬q ∨ ¬¬(p → q) ∨ p
⇒ logic.propositional.notnotq ∨ ¬¬(p → q) ∨ p
⇒ logic.propositional.notnotq ∨ (p → q) ∨ p
⇒ logic.propositional.defimplq ∨ ¬p ∨ q ∨ p
3.
((q ∨ p) → (q → p)) → (r ∧ q ∧ p)
⇒ logic.propositional.defimpl¬((q ∨ p) → (q → p)) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.defimpl¬(¬(q ∨ p) ∨ (q → p)) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.demorganor(¬¬(q ∨ p) ∧ ¬(q → p)) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.notnot((q ∨ p) ∧ ¬(q → p)) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.defimpl((q ∨ p) ∧ ¬(¬q ∨ p)) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.demorganor((q ∨ p) ∧ ¬¬q ∧ ¬p) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.notnot((q ∨ p) ∧ q ∧ ¬p) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.absorpand(q ∧ ¬p) ∨ (r ∧ q ∧ p)
⇒ logic.propositional.genoroverand((q ∧ ¬p) ∨ r) ∧ ((q ∧ ¬p) ∨ q) ∧ ((q ∧ ¬p) ∨ p)
⇒ logic.propositional.absorpor((q ∧ ¬p) ∨ r) ∧ q ∧ ((q ∧ ¬p) ∨ p)
⇒ logic.propositional.oroverand(q ∨ r) ∧ (¬p ∨ r) ∧ q ∧ ((q ∧ ¬p) ∨ p)
⇒ logic.propositional.oroverand(q ∨ r) ∧ (¬p ∨ r) ∧ q ∧ (q ∨ p) ∧ (¬p ∨ p)
⇒ logic.propositional.absorpand(q ∨ r) ∧ (¬p ∨ r) ∧ q ∧ (¬p ∨ p)
⇒ logic.propositional.complor(q ∨ r) ∧ (¬p ∨ r) ∧ q ∧ T
⇒ logic.propositional.truezeroand(q ∨ r) ∧ (¬p ∨ r) ∧ q
4.
p ↔ (p ∧ q)
⇒ logic.propositional.defequiv(p ∧ p ∧ q) ∨ (¬p ∧ ¬(p ∧ q))
⇒ logic.propositional.idempand(p ∧ q) ∨ (¬p ∧ ¬(p ∧ q))
⇒ logic.propositional.oroverand((p ∧ q) ∨ ¬p) ∧ ((p ∧ q) ∨ ¬(p ∧ q))
⇒ logic.propositional.complor((p ∧ q) ∨ ¬p) ∧ T
⇒ logic.propositional.oroverand(p ∨ ¬p) ∧ (q ∨ ¬p) ∧ T
⇒ logic.propositional.complorT ∧ (q ∨ ¬p) ∧ T
⇒ logic.propositional.truezeroand(q ∨ ¬p) ∧ T
⇒ logic.propositional.truezeroandq ∨ ¬p
5.
(p ∧ q) ∨ (p ↔ r)
⇒ logic.propositional.defequiv(p ∧ q) ∨ (p ∧ r) ∨ (¬p ∧ ¬r)
⇒ logic.propositional.oroverand(p ∧ q) ∨ (((p ∧ r) ∨ ¬p) ∧ ((p ∧ r) ∨ ¬r))
⇒ logic.propositional.oroverand(p ∧ q) ∨ ((p ∨ ¬p) ∧ (r ∨ ¬p) ∧ ((p ∧ r) ∨ ¬r))
⇒ logic.propositional.complor(p ∧ q) ∨ (T ∧ (r ∨ ¬p) ∧ ((p ∧ r) ∨ ¬r))
⇒ logic.propositional.truezeroand(p ∧ q) ∨ ((r ∨ ¬p) ∧ ((p ∧ r) ∨ ¬r))
⇒ logic.propositional.oroverand(p ∧ q) ∨ ((r ∨ ¬p) ∧ (p ∨ ¬r) ∧ (r ∨ ¬r))
⇒ logic.propositional.complor(p ∧ q) ∨ ((r ∨ ¬p) ∧ (p ∨ ¬r) ∧ T)
⇒ logic.propositional.truezeroand(p ∧ q) ∨ ((r ∨ ¬p) ∧ (p ∨ ¬r))
⇒ logic.propositional.oroverand((p ∧ q) ∨ r ∨ ¬p) ∧ ((p ∧ q) ∨ p ∨ ¬r)
⇒ logic.propositional.absorpor((p ∧ q) ∨ r ∨ ¬p) ∧ (p ∨ ¬r)
⇒ logic.propositional.oroverand(p ∨ r ∨ ¬p) ∧ (q ∨ r ∨ ¬p) ∧ (p ∨ ¬r)