Шаг 1. Представить формулу F в виде ПНФ, т.е.
F=Âx1Âx2¼Âxn(M), где ÂiÎ{«; $}Шаг 2. Найти в префиксе самый левый квантор существования:
a) если квантор находится на первом месте префикса, то вместо переменной, связанной квантором существования, подставить всюду предметную постоянную a, отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования удалить;
б) если квантор находится не на первом месте префикса, т.е. «x1«x2¼»xi-1$xi .., то выбрать (i-1)-местный функциональный символ, отличный от функциональных символов матрицы М и выполнить замену предметной переменной xi, связанной квантором существования, на функцию f(x1;x2 ;¼ xi-1 ) и квантор существования удалить.
Шаг 3. Найти следующий справа квантор существования и перейти к исполнению шага 2, иначе конец.
Формулу ПНФ, полученную в результате введения сколемовской функции называют сколемовской стандартной формой формулы (ССФ).
Пример:
F=$x1″x2″x3$x4″x5$x6 ((P21 (x1; x2) ÚùP32(x3; x4; x5))&P 23(x4; x6)).
1) заменить предметную переменную x1 на постоянную a:
F=»x2″x3$x4″x5$x6 ((P21. (a; x2)ÚùP32.(x3; x4; x5))&P23 (x4; x6));
2) заменить предметную переменную x4 на функцию f2 1.(x2;x3):
F=»x2″x3″x5$x6 ((P21.(a; x2)ÚùP32 (x3; f 21(x2; x3); x5))&P23 (f21(x2; x3); x6));
4) заменить предметную переменную x6 на функцию
f32(x2; x3 ; x5 ):
F=»x2″x3″x5((P21(a; x2)ÚùP32(x3; f21(x2; x3); x5))&
&P23(f21(x2; x3);f32(x2; x3 ; x5 ))).
К={(P21(a; x2)ÚùP32(x3; f21(x2; x3); x5)); P23(f21(x2; x3);f32(x2; x3 ; x5 ))}.