### Skolem Constants and Functions Can Handle "exists"

- Existentially quantified variables are handled by a technique called
**skolemization**, which replaces the variable with a new constant.
- For example, the formula
∃
*y* ∀ *x* .
`loves`

(*x*, *y*)
would be encoded as a formula such as `loves(X, sk1)`

, where
`sk1`

is a new constant that stands for the object that is
asserted to exist.
`sk1`

is called a **Skolem constant**.