• Propositional Logic 101: Syntax, Semantics, and Truth
• Truth Tables: Building and Using Them Effectively
• Normal Forms: CNF, DNF, and Why They Matter
• Inference Rules: Modus Ponens to Resolution
• Proof Systems: Natural Deduction, Tableaux, and SAT
• Satisfiability (SAT): From NP-Completeness to Practical Solvers
• Common Pitfalls: Ambiguity, Implication, and Scope of Negation
• Exercises: Build Intuition with Targeted Problems

Propositional logic studies statements (propositions) that are either true or false and how to combine them with logical connectives.

• Syntax: propositions (P, Q, R), connectives (¬, ∧, ∨, →, ↔), parentheses.
• Semantics: a valuation assigns True/False to each atomic proposition; connectives are evaluated by truth tables.
• Well-formed formulas (WFFs): built inductively from atoms with connectives.

Example
Atoms: P = "It rains", Q = "The ground is wet".
Formula: P → Q  (If it rains, the ground is wet)
Truth table row where P = T, Q = F makes P → Q false.

Truth tables exhaustively evaluate a formula across all assignments.

1. List all atomic propositions and enumerate 2ⁿ rows.
2. Evaluate subformulas column by column.
3. Classify: tautology (always true), contradiction (always false), contingent (mixed).

P  Q | P → Q | (P → Q) ∧ P
T  T |   T   |     T
T  F |   F   |     F
F  T |   T   |     F
F  F |   T   |     F

Bringing formulas to canonical shapes aids reasoning and automation.

• DNF: disjunction of conjunctions (OR of ANDs).
• CNF: conjunction of disjunctions (AND of ORs). Key for SAT solvers.
• Equivalences: eliminate ↔, →; push ¬ inward; use distributivity.

To CNF sketch
1) A → B ≡ ¬A ∨ B
2) ¬(A ∧ B) ≡ ¬A ∨ ¬B;  ¬(A ∨ B) ≡ ¬A ∧ ¬B
3) Distribute: (A ∨ (B ∧ C)) ≡ (A ∨ B) ∧ (A ∨ C)

Rules allow deriving new truths from known premises.

• Modus Ponens: from P and P → Q infer Q.
• Modus Tollens: from ¬Q and P → Q infer ¬P.
• Hypothetical Syllogism: (P → Q), (Q → R) ⟹ (P → R).
• Resolution (CNF): from (A ∨ C) and (¬A ∨ D) infer (C ∨ D).

Resolution example
(¬P ∨ R), (P ∨ Q) ⟹ (R ∨ Q)

Different proof styles serve different goals—human readability vs automation.

• Natural Deduction: introduction/elimination rules for each connective.
• Semantic Tableaux: refutation by systematically exploring branches.
• Resolution + SAT: algorithmic search over CNF with heuristics.

ND sketch for (P ∧ (P → Q)) → Q
1) Assume P ∧ (P → Q)
2) From 1, get P and (P → Q)
3) From 2 by MP, infer Q
4) Discharge assumption: conclude (P ∧ (P → Q)) → Q

SAT asks: is there an assignment making a CNF formula true?

• Cook–Levin: SAT is NP-complete.
• DPLL/CDCL: modern solvers use backtracking, unit propagation, clause learning, and restarts.
• Applications: verification, planning, configuration, circuit design.

• Avoid ambiguous grouping—use parentheses liberally.
• Remember: P → Q is equivalent to ¬P ∨ Q, not to P ∧ Q.
• Push negations inward carefully using De Morgan’s laws.
• Watch for operator precedence differences across texts.

¬(P ∨ Q) ≡ ¬P ∧ ¬Q
¬(P ∧ Q) ≡ ¬P ∨ ¬Q

1. Classify as tautology/contradiction/contingent: (P ∨ ¬P), (P ∧ ¬P), (P → Q).
2. Convert to CNF: ¬(P → (Q ∨ R)) ∨ S.
3. Show equivalence: (P → Q) ↔ (¬P ∨ Q) using truth tables.
4. Use resolution to derive R from (P ∨ R), (¬P ∨ Q), (¬Q).