- 2069 Bhadra · 4 marks
Short note: 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.
Write a short note on Skolemization.
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
- 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".
- 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.
- 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.
✓ Answer checked by Claude Opus 5.5 (high effort)