Theory: sat

Theorems

⊢ ∀A B C. A ∧ B ⇒ C ⇔ A ⇒ B ⇒ C

⊢ ∀A. ¬A ∧ A ⇔ F

⊢ (¬A ⇒ F) ⇒ (A ⇒ F) ⇒ F

⊢ ∀A. A ⇒ ¬A ⇒ F

⊢ ∀b. ¬b ⇒ (b ⇔ F)

⊢ ∀b. b ⇒ (b ⇔ T)

⊢ ¬A ⇒ F ⇔ A

⊢ ∀t. ¬¬t ⇔ t

⊢ ¬(A ∨ B) ⇒ F ⇔ ¬A ⇒ ¬B ⇒ F

⊢ ¬(A ∨ B) ⇒ F ⇔ (A ⇒ F) ⇒ ¬B ⇒ F

⊢ ¬(¬A ∨ B) ⇒ F ⇔ A ⇒ ¬B ⇒ F

⊢ (p ⇔ if q then r else s) ⇔
  (p ∨ q ∨ ¬s) ∧ (p ∨ ¬r ∨ ¬q) ∧ (p ∨ ¬r ∨ ¬s) ∧ (¬q ∨ r ∨ ¬p) ∧
  (q ∨ s ∨ ¬p)

⊢ (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)

⊢ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)

⊢ (p ⇔ (q ⇔ r)) ⇔
  (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)

⊢ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)

⊢ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)

⊢ p ∧ q ⇒ p

⊢ p ∧ q ⇒ q

⊢ ¬(p ⇒ q) ⇒ p

⊢ ¬(p ⇒ q) ⇒ ¬q

⊢ ¬¬p ⇒ p

⊢ ¬(p ∨ q) ⇒ ¬p

⊢ ¬(p ∨ q) ⇒ ¬q