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

X R – ППФ,

Если t1 и t2 – термы, а f – функциональный символ, то t1 f t2 – терм.

Если t1, …, tn – термы, а f – функциональный символ, то f(t1, …, tn) – терм.

Других термов нет.

Атомарная формула

Каждый предикатный символ есть атомарная формула.

Если t1, …, tn – термы, а p – предикатный символ, то p(t1, …, tn) – атомарная формула.

Других атомарных формул нет.

Правильно построенная формула (ППФ)

Всякая атомарная формула – это ППФ.

Если R – ППФ, то

(R)– ППФ; R – ППФ.

Если R и Q – ППФ, то

R Q – ППФ, R Q – ППФ, R Q – ППФ.

Если R – ППФ, а X – символ переменной, то

X R – ППФ.

Говорят, что переменная X связана соответствующим квантором. ППФ R называют областью действия квантора. Будем считать, что все переменные, входящие в любую ППФ, связаны каким-нибудь квантором, так как свободных (не связанных) переменных в ППФ быть не должно.

Других ППФ нет.

Пример 1.3. Пусть +, –, add – функциональные символы, а number, equal, >, greaterthen – предикатные символы.

Примеры термов:

2002, a + b, –2 + add(2, 0), add(2+3, 1/(5+7)).

Примеры атомарных формул:

number(5), number(banana), equal(X, Y), greaterthen(4, 5), greaterthen(2 + 3, 8 – 4).

Примеры правильно построенных формул (ППФ):

X + 2 > X + 1, add(1, 4) equal add(2, 3),

11

number(апельсин) number(5),

X (number(X) Y(number(Y)greaterthen(Y, X))).

Теперь определим понятие «семантическая интерпретация формулы ЯИП-1П».

Рассмотрим множество Е произвольной природы. Оно может быть конечным или бесконечным, состоящим из реальных объектов (например, студентов и сотрудников нашего института) или/и абстрактных понятий (например, целых положительных чисел). Назовём это множество областью семантической интерпретации.

Разумеется, в указанной области нас, как создателей некоей модели для решения вполне определённого класса задач, будет что-то интересовать, а что-то – нет. Поставим в соответствие каждому интересующему нас объекту области Е уникальный константный символ алфавита создаваемого нами языка – ЯИП-1П. Каждой интересующей нас функции, определённой на объектах области Е и возвращающей объект из этой области, поставим в соответствие функциональный символ нашего языка. А каждому интересующему нас отношению в данной области поставим в соответствие предикатный символ.

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

Истинность атомарной формулы означает, что одним из двух её возможных значений (true или false) является true – истина. Это

имеет место тогда и только тогда, когда соответствующее предикатному символу отношение в области Е существует для объектов, которым соответствуют термы, входящие в эту формулу.

Пример 1.4. Пусть область Е – моя семья. Меня зовут Николай Геннадьевич. Пусть символы Николай, Геннадий, Ирина – константные символы ЯИП-1П. И пусть символ father – предикатный символ. Атомарная формула father(Геннадий, Николай) имеет значение true. Атомарная формула father(Геннадий, Ирина) имеет значение false. (Вы этого

12

не знаете, но отчество моей жены Ирины отличается от моего отчества – она Сергеевна.)

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

А теперь об истинности ППФ с кванторами.

Будем считать, что значением переменной X, содержащейся в ППФ R, может быть любой константный символ (a1, …, an), соответствующий любому объекту (число объектов n может быть и

бесконечным) области семантической интерпретации E. Обозначим данную ППФ как R(X). Отметим, что

истинность формулы X R(X) означает, что формула

R(a1) … R(an) истинна;

истинность формулы X R(X) означает, что формула

R(a1) … R(an) истинна.

Влогическом программировании рассматриваются не любые

ППФ, а только их подмножество, которое включает в себя только

утверждения (или дизъюнкты) Хорна.

3. Утверждения Хорна

Проведём следующие преобразования произвольной ППФ. Сначала избавимся от знаков кванторов.

От кванторов существования можно избавиться методом

