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

Если 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