# LP, the Larch Prover -- Skolem constants and functions

A Skolem constant is a new constant that is substituted for a variable when eliminating an existential quantifier from a fact or a universal quantifier from a conjecture. For example, the fact \A x (f(x) = c) can be obtained by eliminating the existential quantifier from \E y \A x (f(x) = y) and replacing y by the Skolem constant c. As long as c does not appear in any other fact or in the current conjecture, this Skolemization represents a conservative extension of LP's logical system.

For another example, the conjecture \A x (f(x) = 0) can be proved from the subgoal f(c) = 0, where c is a Skolem constant. As long as c is new, the proof is sound.

When an existential quantifier is being eliminated from a fact that contains free variables, or when the existential quantifier occurs in the scope of a universal quantifier, the quantified variable must be replaced by a term involving a Skolem function applied to the free and universally quantified variables. For example, the fact \A x (x < bigger(x)) can be obtained by eliminating the existential quantifier from \A x \E y (x < y) and replacing y by bigger(x). See the fix command and the generalization proof method.