Алгоритм Сколема

Шаг 1. Представить формулу F в виде ПНФ, т. е.

F = x ₁ x ₂¼Â x_n (M), где Â_iÎ{"; $}.

Шаг 2. Найти в префиксе самый левый квантор существования:

a) если квантор находится на первом месте префикса, то вместо переменной, связанной кван­тором существования, подставить всюду предметную по­стоянную a, отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования удалить;

б) если квантор находится не на первом месте префикса, т. е. " x ₁" x ₂¼" x_{i -1} $ x_i.., то выбрать (i –1)-местный функциональный символ, отлич­ный от функциональных символов матрицы М и выполнить замену предметной переменной x_i, связанной кванто­ром существования, на функцию f (x ₁, x ₂,¼, x_{i -1}) и квантор существования удалить.

Шаг 3. Найти следующий справа квантор существования и перей­ти шагу 2, иначе конец.

Формулу ПНФ, полученную в результате введения сколемовской функции называют сколемовской стандартной формой формулы (ССФ).

Пример.

1) заменить предметную переменную x ₁ на постоянную a:

2) заменить предметную переменную x ₄ на функцию :

3) заменить предметную переменную x ₆ на функцию

:

Задание 5

Найти формулы ПНФ и ССФ.