5.3. Стандартная нормальная форма

3. Предваренная нормальная форма не единственна для формулы. Результат зависит от порядка применения эквивалентных преобразований, а также от произвола при переименовании. Эквивалентны, например, следующие ПНФ:

8x(P (x) ^ Q(x)) и 8x8y(P (x) ^ Q(y)). I

Пример 5.6.

Преобразовать в ПНФ формулу 8xP (x) ! 9xQ(x).

8xP (x) ! 9xQ(x) = :(8xP (x)) _ 9xQ(x) =

=9x(:P (x)) _ 9xQ(x) = 9x(:P (x) _ Q(x)) =

=9x(P (x) ! Q(x)). J

Очевидны следующие соотношения для кванторов (почему?):

8x8yP (x; y) = 8y8xP (x; y);

9x9yP (x; y) = 9y9xP (x; y);

9x8yP (x; y) =6 8y9xP (x; y).

5.3 Стандартная нормальная форма

Для исчисления высказываний мы приводили формулы к КНФ и представляли КНФ в виде множества клозов. Затем задача логического вывода сводилась к выводу пустого клоза 2 из множества клозов. Нечто подобное мы хотим сделать и с формулами исчисления первого порядка – привести к некоторой стандартной нормальной форме (СНФ), а затем представить в виде множества клозов.

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

1.Приведение формулы к ПНФ.

2.Приведение матрицы M формулы (в ПНФ) к конъюнктивной нормальной форме (КНФ). Матрица M представлена

вКНФ, если она записана в виде M = C1 ^C2 ^¢ ¢ ¢^Cn, где Ci

– клоз. Приведение матрицы к КНФ достигается применением нужного числа раз дистрибутивного закона F _ (G ^ H) = (F _ G) ^ (F _ H).

3. Сколемизация – исключение из формулы кванторов существования 9.

Пусть формула F представлена в ПНФ:

ij1x1ij2x2 : : :ijnxnM[x1; : : : ; xn],

где M представлена в КНФ.

Пусть, далее, ijkxk; 1 · k · n, есть квантор 9xk. Если никакой квантор всеобщности 8xj не находится в префиксе левее 9xk =ijkxk, то выберем новую константу c, отличную от констант входящих в M, и заменим все вхождения xk в M на c, а ijkxk удалим из префикса.

Если ijs1 xs1 ¢ ¢ ¢ijsm xsm – список всех кванторов всеобщности, встретившихся левее 9xk =ijkxk, 1 · s1 < s2 < ¢ ¢ ¢ < k, то выберем новый m-местный функциональный символ f, отличный от других функциональных символов, заменим в M все xk на f(xs1 ; : : : ; xsm ) и удалим ijkxk из префикса.

Этот процесс применим ко всем кванторам существования в префиксе. В результате полученная формула будет представлена в стандартной нормальной форме формулы F

(сколемовской, клаузальной, стандартной форме). Константы и функции, используемые для замены переменных, связанных квантором 9, называются сколемовскими функциями. Выбор сколемовских функций не произволен: для каждой конкретной формулы выбирается конкретная функция.

Примеры 5.7. .

1. Пусть дана формула 8y9x[x + y = 0]; D = R (множество вещественных чисел). Ясно, что этой формуле удовлетворяет функция x = f(y) = (¡y). Заменив вхождение переменной x в формулу на f(y) и удалив квантор 9 из префикса, получим стандартную форму исходной формулы:

8y[(¡y) + y = 0].

2.Пусть G = (X; U) – обыкновенный граф, где X – множество вершин, U – множество ребер, а предикат P (x; u; y) чи-

тается следующим образом: ребро u 2 U соединяет вершины x; y 2 X. Тогда определение полного обыкновенного графа (все вершины которого попарно смежны) можно записать с помощью формулы:

8x 2 X8y 2 X9u 2 U [P (x; u; y)].

Для представления этой формулы в стандартной форме заменим вхождение переменной u в формулу на f(x; y) и удалим квантор 9 из префикса. Теперь формула представляется в виде

8x8y [P (x; f(x; y); y],

где f(x; y) определяет ребро, соединяющее вершины x; y. J

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

Пример 5.8.

Представить в виде множества клозов формулу

8x9y9z[(:P (x; y) ^ Q(x; z))) _ R(x; y; z)].

Эта формула представлена в ПНФ. Приведем матрицу M к КНФ:

[:P (x; y) _ R(x; y; z)] ^ [Q(x; z) _ R(x; y; z)].

Проведем сколемизацию. Перед кванторами 9y и 9z есть квантор всеобщности 8x. Поэтому заменим переменные y; z соответственно одноместными функциями f(x) и g(x). Получим

8x[(:P (x; f(x)) _ R(x; f(x); g(x)) ^ (Q(x; g(x)) _ R(x; f(x); g(x))].

Образуем множество клозов:

S = f:P (x; f(x))_R(x; f(x); g(x)); Q(x; g(x))_R(x; f(x); g(x))g. J

Приводя формулу к стандартной (клаузальной) форме, мы хотели иметь удобное представление для доказательства

противоречивости формулы. Удаляя кванторы существования мы предполагаем, что противоречивость формулы сохраняется. Это действительно так.

Пусть S – множество клозов, которые представляют стандартную форму формулы F .

Теорема 5.1 Формула F противоречива тогда и только тогда, когда множество S противоречиво.

З а м е ч а н и е. Подчеркнем, что при сколемизации сохраняется только противоречивость, а не эквивалентность F = S, которая может не сохраняться. I

Д о к а з а т е л ь с т в о . Без потери общности можно положить, что F представлена в ПНФ, т.е.

F =ij1x1 ¢ ¢ ¢ijnxnM[x1; : : : ; xn]:

Пусть ijk первый слева в формуле квантор 9 и пусть

F1 =ij1x1 ¢ ¢ ¢ijk¡1xk¡1ijk+1xk+1 ¢ ¢ ¢ijnxn

M[x1; : : : ; xk¡1; f(x1; : : : ; xk¡1); : : : ; xn],

где f(x1; : : : ; xk¡1) – сколемовская функция, соответствующая xk; 1 · k · n.

Покажем, что F противоречива тогда и только тогда, когда F1 противоречива.

°) Пусть F противоречива. Если F1 непротиворечива, то существует такая интерпретация I, что F1 истинна в I, т.е.

для всех x1; : : : ; xk¡1 существует элемент f(x1; : : : ; xk¡1), для которого формула

ijk+1xk+1 ¢ ¢ ¢ijnxnM[x1; : : : ; xk¡1; f(x1; : : : ; xk¡1); xk+1; : : : ; xn],

истинна в I. Но тогда и F истинна в I, что противоречит предположению. Следовательно, F1 должна быть противоречивой.

°( Пусть теперь F1 противоречива. Если F непротиворечива, то в D существует такая интерпретация I, что F истинна в I, т.е. для всех x1; : : : ; xk¡1 существует такой элемент xk, что