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

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

Для устранения кванторов существования из префикса формулы разработан алгоритм Сколема, вводящий сколемовскую функцию для связывания предметной переменной квантора существования с другими предметными переменными.

Шаг 5. Преобразовать бескванторную матрицу к виду КНФ. Алгоритм приведения матрицы формулы к виду КНФ приведен в алгебре высказываний.

Шаг 4. Вынести кванторы влево по законам алгебры логики.

Алгоритм приведения формулы к виду ПНФ

Шаг 1. Исключить всюду логические связки « и ® по правилам:

(F₁«F₂)=(F₁®F₂)& (F₂®F₁)=(ùF₁ÚF₂)&(ùF₂ÚF₁);

(F₁®F₂)=(ù F₁ÚF₂);

Шаг 2. Продвинуть отрицание до элементарной формулы по правилам:

ù"x(F)=$x(ùF); ù(F₁ÚF₂)=(ùF₁&ùF₂);

ù$x(F)="x(ùF);. ù(F₁&F₂)=(ùF₁ÚùF₂);

Шаг 3. Переименовать связанные переменные по правилу:

“ найти самое левое вхождение предметной переменной такое, что это вхождение связано некоторым квантором, но существует еще одно вхождение этой же переменной; затем сделать замену связанного вхождения на вхождение новой переменной “, операцию повторять пока возможна замена связанных переменных;

2.9. Сколемовская стандартная форма

Наличие разноимен­ных кванторов усложняет вывод заключения. Поэтому рассмотрим класс формул, содержащих только кванторы всеобщности. Фор­мула F называется " - формулой, если она представлена в ПНФ и содержит только кванторы всеобщности, т.е.

F = "_x1"_x2 ¼"_xn (M).

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

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

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

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

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

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