6.4. Сколемовские стандартные формы исчисления предикатов

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

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

F = x₁x₂ …x_r M, где М – бескванторная формула.

Таким образом, возникает задача устранения кванторов существования в формулах, представленных в ПНФ. Это можно сделать путем введения сколемовских функций.

Пусть формула представлена в ПНФ и пусть _i (1 i  r) – квантор существования в префиксе. Если i = 1, т. е. ни один квантор всеобщности не стоит перед квантором существования, то выбирается константа с из области определения М, отличная от констант, встречающихся в М, и заменяется х₁ на с в М. Из префикса квантор существования ₁x₁ вычеркивается. Если перед квантором существования _i стоит m кванторов всеобщности, то выбирается m-местный функциональный символ f, отличный от функциональных символов в М, и заменяется x_i на функцию f(x_j1, x_j2, … x_jm), называемую сколемовской функцией. Квантор существования _i x_i вычеркивается из префикса.

Алгоритм последовательного исключения кванторов существования из ПНФ, основанный на описанной процедуре, называется алгоритм Сколема:

1. Формулу представить в ПНФ.

2. Найти наименьший индекс i такой, что ₁₂ … _i-1 – все равны , но _i = . Если i = 1, то вместо х₁ в формулу М подставить константу с , отличную от констант, встречающихся в М. Если такого i нет, то формула F является -формулой.

3. Взять новый (i -1)-местный функциональный символ f_i, не встречающийся в F, и заменить x_i на f_i (х₁, …, x_i-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))].

6.5. Процедура вывода Эрбрана

В исчислении предикатов не существует универсального алгоритма, который позволяет проверить общезначимость, нейтральность, невыполнимость формулы, т.к. для формулы исчисления предикатов существует бесконечное число интерпретаций. Однако было установлено, что множество дизъюнктов (СНФ) невыполнимо тогда и только тогда, когда принимает значение ложь на всех интерпретациях, на любых областях. Но так как рассмотрение всех интерпретаций на любых областях невозможно, хорошо было бы найти такую специальную область интерпретации, установив на которой факт невыполнимости множества дизъюнктов, можно было бы сделать вывод о невыполнимости этого множества на любых других областях интерпретаций. Такая область существует, называется универсумом Эрбрана и определяется следующим образом.

Пусть H_о – множество констант, появляющихся в множестве дизъюнктов S. Если в S нет констант, то в H_о включается некоторая константа, например H_о = {a}. Для i = 0,1,2, … H_i+1 = H_i  {fⁿ(t₁, t₂, …, t_n)}, где fⁿ – все n-местные функциональные символы, встречающиеся в S, а t₁, t₂, …, t_n – элементы множества H_i.

Тогда множество H = H_ называется универсумом Эрбрана для S, а H_i – его уровнем i. Элементы эрбрановой области не имеют конкретных значений, это синтаксические объекты.

Пример. Пусть S = { P(x, a, g(y))  ¬Q(х)), ¬P(f(x), a, y)  Q(a)}. Тогда

H_o = {a};

H₁ = {a, f(a), g(a)};

H₂ = {a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), g(g(a))};

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

H_ = {a, f(a), g(a), f(f(a)), f(g(a)), …}.

На универсуме Эрбрана вводится понятие эрбрановой интерпретации, или H-интерпретации. Говорят, что интерпретация I_H является H-интерпретацией для множества дизъюнктов S, если выполнены следующие условия:

1. каждому предикатному символу P_jⁿ соответствует некоторое n-местное отношение в H;

2. каждому функциональному символу f_jⁿ соответствует некоторая n-местная операция в H ( т. е. функция, отображающая Hⁿ в H);

3. каждой предметной константе a_i из S соответствует некоторая константа из H (т. е. все константы отображаются на самих в себя).

Пример. Пусть S = {¬P(f(x))  Q(x), R(x)}. Тогда примеры H-интерпретаций следующие:

I¹_H = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), …}.

I²_H = {¬P(a), ¬Q(a), ¬R(a), ¬P(f(a)), ¬Q(f(a)), ¬R(f(a)), …}.

I³_H = {P(a), ¬Q(a), ¬R(a), P(f(a)), ¬Q(f(a)), ¬R(f(a)), …}.

При I¹_H оба дизъюнкта выполнимы, при I²_H первый дизъюнкт выполним, второй – нет, при I³_H оба дизъюнкта невыполнимы, т. е. принимают значение «ложь».

В случае, если интерпретация задана не на универсуме Эрбрана, а на произвольной области D, то можно установить следующее соответствие между этими интерпретациями. Пусть дана интерпретация I на некоторой области D. Говорят, что H-интерпретация I_H соответствует интерпретации I, если имеет место следующее: пусть h₁, h₂, …, h_n, … – элементы H и пусть каждый h_i отображается на некоторый элемент d_i области D, тогда если любой P(d₁, d₂, …, d_n) принимает значение «истина» («ложь») при интерпретации I, то P(h₁, h₂, …, h_n) также принимает значение «истина» («ложь») при I_H.

Справедлива следующая теорема: множество дизъюнктов S невыполнимо тогда и только тогда, когда S ложно при всех H-интерпретациях. Таким образом, для установления невыполнимости множества дизъюнктов достаточно рассмотреть не все его интерпретации, а только H-интерпретации.

Процедура вывода Эрбрана основывается на его теореме, которая гласит: множество дизъюнктов S невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество фундаментальных примеров дизъюнктов в S.

Фундаментальным примером дизъюнкта называется дизъюнкт, полученный заменой всех переменных в этом дизъюнкте элементами универсума Эрбрана таким образом, что все вхождения одной и той же переменной в дизъюнкт заменяются на один и тот же элемент универсума.

Таким образом, для установления невыполнимости множества дизъюнктов необходимо образовать множества S₁, S₂, …, S_n, … фундаментальных примеров дизъюнктов и последовательно проверить их на ложность. Теорема Эрбрана гарантирует, что если множество S невыполнимо, то данная процедура обнаружит такое n , что S_n является ложным.

Недостаток процедуры Эрбрана состоит в экспоненциальном росте множеств S_i при увеличении i. Иной подход предложил Дж. Робинсон, который ввел принцип резолюций, являющийся теоретической основой для построения большинства методов автоматического доказательства теорем.