:- ensure_loaded('../Basis/internal_operators.pl').
:- use_module('../Basis/utilities.pl').

%
%  skolemize(+PrenexFormula, -SkolemizedFormula)
%    SkolemizedFormula is the result of applying skolemization to
%    the prenex formula PrenexFormula, that should not contain any term
%    of the form fi for any nonnull natural number i
%
skolemize(PrenexFormula, SkolemizedFormula) :-
	reset_gensym(f),
	skolemize(PrenexFormula, [], [], SkolemizedFormula).

%
%  skolemize(+Form, +UniversalVars, +SkolemMapping, -SkolemizedForm)
%    Form is a formula in prenex form, that should not contain any term
%    of the form fi for any nonnull natural number i;
%    existential quantifiers in Form are removed and the corresponding
%    quantified variables in the matrix of Form are replaced by Skolem
%    functions, taking as arguments the members of the list UniversalVars
%    of preceding universally quantified variables;
%    SkolemMapping is the list of pairs of the form (X, fi(Y1,..,Yn))
%    such that existentially quantified variable X has been replaced by
%    a Skolem function of the form fi(Y1,..,Yn) in the matrix of Form 
%
skolemize(forall X sep A, UniversalVars, SkolemMapping, forall X sep B) :- !,
	skolemize(A, [X| UniversalVars], SkolemMapping, B).
skolemize(exists X sep A, UniversalVars, SkolemMapping, B) :- !,
	gensym(f, SkolemFunctionSymbol),
	SkolemFunction =.. [SkolemFunctionSymbol| UniversalVars],
	skolemize(A, UniversalVars, [(X, SkolemFunction)| SkolemMapping], B).
skolemize(Formula, _, [(X, SkolemFunction)| SkolemMapping], SkolemFormula) :-
	instance(X, SkolemFunction, Formula, Instance),
	skolemize(Instance, _, SkolemMapping, SkolemFormula).
skolemize(Formula, _, [], Formula).