# Skolem Form

A first-order formula in Prenex Normal Form (PNF) can be put into a Skolem form which is satsfiable if and only if the original one is. A Skolem form is a universal sentence `∀x0...∀xn-1φ`. All of the existential quantifiers in the PNF are replaced by Skolem functions.

If we have a PNF `∀x0...∀xn-1∃y φ` where `φ` may contain quantifiers — we have only written the prefix out to the first existential quantifier — then we create the Skolem function `f` which is a new function of arity `n`. We now replace `y` in `φ` with `f(x0, ..., xn-1)` written `φ{y/f(x0, ..., xn-1)}`. If `n=0` then the Skolem function is a constant.

Lemma. The formula `∀x0...∀xn-1∃y φ` is satisfiable if and only if `∀x0...∀xn-1 φ{y/f(x0, ..., xn-1)}` is satisfiable.

Proof.

(⇒) Assume that `M` is a model such that `M⊨∀x0...∀xn-1∃y φ`. For every `x0...xn-1` there is a `y` such that `φ` is true. We can let `f(x0, ...,xn-1)` be `y` and augment `M` to have `f`. This augmented model satisfies `∀x0...∀xn-1 φ{y/f(x0, ..., xn-1)}`.

(⇐) Vacuously every model of `∀x0...∀xn-1 φ{y/f(x0, ..., xn-1)}` is a model of `∀x0...∀xn-1∃y φ`.

### Examples

• The formula ``` ∀x.a(x) ``` becomes ``` ∀x.a(x) ``` as it contains no existential quantifiers.
• The formula ``` ∃x.∀y.∃z.foo(x,y,z) ``` becomes ``` ∀y.foo(f,y,g(y)) ```

## Transformation Algorithm

The above lemma is applied until all of the existential quantifiers have been eliminated.

## Implementation

The following code can be found in the examples directory of the Barry's Prolog distribution.

First we fix a set of operators which we will need to represent the formulas of first-order logic. ``` ```

``````:-op(200, fy, ~).                   % Negation
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which is yfx)
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, =>).                 % Implication
:-op(700, xfy, <=>).                % Equivalence
``````
``` ```

``` ```

The predicate `skolem_prefix(-Prefix)` helps us build unique Skolem function names. `Prefix` is an atom used to build the principle of Skolem functions.

``` skolem_prefix('\$skolem'). ```

In a call to `skolem_index(-I)` `I` is an index counter used to make unique Skolem functions.

``` :- dynamic(skolem_index/1). skolem_index(0). ```

The predicate `fresh_skolem_atom(-Atom)` gives us a unique Skolem function's principle atom. Here `Atom` is constructed from the Skolem index and the Skolem prefix.

``` fresh_skolem_atom(Atom) :- skolem_prefix(Prefix), name(Prefix, PrefixCodes), retract(skolem_index(Index)), NewIndex is Index+1, assert(skolem_index(NewIndex)), name(Index, IndexCodes), append(PrefixCodes, IndexCodes, AtomCodes), name(Atom, AtomCodes). ```

The predicate `skolem_function(+Args, -Function)` creates a Skolem function. Here `Function` is a Skolem function which takes `Args`.

``` skolem_function(Args, Function) :- fresh_skolem_atom(Atom), Function =.. [Atom|Args]. ```

In the predicate `skolem_rewrite_variable(+Phi, +V, +W, -Psi)` the forumula `Phi` has all occurrences of the variable `V` rewritten to `W` giving `Psi` as the resulting formula.

``` skolem_rewrite_variable(F, V, W, W) :- var(F), F == V, !. skolem_rewrite_variable(F, _, _, F) :- var(F), % F \== V, !. skolem_rewrite_variable(~A0, V, W, ~A1) :- !, skolem_rewrite_variable(A0, V, W, A1). skolem_rewrite_variable(A0 /\ B0, V, W, A1 /\ B1) :- !, skolem_rewrite_variable(A0, V, W, A1), skolem_rewrite_variable(B0, V, W, B1). skolem_rewrite_variable(A0 \/ B0, V, W, A1 \/ B1) :- !, skolem_rewrite_variable(A0, V, W, A1), skolem_rewrite_variable(B0, V, W, B1). skolem_rewrite_variable(exists(X, F), V, _, exists(X, F)) :- X == V, !. skolem_rewrite_variable(exists(X, F0), V, W, exists(X, F1)) :- % X \== V, !, skolem_rewrite_variable(F0, V, W, F1). skolem_rewrite_variable(forall(X, F), V, _, forall(X, F)) :- X == V, !. skolem_rewrite_variable(forall(X, F0), V, W, forall(X, F1)) :- % X \== V, !, skolem_rewrite_variable(F0, V, W, F1). skolem_rewrite_variable(Predicate0, V, W, Predicate1) :- % processes functions and predicates Predicate0 =.. [F|Args0], skolem_rewrite_variable_in_args(Args0, V, W, Args1), Predicate1 =.. [F|Args1]. ```

A helper predicate to the one above is `skolem_rewrite_variable_in_args(+Args, +V, +W, -Result)`. Each variable `V` in `Args` is rewritten to `W` which gives the list `Result`.

``` skolem_rewrite_variable_in_args([], _, _, []) :- !. skolem_rewrite_variable_in_args([H0|T0], V, W, [H1|T1]) :- skolem_rewrite_variable(H0, V, W, H1), skolem_rewrite_variable_in_args(T0, V, W, T1). ```

The predicate `skolem_transform(+Phi, +Vars, -Psi)` organises the transformation into Skolem form. `Phi` is a subformula which is transformed into the Skolem form `Psi`. The argument `Vars` is a list of universally quantified variables which have been processed so far in the superformula.

``` skolem_transform(forall(X, Phi), Vars, forall(X, Psi)) :- !, skolem_transform(Phi, [X|Vars], Psi). skolem_transform(exists(X, Phi0), Vars, Psi) :- !, reverse(Vars, ReversedVars), skolem_function(ReversedVars, SkolemFunction), skolem_rewrite_variable(Phi0, X, SkolemFunction, Phi1), skolem_transform(Phi1, Vars, Psi). skolem_transform(Phi, _, Phi). ```

The entrypoint is the predicate `skolem_transform(+Phi, -Psi)` Here the Skolem form of `Phi` is `Psi`.

``` skolem_transform(Phi, Psi) :- skolem_transform(Phi, [], Psi). ```

## References

Chang, C-L, Lee, R C-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.