Logic Flashcards
commutativity
φ ∧ ψ ≡ ψ ∧ φ
φ ∨ ψ ≡ ψ ∨ φ
idempotence
φ ∧ φ ≡ φ
φ ∨ φ ≡ φ
associativity
(φ ∧ ψ) ∧ χ ≡ φ ∧ (ψ ∧ χ)
(φ ∨ ψ) ∨ χ ≡ φ ∨ (ψ ∨ χ)
De Morgan
¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
involution
¬¬φ ≡ φ
φ → ψ ≡ ¬φ ∨ ψ
distributivity
(φ ∧ ψ) ∨ χ ≡ (φ ∨ χ) ∧ (ψ ∨ χ)
sheffer stroke
φ | ψ ≡ ¬(φ ∧ ψ)
φ | φ ≡ ¬φ
φ ∨ ψ ≡ (φ | φ) | (ψ | ψ)
φ ∧ ψ
¬¬(φ ∧ ψ)
CNF1:
IMPL-FREE: φ → ψ ≡ ¬φ ∨ ψ
CNF2:
NNF: ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
¬¬φ ≡ φ
CNF3:
DISTR: (φ ∧ ψ) ∨ χ ≡ (φ ∨ χ) ∧ (ψ ∨ χ)
χ ∨ (φ ∧ ψ) ≡ (χ ∨ φ) ∧ (χ ∨ ψ)
CNF from truth table
look at false formulas and negate the literals (…v…) ^ (…v…)
DNF from truth table
look at true formulas and write down literals (… ^ …) v (…^…)
DPLL
assume a literal is true or false, look for pure literals and unit clauses first then repeat till satisfiable or not satisfiable