На этом шаге мы рассмотрим доказательство общезначимости и противоречивости формул в логике предикатов первого порядка.

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

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

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

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

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

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

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

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

Дизъюнктом называется дизъюнкция литер. Множество литер можно рассматривать как синоним дизъюнкта.

Дизъюнкт, содержащий n литер, называется n-литерным дизъюнктом.

Однолитерный дизъюнкт называется единичным дизъюнктом.

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

Метод резолюций для логики высказываний

Метод резолюций можно применять к любому множеству дизъюнктов с целью проверки их невыполнимости (противоречивости). Рассмотрим сначала метод резолюций для логики высказываний.

Литеры A и ~A называются контрарными, а множество {A, ~A} – контрарной парой.

Допустим, что в дизъюнкте C₁ существует литера L₁ , контрарная литере L₂ в дизъюнкте C₂. Вычеркнем литеры L₁ и L₂ из дизъюнктов C₁ и C₂ соответственно и построим дизъюнкцию оставшихся дизъюнктов. Построенный дизъюнкт называется резольвентой дизъюнктов C₁ и C₂. Резольвента двух дизъюнктов является их логическим следствием. Резольвента двух единичных дизъюнктов (если она существует) – пустой дизъюнкт.

Резолютивный вывод C из множества дизъюнктов S есть такая конечная последовательность C₁, C₂, ..., C_k дизъюнктов, в которой каждый C_i (i=1, ..., k) или принадлежит S, или является резольвентой дизъюнктов, предшествующих C_i и C_k=C.

Дизъюнкт C может быть выведен или получен из S, если существует вывод C из S. Для невыполнимого множества дизъюнктов в результате последовательного применения правила резолюций получается пустой дизъюнкт.

Вывод из множества S пустого дизъюнкта называется опровержением (доказательством невыполнимости) S.

Метод резолюций для логики предикатов первого порядка

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

Рассмотрим несколько примеров.

Пусть формулы A(x) и A(b) не тождественны. В формуле A(x) встречается переменная x, а в A(b) – константа b. Чтобы отождествить A(x) и A(b), заменим переменную x на константу b, то есть присвоим переменной x значение b. В результате получаем A(x)=A(b).
Рассмотрим дизъюнкты: D₁: A(x) B(x),
D₂: ~A(f(y)) C(y),
которые не содержат контрарных литер. Если в D₁ подставить f(a) вместо x, а в D₂ – значение a вместо y, то дизъюнкты преобразуются к следующему виду:
    D₁: A(f(a)) B(f(a)),
    D₂: ~A(f(a)) C(a).

    Так как A(f(a)) и ~A(f(a)) контрарны, то получим резольвенту дизъюнктов D₁ и D₂ в виде:
    R: B(f(a)) C(a).

Дизъюнкты имеют одну или несколько резольвент, так как возможны разные подстановки. Любую подстановку можно представить с помощью множества упорядоченных пар t_i/x_i:

S={t₁/x₁, t₂/x₂ , ..., t_n/x_n},

где t_i – терм, x_i – переменная, i=1, ..., n.

Пара t_i/x_i означает, что переменная x_i повсюду заменяется на терм t_i. Переменная не может быть заменена на терм, содержащий ту же самую переменную, например переменную x_i нельзя заменить на терм t_i=f(x_i).

Если подстановка S применяется к каждому члену некоторого множества {E_i}, то множество подстановочных выражений обозначается {E_i}S. Множество выражений {E_i} унифицируемо, если существует подстановка S такая, что E₁S= E₂S= E₃S=... . В таком случае S называется унификатором для множества выражений {E_i}.

Например, подстановка S={A/x,B/y} унифицирует выражения P(x,f(y),B) и P(x,f(B),B). После замены переменной x на терм A и переменной у на терм В выражение P(x,f(y),B) преобразуется в P(A,f(B),B), a P(x,f(B),B) в P(A,f(B),B). Полученные выражения унифицируемы.

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

Процесс сопоставления некоторого выражения с эталонным называется сопоставлением с образцом. Он играет важную роль в системах искусственного интеллекта.

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

На следующем шаге мы рассмотрим семь этапов приведения формул к стандартной форме записи.

Предыдущий шаг Содержание Следующий шаг