Сколема (так называемой сколемизацией). Продемонстрируем этот метод на примере. Рассмотрим формулу X Y greaterthen(Y, X). Её можно заменить формулой X greaterthen(s(X), X).

Здесь переменная Y в исходной формуле формально (не вникая в смысл предиката greaterthen) заменена на абстрактную функцию

s(X), которая называется функцией Сколема. При конкретной ин-

терпретации данного предиката (по его мнемонике) этой функцией могла бы быть s(X) = X + 1.

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

13

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

Теперь избавимся от знаков импликации и раскроем все скобки. С помощью замены формул R Q эквивалентными им по истинности формулами R Q, а также с помощью замены формул(R Q) формулами R Q, а также формул (R Q) формулами R Q по так называемым правилам де Моргана лю-

бую ППФ можно представить в виде конъюнкции дизъюнктов:

D1 … DM, где каждый дизъюнкт Di ( i = 1, …, M) – это

дизъюнкция литералов;

L1 … LN, где каждый литерал Lj ( j = 1, …, N) – это атомарная формула или её отрицание.

Вместо «конъюнкции дизъюнктов» используют термин «множество дизъюнктов», а каждый дизъюнкт называют клозом или утверждением. Итак, любую ППФ ЯИП-1П можно представить в виде множества утверждений. Отдельное утверждение удобно пред-

ставить в следующем виде:

P1 … Pn Q1 … Qm.

Здесь Pi и Qj – атомарные формулы.

Если n = 0 или m = 0, тогда искусственно увеличим эти значения:

Если n = 0, то добавим в формулу слева цепочку true . Тогда

значение n станет равным 1.

Если m = 0, то добавим в формулу справа цепочку false. Тогда значение m станет равным 1.

Полученное выражение преобразуем в следующую форму:

(P1 … Pn) Q1 … Qm,

и, наконец, в форму:

P1 … Pn Q1 … Qm.

Теперь можно определить дизъюнкт (утверждение) Хорна.

Это формула в только что полученном виде, у которой m = 1. Очевидно, что есть три вида таких формул:

1.true Q.

2.P1 … Pn Q.

3.P1 … Pn false.

14

И ещё одно важное замечание. Единственная исходная ППФ превращается в несколько дизъюнктов (утверждений). При этом может оказаться, что одна и та же переменная (иначе, переменная, связанная одним квантором) присутствует в разных утверждениях. Это означает, что утверждения не являются независимыми! В дальнейшем (в языке Пролог) такой зависимости утверждений быть не должно. Это ещё одно ограничение, которое накладывается на класс логических формул, используемых в логическом программировании.

4. Автоматическое доказательство теорем

Автоматическое доказательство теорем (АДТ) – это логи-

ческий вывод истинности теоремы из истинности множества аксиом, производимый компьютером без участия человека. Разумеется, что как теорема, так и аксиомы представляют собой ППФ ЯИП-1П.

Возникает естественный вопрос: «Как компьютер может проверять истинность логических формул, – ведь ему неведома их семантика?» Оказывается, что для решения данной задачи, как будет видно из дальнейшего, не нужно обращаться к семантической интерпретации аксиом и теоремы! Вместо понятий истинности и ложности ППФ нам понадобятся другие понятия: общезначимости

и невыполнимости.

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

Невыполнимость формулы – это ложность этой формулы при любой семантической интерпретации.

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

Формально постановка задачи АДТ следующая.

Пусть Ax1, …, AxN – аксиомы (ППФ ЯИП-1П), а Th – теорема (тоже ППФ на том же языке).

Рассмотрим импликацию: Ax1 … AxN Th. Допустим, что эта формула общезначима. Тогда из её истинности при данной семантической интерпретации (в частном случае) и из истинности

15

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

вилу 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. Введём следующие обозначения:

R0(W) = W;	Rk+1(W) = R(Rk(W)) (k = 0, 1, …).
	16

По теореме Робинсона множество 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)}.

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

{ ошибается(Сократ)}.
Объединение указанных множеств:
{ человек(X) ошибается(X),	грек(Сократ),

грек(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