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 .
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.