Материал: Волченков Логическое программирование язык пролог 2015

аксиом следует истинность теоремы (по известному в логике пра-

вилу Modus Ponens).

Следовательно, достаточным (но вовсе не необходимым) условием истинности теоремы при условии истинности аксиом является общезначимость вышеупомянутой импликации или, что проще установить компьютеру, невыполнимость отрицания этой импликации.

Другими словами, если компьютер докажет невыполнимость

формулы

(Ax1 … AxN Th),

то это будет означать истинность теоремы при условии истинности аксиом.

Очевидное преобразование этой формулы даёт

Ax1 … AxN Th.

Конъюнкцию ППФ, как и раньше, будем трактовать как множество этих формул.

При этом задачу АДТ будем формулировать как задачу доказательства логической несовместимости (внутренней противоречивости) множества, состоящего из аксиом и отрицания теоремы.

Есть ли алгоритмы решения этой задачи? Есть. И одним из лучших является так называемый метод резолюций.

5. Метод резолюций

Метод резолюций стал достоянием общественности в 1965 г., когда в журнале «Journal of the ACM» была опубликована статья Дж. Робинсона «A Machine-Oriented Logic Based on the Resolution Principle» [1].

Идея метода заключается в следующем.

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

Пусть W – множество дизъюнктов, а R(W) – объединение W с множеством всех резольвент, которые могут быть получены из всех пар элементов множества W. Введём следующие обозначения:

По теореме Робинсона множество W является невыполнимым (напомним, что это означает успешное доказательство теоремы) тогда и только тогда, когда для некоторого числа n > 0 множество

Rn(W) содержит пустой дизъюнкт (или, в нотации Хорна, содержит утверждение true false).

На этой теореме основана стратегия АДТ, которая и носит на-

звание «метода резолюций». Это алгоритм, каждый шаг которого – вычисление Rn(W) (n = 1, 2, …).

После очередного шага этого алгоритма может оказаться, что: Rn(W) содержит пустой дизъюнкт (или, в нотации Хорна, ут-

верждение true false), тогда процесс завершается, так как множество W невыполнимо, то есть теорема верна;

Rn(W) = Rn-1(W), тогда процесс тоже завершается, так как множество W не является невыполнимым, то есть теорема неверна.

В противном случае после очередного шага алгоритма процесс продолжается.

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

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

Правило резолюции

Рассмотрим два дизъюнкта не в форме Хорна, а в общем виде:

(1) P1 … Pn1 Q1 … Qm1,

где Pi и Qj – атомарные формулы;

(2) R1 … Rn2 T1 … Tm2,

где Ri и Tj – атомарные формулы.

Каждое логическое «слагаемое» каждого из этих двух выражений называется литералом (слева расположены «отрицательные литералы», а справа – «положительные литералы»).

Может оказаться так, что какой-нибудь отрицательный литерал выражения (1) и какой-нибудь положительный литерал выражения

(2) унифицируются, то есть для них может быть построен так на-

зываемый наиболее общий унификатор (НОУ).

Унификатор – это последовательность подстановок (замен переменных термами или другими переменными в термах двух ато-

17

марных формул), после которых атомарные формулы становятся одинаковыми. НОУ – это, в некотором смысле, «минимальный» из всех унификаторов для двух данных литералов.

Пример 1.5. Рассмотрим два литерала: p(f(X, b), X, g(X), V) и p(Y, a, Z, g(W)).

Один из множества унификаторов – это последовательность подстановок: {Y ← f(X, b), Z ← g(X), X ← a, V ← g(W)}.

НОУ: {Y ← f(a, b), X ← a, Z ← g(a), V ← g(W)}.

После унификации атомарные формулы в обоих литералах ста-

новятся одинаковыми: p(f(a,b), a, g(a), g(W)).

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

Пример 1.6.

Рассмотрим дизъюнкты с литералами из примера 1.5:

(1)q(X, V) p(f(X, b), X, g(X), V),

(2)p(Y, a, Z, g(W)) q(f(Y, Z), W).

Одна из резольвент: q(a, g(W)) q(f(f(a, b), g(a)), W).

Автор предлагает слушателям (читателям) самостоятельно найти другую резольвенту.

Пример 1.7. Рассмотрим аксиомы «Всем людям свойственно ошибаться», «Сократ грек», «Все греки люди» и теорему «Сократу свойственно ошибаться».

Множество аксиом на ЯИП-1П (после преобразования в форму дизъюнктов):

{человек(X) ошибается(X), грек(Сократ),грек(Y) человек(Y)}.

Множество дизъюнктов, в которые преобразуется отрицание теоремы:

грек(Y) человек(Y), ошибается(Сократ)}.

18

Применение правила резолюции удобно изображать с помощью диаграммы – «куста» из трёх вершин и двух дуг (рис. 1.1).

Дизъюнкт1 Дизъюнкт2

Дизъюнкт3 (резольвента)

Рис. 1.1. Графическое представление применения правила резолюции

Используя такие диаграммы, поиск доказательства невыполнимости множества дизъюнктов методом резолюций можно представить в виде графа, пример которого показан на рис. 1.2 – для приведённого выше примера 1.7 «о Сократе, которому свойственно ошибаться».

На «верхнем ярусе» этого графа четыре вершины. Это исходные дизъюнкты, составляющие множество R0(W) = W. На первом шаге алгоритма доказательства невыполнимости этого множества методом резолюций строятся резольвенты, расположенные на «среднем ярусе» графа. Их три и получены они с помощью трёх применений правила резолюции (три «куста» на рисунке). Таким образом, множество R1(W) состоит уже из семи элементов. Второй шаг работы алгоритма даёт ещё три новых дизъюнкта. Они получаются с помощью пяти применений правила резолюции (5 «кустов» на рисунке). Таким образом, множество R2(W) состоит уже из 10 элементов. Оно содержит пустой дизъюнкт. (На рис. 1.2 – вершина с пометкой «nil».) Остальные два «куста» на рисунке не реализуются в описанном выше алгоритме, так как из-за наличия пустого дизъюнкта во множестве R2(W) процесс должен завершиться.

19

человек(X) ошибается(X)

грек(Y) человек(Y)

грек(Сократ)

ошибается(Сократ)

грек(Y) ошибается(Y)

человек(Сократ)

человек(Сократ)

ошибается(Сократ)

nil

грек(Сократ)

Рис. 1.2. Пример доказательства методом резолюций

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

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

6. Стратегия линейной резолюции

Кандидатами на роли участников очередного применения правила резолюции выступают: на роль 1-го участника – дизъюнкт, полученный из отрицания теоремы (а это, как правило, единственный дизъюнкт), или резольвента, полученная на предыдущем

20