2015-04-12
1322
Шаг 1. Представить формулу F в виде ПНФ, т.е.
F = x 1 x 2¼Â xn (M), где ÂiÎ{"; $}.
Шаг 2. Найти в префиксе формулы самый левый квантор существования:
a) если квантор находится на первом месте префикса, то вместо переменной, связанной квантором существования, подставить всюду предметную постоянную a, отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования удалить;
б) если квантор находится не на первом месте префикса, т. е. " x 1" x 2¼" xi -1 $ xi.., то выбрать (i –1)-местный функциональный символ, отличный от функциональных символов матрицы М и выполнить замену предметной переменной xi, связанной квантором существования, на функцию f (x 1, x 2,¼, xi -1) и квантор существования удалить.
Шаг 3. Найти следующий справа квантор существования и перейти шагу 2, иначе конец.
Формулу ПНФ, полученную в результате введения сколемовской функции называют сколемовской стандартной формой формулы (ССФ).
Пример.
1) заменить предметную переменную x 1 на постоянную a:
|
|
|
2) заменить предметную переменную x 4 на функцию 
:
3) заменить предметную переменную x 6 на функцию
:
