Propositional logic (also called propositional calculus or Boolean logic) is a formal system for representing and reasoning about propositions — statements that are either true or false. It forms the simplest knowledge representation language in AI. Key components include propositional symbols, logical connectives (¬, ∧, ∨, →, ↔), truth tables, logical equivalences, normal forms (CNF, DNF), inference rules, and the resolution algorithm. GATE DA tests tautology identification, CNF conversion, resolution proofs, and the soundness/completeness of inference procedures.
Syntax: the language
Propositional logic sentences are built from atomic propositions (symbols like P, Q, R — each representing a statement that is true or false) and connectives:
| Connective | Symbol | English | True when... |
|---|---|---|---|
| Negation | ¬P | not P | P is false |
| Conjunction | P ∧ Q | P and Q | Both P and Q are true |
| Disjunction | P ∨ Q | P or Q | At least one of P, Q is true |
| Implication | P → Q | if P then Q | P is false, OR Q is true (equiv: ¬P ∨ Q) |
| Biconditional | P ↔ Q | P if and only if Q | P and Q have the same truth value |
Implication trap
P → Q is FALSE only when P is TRUE and Q is FALSE. If P is false, P → Q is vacuously true regardless of Q. This is a frequent source of error. Remember: ¬P ∨ Q is logically equivalent to P → Q.
Semantics: truth tables and satisfiability
The truth value of a sentence is determined by its semantics: a model assigns a truth value (T or F) to every propositional symbol. A sentence is: satisfiable if it is true in at least one model; valid (tautology) if it is true in every model; unsatisfiable (contradiction) if it is false in every model.
| P | Q | P∧Q | P∨Q | P→Q | P↔Q | ¬P→Q |
|---|---|---|---|---|---|---|
| T | T | T | T | T | T | T |
| T | F | F | T | F | F | T |
| F | T | F | T | T | F | T |
| F | F | F | F | T | T | F |
Entailment vs. implication
KB ⊨ α (KB entails α) means: in every model where KB is true, α is also true. This is a semantic relationship between sentences, not a symbol in the language. P → Q is a sentence in the language; if it is a tautology, it reflects an entailment. Distinguishing KB ⊨ α from KB → α is essential for GATE.
Logical equivalences (critical for GATE)
| Equivalence | Formula | Name |
|---|---|---|
| Double negation | ¬¬P ≡ P | |
| Commutativity | P∧Q ≡ Q∧P; P∨Q ≡ Q∨P | |
| Associativity | (P∧Q)∧R ≡ P∧(Q∧R) | |
| Distributivity | P∧(Q∨R) ≡ (P∧Q)∨(P∧R) | |
| De Morgan | ¬(P∧Q) ≡ ¬P∨¬Q; ¬(P∨Q) ≡ ¬P∧¬Q | Push negation inward, flip connective |
| Implication elimination | P→Q ≡ ¬P∨Q | Essential for CNF conversion |
| Contrapositive | P→Q ≡ ¬Q→¬P | Equivalent direction of reasoning |
| Biconditional elimination | P↔Q ≡ (P→Q)∧(Q→P) | |
| Modus Ponens (valid inference) | P, P→Q ⊢ Q | From premises P and P→Q, derive Q |
| Modus Tollens (valid inference) | ¬Q, P→Q ⊢ ¬P |
Conjunctive Normal Form (CNF) and the DPLL algorithm
A CNF formula is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals (a literal is a propositional symbol or its negation). Every propositional sentence can be converted to CNF in polynomial time.
Steps to convert to CNF: (1) Eliminate biconditionals: P↔Q → (P→Q)∧(Q→P). (2) Eliminate implications: P→Q → ¬P∨Q. (3) Move ¬ inward using De Morgan and double negation. (4) Distribute ∨ over ∧.
CNF conversion example: (P → Q) ↔ R
Step 1: Eliminate biconditional (↔):
((P→Q)→R) ∧ (R→(P→Q))
Step 2: Eliminate implications (→):
(¬(P→Q)∨R) ∧ (¬R∨(¬P∨Q))
= (¬(¬P∨Q)∨R) ∧ (¬R∨¬P∨Q)
Step 3: Move ¬ inward (De Morgan on ¬(¬P∨Q)):
((P∧¬Q)∨R) ∧ (¬R∨¬P∨Q)
Step 4: Distribute ∨ over ∧:
(P∨R) ∧ (¬Q∨R) ∧ (¬R∨¬P∨Q)
Final CNF: 3 clauses: (P∨R), (¬Q∨R), (¬R∨¬P∨Q)DPLL (Davis-Putnam-Logemann-Loveland) is the foundational SAT-solving algorithm. It checks satisfiability via: (1) Unit propagation — if a clause has one literal, assign it true. (2) Pure symbol elimination — if a symbol appears only positively or only negatively, assign it to satisfy all such clauses. (3) Split — pick an unassigned symbol and recurse on both truth values.
Resolution — a complete inference procedure
Resolution is a single inference rule that operates on CNF clauses and is both sound and complete for propositional logic. Given two clauses containing complementary literals P and ¬P, the resolvent is the disjunction of all remaining literals from both clauses.
Resolution rule: P and ¬P cancel out. The resolvent is the disjunction of all remaining literals from both parent clauses.
Proof by refutation (resolution refutation): to prove KB ⊨ α, add ¬α to KB (both in CNF), then apply resolution until the empty clause (□, representing FALSE) is derived or no new clauses can be derived. If □ is derived, KB ⊨ α; otherwise, KB ⊭ α.
Soundness & completeness of resolution
Resolution is sound (every derived clause is logically entailed) and refutation-complete (if KB ⊨ α, refutation will eventually find the empty clause). But resolution is not complete for generating all entailed sentences — only for refutation.
GATE PYQ Spotlight
GATE DA 2025 — Propositional tautologies (2-mark)
Let p and q be any two propositions. Consider: S₁: p → ((p → q) → q) S₂: (p → q) → (¬q → ¬p) S₃: (p ∧ (p → q)) → q Which are tautologies? Answer: All three are tautologies. S₁: "If p is true, and if p implies q, then q" — this is Modus Ponens encoded as a sentence. S₂: this is the contrapositive (P→Q ≡ ¬Q→¬P). S₃: Modus Ponens written as a single formula. Verify by truth table: check all 4 combinations of p,q.
GATE DA — FOL natural language representation (1-mark)
Which is a correct logical representation of "All balls are round except balls used in rugby"? Let Ball(x), Round(x), UsedInRugby(x). Answer: ∀x [Ball(x) ∧ ¬UsedInRugby(x) → Round(x)] Note: "All A except B are C" translates to ∀x[A(x) ∧ ¬B(x) → C(x)]. The common wrong answer is ∀x[Ball(x) → ¬UsedInRugby(x) → Round(x)] which is logically equivalent here but ∀x[Ball(x) ∧ UsedInRugby(x) ∧ ¬Round(x)] is wrong (claims all objects have all three properties).
Practice questions
- What is the difference between satisfiability and validity in propositional logic? (Answer: Satisfiable: there EXISTS at least one truth assignment that makes the formula true. '{p ∧ q}' is satisfiable (both true). Unsatisfiable (contradiction): NO assignment makes it true. '{p ∧ ¬p}' is unsatisfiable. Valid (tautology): ALL assignments make it true. '{p ∨ ¬p}' is always true. Key: satisfiability is about existence; validity is about universality. SAT solvers determine satisfiability — a central problem in computer science (NP-complete for general propositional formulas).)
- What is modus ponens and how is it used in AI inference systems? (Answer: Modus ponens: from P and P → Q, infer Q. Example: 'It is raining' (P), 'If it rains the ground is wet' (P → Q), therefore 'The ground is wet' (Q). In AI: rule-based systems chain modus ponens applications: if symptom A → disease B, symptom A is present → infer disease B. This is forward chaining. Backward chaining: start from goal (disease B?), find rules with B in consequent (A → B), check if A is present. Both are sound inference strategies based on modus ponens.)
- What is conjunctive normal form (CNF) and why is it important for SAT solving? (Answer: CNF: a conjunction of clauses, where each clause is a disjunction of literals. Example: (p ∨ q) ∧ (¬p ∨ r) ∧ (q ∨ ¬r). Any propositional formula can be converted to CNF (Tseitin transformation). SAT solvers (DPLL, CDCL) require CNF input — they exploit the clause structure for efficient backtracking search. Key: if any clause is all-false, the formula is unsat. If all clauses have at least one true literal, it is sat. The DIMACS format for SAT instances is CNF.)
- What is the completeness of propositional resolution and how does it relate to SAT? (Answer: Propositional resolution: from (A ∨ p) and (B ∨ ¬p), derive (A ∨ B) — the 'resolution rule.' Resolution is refutation-complete: if a set of clauses is unsatisfiable, repeated application of resolution WILL derive the empty clause (contradiction). However, refuting a satisfiable formula requires detecting when no further resolutions are possible. Modern SAT solvers implement CDCL (Conflict-Driven Clause Learning) — a highly optimised resolution with learned clauses.)
- How does propositional logic differ from first-order logic in expressive power? (Answer: Propositional logic: propositions are atomic (P, Q, R) — no quantifiers, no variables, no predicates. Limited: 'All humans are mortal' requires one proposition per human. First-order logic: includes predicates (Human(Socrates)), variables (x), and quantifiers (∀x∃y). 'All humans are mortal': ∀x. Human(x) → Mortal(x). Much more expressive but harder computationally (semi-decidable). Propositional logic: decidable (SAT). First-order logic: undecidable (halting problem). Most AI knowledge representation uses first-order or description logics.)