Очевидно, что если формулы F и Ф равносильны, то F логически невыполнима тогда и только тогда, когда логически невыполнима Ф. Благодаря этому утверждению и в силу того, что алгоритмы приведения в ПНФ сохраняют равносильность невыполнимых формул, в дальнейших процедурах доказательства можно ограничиться формулами, имеющими пренексный вид, и даже еще более узким классом формул, так называемыми "-формулами.
Формула F называется "-формулой, если она представлена в ПНФ, причем кванторная часть состоит только из кванторов всеобщности, т. е.
F = "x1"x2 …"xr M, где М – бескванторная формула.
Таким образом, возникает задача устранения кванторов существования в формулах, представленных в ПНФ. Это можно сделать путем введения сколемовских функций.
Пусть формула представлена в ПНФ и пусть zi (1£ i £ r) – квантор существования в префиксе. Если i = 1, т. е. ни один квантор всеобщности не стоит перед квантором существования, то выбирается константа с из области определения М, отличная от констант, встречающихся в М, и заменяется х1 на с в М. Из префикса квантор существования z1x1 вычеркивается. Если перед квантором существования zi стоит m кванторов всеобщности, то выбирается m-местный функциональный символ f, отличный от функциональных символов в М, и заменяется xi на функцию f(xj1, xj2, … xjm), называемую сколемовской функцией. Квантор существования zi xi вычеркивается из префикса.
Алгоритм последовательного исключения кванторов существования из ПНФ, основанный на описанной процедуре, называется алгоритм Сколема:
1. Формулу представить в ПНФ.
2. Найти наименьший индекс i такой, что z1z2 … zi-1 – все равны ", но zi = $. Если i = 1, то вместо х1 в формулу М подставить константу с , отличную от констант, встречающихся в М. Если такого i нет, то формула F является "-формулой.
3. Взять новый (i -1)-местный функциональный символ fi, не встречающийся в F, и заменить xi на fi (х1, …, xi-1). Перейти к шагу 2.
Переход от формулы в ПНФ к "-формуле не затрагивает свойство формулы быть невыполнимой. Таким образом, алгоритм Сколема, сохраняя свойство невыполнимости, приводит произвольную формулу, имеющую пренексный вид, к "-формуле.
Бескванторная часть формулы (матрица) должна быть приведена к КНФ. Алгоритм равносильного преобразования произвольной бескванторной формулы в КНФ аналогичен алгоритму, изложенному в исчислении высказываний.
Итак, последовательным применением алгоритмов приведения в ПНФ, Сколема и приведения к КНФ с сохранением свойства невыполнимости любая формула F может быть представлена набором дизъюнктов, объединенных кванторами всеобщности. Такая формула называется формулой, представленной в Сколемовской стандартной форме (ССФ).
Пример. Привести формулу F к ССФ.
1. F = "x [P(x) Ù "y $x (¬¬Q(x,y) Ú "z R(a,x,y))].
2. "x "y $u [P(x) Ù (Q(u,y) Ú R(a,u,y))].
3. u ® f(x,y).
4. "x "y [P(x) Ù (Q(f(x,y),y) Ú R(a, f(x,y),y))].