---
title: "Short note: Skolemization"
subject: "Artificial Intelligence"
chapter: 4
key: "semester_6/artificial_intelligence:skolemization"
source: https://www.bctengineer.com/q/semester_6/artificial_intelligence/skolemization
site: BCT Engineering
---

# Short note: Skolemization

Artificial Intelligence · Chapter 4: Knowledge Representation, Inference & Reasoning

- Asked in: 2069 Bhadra, 4 marks
- Video: [Skolemization | Artificial intelligence](https://www.youtube.com/watch?v=vRSVeINP4h8) — AI world with AR
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_6/artificial_intelligence/skolemization
- Whole chapter: https://www.bctengineer.com/md/semester_6/artificial_intelligence/chapter-4

## Question

Write a short note on Skolemization.

## Short answer

Skolemization eliminates existential quantifiers during CNF conversion. Variables not in universal scope become Skolem constants; those inside become Skolem functions of the universal variables. The resulting formula is equisatisfiable but not logically equivalent to the original.

## Answer

**Skolemization** (named after Thoralf Skolem) is the process of **eliminating existential quantifiers (∃)** from a first-order logic formula while converting it to clause form for resolution. Each existentially quantified variable is replaced by a new term called a **Skolem constant** or **Skolem function**.

#### Rules
1. If the existential quantifier is **not inside** the scope of any universal quantifier, replace the variable by a new **Skolem constant**.
   - ∃x King(x) becomes King(K1), where K1 is a new constant naming "some king".
2. If the existential quantifier is **inside** the scope of universal quantifiers ∀x1 ... ∀xn, replace the variable by a **Skolem function** of those universal variables.
   - ∀x ∃y Loves(y, x) becomes ∀x Loves(F(x), x). The person who loves x depends on x.
3. The Skolem name must be **new**, i.e. not used anywhere else in the knowledge base.

#### Example
∀x ∃y Mother(y, x)  →  ∀x Mother(m(x), x) → (dropping ∀) Mother(m(x), x).

#### Notes
- Skolemization is step 5 of the CNF conversion; after it the universal quantifiers are dropped.
- The new formula is **not logically equivalent** to the original, but it is **satisfiable if and only if** the original is satisfiable, which is all that resolution refutation needs.

## Check yourself

The answer's key points as multiple-choice questions, with the correct option and why.

1. What does Skolemization do?
   A. Eliminates existential quantifiers by replacing the variables with Skolem constants or functions
   B. Eliminates universal quantifiers only
   C. Converts clauses to implications
   D. Renames all predicates
   Answer: A. It removes ∃ while converting to clause form for resolution. (Key point: Purpose)

2. What is ∀x ∃y Loves(y, x) after Skolemization?
   A. ∀x Loves(F(x), x)
   B. Loves(K1, x) with a constant K1
   C. ∃y Loves(y, F(x))
   D. ∀x ∀y Loves(y, x)
   Answer: A. The ∃ lies inside ∀x, so y is replaced by a function F(x) of x. (Key point: Skolem function)

3. When is a Skolem constant used instead of a function?
   A. When the ∃ is not inside the scope of any universal quantifier
   B. When there are many ∀ before it
   C. Always
   D. Never
   Answer: A. ∃x King(x) becomes King(K1) because no universal variable is involved. (Key point: Skolem constant)

4. How is the Skolemized formula related to the original?
   A. Logically equivalent
   B. Satisfiable iff the original is satisfiable (not equivalent)
   C. Always unsatisfiable
   D. Always valid
   Answer: B. Equisatisfiability is enough for resolution refutation. (Key point: Equivalence)