First-Order Logic (FOL), also called predicate logic or predicate calculus, extends propositional logic with quantifiers (∀, ∃), variables, constants, functions, and predicate symbols. This expressiveness allows FOL to represent general facts about objects and their relationships — making it the dominant formal language for knowledge representation in classical AI. Key GATE topics include FOL syntax, semantics, unification, generalized modus ponens, forward/backward chaining, and resolution in FOL.
FOL syntax: the vocabulary
| Syntactic element | Examples | Meaning |
|---|---|---|
| Constants | John, Mary, 2, IIT | Specific objects in the world |
| Variables | x, y, z | Placeholders for objects (must be bound by a quantifier) |
| Predicates | Loves(x,y), Prime(n), Student(x) | Properties of or relations between objects; return T or F |
| Functions | FatherOf(x), Plus(x,y) | Map objects to objects; return a constant, not a truth value |
| Connectives | ¬, ∧, ∨, →, ↔ | Same as propositional logic |
| Quantifiers | ∀ (for all), ∃ (there exists) | Bind variables over domains |
| Equality | x = y | Two terms refer to the same object |
An atomic sentence is a predicate applied to terms (constants, variables, or function applications): e.g., Loves(John, Mary), Parent(FatherOf(John), John). Complex sentences are built from atomic sentences and connectives.
Quantifiers and their semantics
Universal quantification ∀x P(x) means 'P(x) is true for every object x in the domain.' Existential quantification ∃x P(x) means 'there is at least one object x for which P(x) is true.'
| Statement | FOL | Common mistake |
|---|---|---|
| All students are smart | ∀x [Student(x) → Smart(x)] | NOT ∀x [Student(x) ∧ Smart(x)] — that would mean everything is a student AND smart |
| Some students are smart | ∃x [Student(x) ∧ Smart(x)] | NOT ∃x [Student(x) → Smart(x)] — a non-student makes this vacuously true |
| No student is dumb | ∀x [Student(x) → ¬Dumb(x)] | Equivalently: ¬∃x [Student(x) ∧ Dumb(x)] |
| All students have a teacher | ∀x [Student(x) → ∃y [Teacher(y) ∧ Teaches(y,x)]] | y is inside the scope of x — different teacher for each student |
Quantifier scope (critical for GATE)
∀x∃y Loves(x,y) ≠ ∃y∀x Loves(x,y). The first says "everyone loves someone (possibly different)"; the second says "there is one person everyone loves." The order of quantifiers matters when they are mixed.
Unification
Unification finds the most general substitution θ (the Most General Unifier, MGU) that makes two terms identical. It is the key computational step in FOL inference.
| Pair to unify | Substitution (MGU) | Result |
|---|---|---|
| Knows(John, x) and Knows(John, Jane) | {x/Jane} | Knows(John, Jane) |
| Knows(John, x) and Knows(y, Bill) | {y/John, x/Bill} | Knows(John, Bill) |
| Knows(John, x) and Knows(x, Elizabeth) | Fail | x cannot be both John and Elizabeth simultaneously |
| Parent(x, f(x)) and Parent(Bill, f(Bill)) | {x/Bill} | Parent(Bill, f(Bill)) |
The occurs check (verifying that a variable x does not appear in term t before setting x←t) prevents circular substitutions. Standard Prolog omits the occurs check for efficiency, which can lead to unsoundness in rare cases.
Inference in FOL
Generalized Modus Ponens (GMP) combines unification with Modus Ponens: given atomic sentences p₁', …, pₙ' and an implication (p₁ ∧ … ∧ pₙ → q) where there is a substitution θ unifying each pᵢ' with pᵢ, infer q·θ.
Generalized Modus Ponens (GMP) — the core inference step in forward and backward chaining over FOL knowledge bases.
| Inference method | Direction | Complete for? | Efficient for? |
|---|---|---|---|
| Forward chaining | Data → Goals (breadth-first over facts) | Definite clauses (Horn clauses) | Query-agnostic; all consequences of KB |
| Backward chaining | Goal ← Subgoals (depth-first, goal-directed) | Definite clauses | Specific queries; underlies Prolog |
| Resolution (full FOL) | Refutation proof | Complete for full FOL | Theorem proving; slower but more general |
A Horn clause has at most one positive literal: either a fact (one positive literal, no negative: p) or an implication with a positive head and a conjunction of positive body literals: p₁ ∧ … ∧ pₙ → q. Knowledge bases of Horn clauses support efficient polynomial-time inference via chaining.
Converting FOL to CNF (Skolemization)
To use resolution in FOL, sentences must be converted to Clausal Form (CNF). This requires Skolemization to eliminate existential quantifiers:
- Eliminate biconditionals and implications
- Move ¬ inward (use De Morgan and quantifier negation: ¬∀x P ≡ ∃x ¬P, ¬∃x P ≡ ∀x ¬P)
- Standardize variables — rename so each quantifier uses a unique variable name
- Skolemize — replace each existentially quantified variable y with a Skolem function F(x₁,...,xₙ) where x₁,...,xₙ are the universally quantified variables in scope: ∃y Loves(x,y) → Loves(x, F(x))
- Drop universal quantifiers — after Skolemization, all remaining variables are implicitly universally quantified
- Distribute ∨ over ∧ to produce CNF clauses
Skolem constants vs. functions
∃x Loves(John, x) has no free universally quantified variables, so ∃x is replaced by a Skolem constant C: Loves(John, C). ∀x ∃y Parent(x,y) has x in scope, so ∃y is replaced by Skolem function: Parent(x, F(x)).
GATE PYQ Spotlight
GATE DA — FOL to English (2-mark)
Translate ∀x [Ball(x) ∧ ¬UsedInRugby(x) → Round(x)] to English. Answer: "Every ball that is not used in rugby is round." Equivalently: "All balls are round except those used in rugby." Common trap: ∀x [Ball(x) ∧ UsedInRugby(x) → ¬Round(x)] says rugby balls are not round (wrong meaning). The correct translation preserves "all balls except rugby balls are round."
GATE CS — Unification (1-mark)
Which pair CANNOT be unified? (A) P(a,b) and P(x,b) (B) P(f(a),y) and P(x,b) (C) P(x,x) and P(a,b) with a≠b (D) P(f(x),y) and P(y,f(a)) Answer: (C) P(x,x) and P(a,b) — requires x=a and x=b simultaneously; impossible if a≠b. (D) requires y=f(x) and y=f(a), giving f(x)=f(a) and x=a — this actually succeeds. The key is to check each substitution step for consistency.
Practice questions
- Translate: 'Every student who studies hard passes the exam' into FOL. (Answer: ∀x. (Student(x) ∧ StudiesHard(x)) → PassesExam(x). Read: For all x, if x is a Student AND x StudiesHard, then x PassesExam. Note the implication (→) rather than conjunction — we don't claim everyone studies hard, just that students who do pass.)
- What is the difference between ∀x P(x) and ∃x P(x)? Give an example of a false statement of each form. (Answer: ∀x P(x): 'For ALL x, P(x) holds.' False example: ∀x. Bird(x) → CanFly(x) — penguins are birds that cannot fly. ∃x P(x): 'There EXISTS at least one x where P(x) holds.' False example: ∃x. Human(x) ∧ LivedForever(x) — no human has lived forever. Universal claims are falsified by one counterexample; existential claims require proving no case exists.)
- What is unification in FOL and give an example? (Answer: Unification: finding a substitution θ that makes two FOL expressions identical. Example: Unify P(x, f(y)) and P(a, f(b)). Substitution θ = {x/a, y/b} makes both P(a, f(b)). Used in resolution theorem proving: to apply a rule '∀x. Human(x) → Mortal(x)' to 'Human(Socrates)', unify x with Socrates, deriving Mortal(Socrates). Unification is the core operation of Prolog's inference engine.)
- What is the resolution principle in FOL and how does it enable theorem proving? (Answer: Resolution: from (A ∨ p) and (¬p ∨ B), derive (A ∨ B) — the resolvent eliminates p. For theorem proving (refutation): negate the goal, add it to the knowledge base in CNF, repeatedly apply resolution. If the empty clause □ is derived, the original goal is provable. Resolution is sound and complete for FOL — if a proof exists, resolution will find it. Limitation: resolution can explore exponentially many resolvents; heuristics (SLD resolution in Prolog) control search.)
- What is the closed world assumption (CWA) and open world assumption (OWA) in FOL knowledge bases? (Answer: CWA (Prolog, databases): if a fact is not in the knowledge base, assume it is FALSE. Fast, efficient. Used when the KB is assumed complete. OWA (Description logics, ontologies, RDF/OWL): if a fact is not in the KB, it is simply UNKNOWN — not false. Essential for incomplete knowledge representations. Example: if the KB has no entry for 'CanFly(Penguin)', CWA concludes penguins cannot fly; OWA concludes we don't know.)