4.3. Равносильности логики предикатов

Помимо эквивалентностей логики высказываний для логики предикатов справедливы следующие эквивалентности (, , - предикаты, a - высказывание):

Комбинация кванторов:

1.;

2. ;

3. .

Комбинация кванторов и отрицаний:

;

;

;

.

Расширение области действия кванторов ( не зависит от ):

1. ;

69

2. ;

3. ;

4. ;

5. ;

6. ;

7. ;

8. .

Расширение области действия кванторов:

1. ;

2.;

3. ;

4. ;

5. /

4.4. Предваренная, сколемовская нормальная и сколемовская стандартная формы

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

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

Например, для нормальной формы

предваренной нормальной формой будет .

70

Всякую формулу логики предикатов можно свести к ПНФ, если использовать следующий алгоритм:

Шаг 1. Исключение логических связок и .

Шаг 2. Продвижение знака отрицания до атома. Многократно (пока это возможно) делаются замены:

,

,

,

,

.

Шаг 3. Переименование связанных переменных.

Шаг 4. Вынесение кванторов. Для вынесения кванторов используются формулы эквивалентности для исчисления предикатов.

После выполнения четвертого шага получаем ПНФ.

Остановимся более подробно на третьем пункте алгоритма - переименовании переменных.

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

Таким образом, переименовывать связанные переменные необходимо только в самом кванторе и в области

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

71

Пример 1. Пусть имеем формулу . Нормальная формула имеет вид .

Переименовываем переменную в кванторе и в области действия этого квантора на .

.

В полученной формуле переменную можно переименовать на в первой посылке и на во второй посылке, либо оставить во второй посылке без изменения

=

Следующие примеры иллюстрируют применение алгоритма приведения к ПНФ.

Пример 2. .

Шаг 1.

Шаг 2.

.

Шаг 3.

.

Шаг 4. Квантор существования можно вынести за знак дизъюнкции, так как второй член дизъюнкции не зависит от и может рассматриваться как константа.

Многократно используя этот подход, получаем

.

72

Пример 3.

Шаг 1. Так как выражение не содержит операций импликации и эквиваленции, то нет необходимости в первом шаге.

Шаг 2 .

Шаг 3.

Шаг 4. =

.

Можно рассматривать еще более узкий класс формул, так называемых ‑ формул.

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

Сколемовская нормальная форма (СНФ) строится в соответствии со следующими правилами:

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

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

73

Пример 1.

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

На следующем шаге вычеркиваем квантор существования и все вхождения переменной заменяем на функцию

.

На последнем шаге вычеркиваем квантор .

.

Переход от ПНФ к сколемовской нормальной форме не затрагивает свойство формулы быть невыполнимой (противоречивой). Это доказывается следующей теоремой.

Теорема. Пусть формула задана в ПНФ и преобразована в СНФ. Тогда в ПНФ логически невыполнима тогда и только тогда, когда невыполнима СНФ для .

Однако следует заметить, что если имеется выполнимая формула , то может оказаться, что СНФ для будет невыполнимой.

Рассмотрим теперь преобразование бескванторной части к виду так называемых дизъюнктов. Дизъюнктом называется формула вида , где  – произвольная литера. Дизъюнкт, не имеющий литер, называется пустым дизъюнктом (). По определению он всегда ложен.

Дизъюнкты, соединенные знаком &, образуют КНФ.

74

Рассмотрим алгоритм равносильного преобразования произвольной бескванторной формулы в КНФ.

Шаг 1. Дана формула , составленная из литер с применением связок & и . Предполагается, что в формуле исключены скобки между одинаковыми связками, т.е. нет выражений вида , , , .

Шаг 2. Найти первое слева вхождение символов “ ( “ или “) ” (здесь предполагается, что скобка не является скобкой атома). Если таких вхождений нет, то - формула находится в КНФ.

Шаг 3. Пусть первым вхождением указанной пары символов является “(“. Тогда нужно взять наибольшие формулы такие, что в входит формула , которая связана с вхождением “(“. Заменить формулу на формулу

&

Шаг 4. Пусть первым вхождением является “)”. Тогда взять наибольшие формулы такие, что в входит формула , связанная с вхождением “)”. Заменить на формулу

.

Шаг 5. Перейти к шагу 2.

Пример. Преобразовать формулу

в КНФ.

75

Отрабатываем сначала первое, а потом второе вхождение символов “”.

=

=

.

Здесь чертой подчеркнуты вхождения “”. Кроме того, в алгоритме надо предусмотреть приведение подобных членов, а также всевозможные склеивания и поглощения.

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

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

Например, множеству дизъюнктов

соответствует следующее представление в ССФ

И, наконец, когда говорят, что множество дизъюнктов

76

невыполнимо (противоречиво), то всегда подразумевают невыполнимость формулы где – различные переменные, входящие в дизъюнкты.

Доказательство правильности логического вывода основано на следующих теоремах.

Теорема 1. Даны формулы и . Формула является логическим следствием формул тогда и только тогда, когда формула общезначима.

Теорема 2. Даны формулы и . Формула является логическим следствием формул тогда и только тогда, когда формула противоречива.

Рассмотрим механизм доказательства правильности умозаключения для логики предикатов на примере

╞ .

Воспользуемся второй теоремой. Сначала приведем это выражение к ССФ. Найдем отрицание заключения:

=

=.

Перейдем к ПНФ

.

Получаем СНФ, которая одновременно является и ССФ.

.

Формируем произведение

.

77