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.