Логическое программирование

Правила образования формул

Если $$p$$ — $$k$$ -местный предикатный символ, а $$t_1, t_2\dts t_k$$ — термы, то выражение $$p(t_1, t_2\dts t_k)$$ является формулой (атомарной).

Если $$A$$ и $$B$$ — формулы, то выражения $$[A \ B]$$, $$[A \vee B]$$, $$[A \to B]$$ и $$\neg A$$ являются формулами.

Если $$A$$ — формула, а $$y$$ — переменная, то выражения $$\forall y\,A$$, $$\exists y\,A$$ являются формулами.

Замечания

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

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

Формула, не имеющая переменных со свободными вхождениями, называется предложением.

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

Пример. Пусть нелогическая сигнатура состоит из трех символов $$\{E, M, S\}$$, где $$E$$ — двухместный предикат, $$S$$ — одноместная функция, $$M$$ — двухместная функция, тогда выражение$$\eq*{ \forall z \forall y E (M (S(z), S(y)), S(M (z, y))), }$$ очевидно, будет формулой. Поскольку в этой формуле нет свободных переменных, то она является предложением.

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

$$M(z, y)$$ — точка, являющаяся серединой отрезка $$(z, y)$$,

$$S(z)$$ — точка, симметричная точке $$z$$ относительно некоторой точки,

$$E(z, y)$$ — предикат, означающий равенство точек $$z$$ и $$y$$.

При такой интерпретации нелогических символов $$M, S, E$$, приведенная выше формула есть утверждение о том, что середина отрезка $$(z, y)$$ симметрична середине отрезка с концами, симметричными точкам $$z, y$$.

Очевидно, что это утверждение истинно.

(рис 14.1)

Рассмотрим еще одну интерпретацию нашей сигнатуры. Пусть на этот раз универсумом рассуждения будет множество действительных чисел, исключая число $$0$$:

$$M(z, y)$$ — произведение чисел $$z, y$$,

$$S(z)$$ — число, обратное числу $$z$$,

$$E(z, y)$$ — " $$z = y$$ ".

Рассматриваемая нами формула является теперь утверждением о том, что для любых двух чисел из нашего универсума выполняется равенство$$\eq*{ (z y)^{-1} = z^{-1} y^{-1}. }$$

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

Примеры. Пусть $$P$$ и $$Q$$ — одноместные предикатные символы.

$$\forall x [\neg P(x) \vee P(x)]$$ — тождественно истинная формула.

$$\forall x [\neg P(x) \ P(x)]$$ — тождественно ложная формула.

$$\forall x [P(x) \vee Q(x)]$$ — истинность этой формулы зависит от интерпретации предикатных символов $$P$$ и $$Q$$.

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

Формула называется выполнимой, если она истинна хотя бы при одной интерпретации.

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

Например, формулы

$$\eq*{ \begin{gathered} \forall x [P(x) \vee Q(x)],\\ [\forall x P(x) \vee \forall x Q(x)] \end{gathered} }$$

не являются логически равносильными, а формулы

$$\eq*{ \begin{gathered} \forall x [P(x) \ Q(x)],\\ [\forall x P(x) \ \forall x Q(x)] \end{gathered} }$$

логически равносильны.

Логическую равносильность формул будем обозначать знаком $$\equiv$$, например,$$\eq*{ \forall x\, [P(x) \ Q(x)] \equiv [\forall x\, P(x) \ \forall x Q(x)]. }$$

Заметим, что в этом выражении фигурирует не одна формула, а две, соединенные знаком логической равносильности.

Некоторые сведения из математической логики

Напомним кратко основную цепочку построений математической логики, используемых в логическом программировании. Известно, что любое предложение в логике предикатов логически равносильно предложению в предваренной нормальной форме, то есть в такой форме, когда в начале расположены все ее кванторы, за которыми расположена бескванторная ее часть. Рассмотрим пример такой формулы$$\eq{ \forall x\, \exists z\, \forall y\, \exists u\, \forall v [P(x, y) \ R(y, z) \to S(x, u, v) \ [S(y, u, v) \vee S(z, y, v)]], }$$ где $$P, R, S$$ — предикатные символы соответствующей арности; $$x, y, z, u$$, $$v$$ — индивидные переменные.

Известно, что по любому предложению $$A$$ в предваренной нормальной форме можно построить так называемое сколемовское предложение $$B$$. Для этого избавляются от кванторов существования следующим образом. Пусть ( $$z$$ — самое левое вхождение квантора существования в рассматриваемую формулу и перед ним расположены $$k$$ кванторов общности с переменными $$x_1, x_2\dts x_k$$. Выбираем новый $$k$$ -местный функциональный символ $$f$$, вхождение $$\exists z$$ удаляем из формулы, а каждое вхождение переменной $$z$$ заменяем термом $$f(x_1, x_2\dts x_k)$$. Аналогичным образом избавляемся и от других кванторов существования. В результате получим сколемовскую формулу $$B$$ для исходной формулы $$A$$.

Так, для формулы (1) соответствующая сколемовская формула будет иметь вид$$\forall x\, \forall y\, \forall v [[P(x, y) \ R(y, f(x)) \to \\ \to S(x, g(x, y), v)] \ [S(y, g(x, y), v) \vee S(g(x, y), y, v)]],$$ полученный из (1) заменой $$z$$ на $$f(x)$$, а $$u$$ на $$g(x, y)$$. Заметим, что если бы было $$k = 0$$, то переменная $$z$$ заменялась бы на новую константу. Процесс получения сколемовской формулы по заданной формуле $$A$$ называется сколемизацией.

Известно, что сколемовская формула $$B$$, соответствующая формуле $$A$$, может быть логически неравносильна формуле $$A$$, однако они либо обе выполнимы, либо обе невыполнимы (равносильность по выполнимости). Для иллюстрации этого факта рассмотрим простую формулу$$\eq*{ \forall x\, \exists y R(x, y), }$$ которая интуитивно выражает существование функции $$f$$, такой, что для любого элемента $$x$$ выполняется $$R(x, f(x))$$. При сколемизации она превращается в формулу$$\eq*{ \forall x R(x, f(x)). }$$

Равносильность по выполнимости формулы $$A$$ и соответствующей ей сколемовской формулы $$B$$ может быть использована следующим образом. Предположим, мы хотим доказать, что формула $$C$$ является логическим следствием формул $$A$$ и $$B$$. Это сводится к доказательству невыполнимости формулы$$\eq*{ [A \ B \ \neg C] }$$ или соответствующей ей сколемовской формулы, что технически осуществить оказывается проще.

Поскольку в сколемовской формуле используются только кванторы общности и все они расположены в начале формулы, их обычно опускают, подразумевая по умолчанию их наличие, а бескванторную часть представляют в нормальной конъюнктивной форме. Полученная таким образом формула называется клаузальной. В нашем случае формула (2) превращается в клаузальную формулу$$\eq{ [\neg P(x, y) \vee \neg R(y, f(x)) \vee S(x, g(x, y), v)] \\\ \ [S(y, g(x, y), v) \vee S(g(x, y), y, v)]. }$$

Упомянутый выше метод резолюций основывается на единственном правиле вывода, называемом правилом резолюции, которое заключается в следующем. Из двух формул вида

$$\eq*{ [\neg A \vee B_1 \vee B_2 \vee \ldots \vee B_k] }$$

и

$$\eq*{ [A \vee D_1 \vee D_2 \vee \ldots \vee D_s] }$$

в соответствии с правилом резолюции выводится формула

$$\eq*{ [B_1 \vee B_2 \vee \ldots \vee B_k \vee D_1 \vee D_2 \vee \ldots \vee D_s]. }$$

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

Из математической логики известно, что не существует алгоритма, который по любому множеству $$H$$ формул-гипотез логики предикатов и еще одной формуле $$A$$ отвечал бы на вопрос, является ли $$A$$ логическим следствием множества $$H$$. Однако существует алгоритм, который в случае, когда $$A$$ логически следует из $$H$$, строит доказательство этого факта с использованием правила резолюции, в противном случае алгоритм может работать бесконечно.

Различные версии языка Пролог базируются на использовании так называемых хорновских клаузальных формул. Хорновскими называются формулы, являющиеся дизъюнкциями атомарных формул и/или их отрицаний, причем атомарная часть без отрицания может быть в такой формуле не более чем одна. Рассмотрим пример такой формулы:$$\eq{ R(x, y) \vee \neg P(x) \vee \neg Q(x, z) \vee \neg S(f(y)). }$$ Ее можно представить в виде$$\eq{ P(x) \ Q(x, z) \ S(f(y)) \to R(x, y). }$$ Эта формула воспринимается Прологом так, как если бы все ее переменные были связаны квантором общности. Восстанавливая кванторы, имеем$$\eq{ \forall x \, \forall y \, \forall z [P(x) \ Q(x, z) \ S(f(y)) \to R(x, y)]. }$$ Учитывая, что $$z$$ не входит в правую часть импликации, формулу (6) можно переписать в виде$$\eq*{ \forall x\, \forall y [\exists z [P(x) \ Q(x, z) \ S(f(y))] \to R(x, y)], }$$ изменив область действия квантора $$\exists z$$.

В Прологе принято формулы, аналогичные формуле (5), записывать в виде$$\eq{ R(x, y)\colon\!\!-P(x), Q(x, z), S(f(y)), }$$ меняя местами левую и правую части импликации и вместо знака конъюнкции ставя запятую.

Формулу (7) Пролог воспримет как указание на то, что для доказательства истинности $$R(x, y)$$ надо найти некоторое значение $$z$$ и доказать, что истинны $$P(x)$$, $$Q(x, z)$$, $$S(f(y))$$. Такие формулы принято называть правилами.

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

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

Примеры формальных доказательств

Пример. Вывести из гипотез $$H_1$$, $$H_2$$, $$H_3$$ заключение $$C$$, где$$\eqa*{ H_1\colon \forall x [E(x) \ \neg P(x) \to \exists y[R(x, y) \ D(y)]],\\ H_2\colon \exists x [E(x) \ M(x) \ \forall y[R(x, y) \to M(y)]],\\ H_3\colon \forall x [M(x) \to \neg P(x)],\\ C\colon \exists x [M(x) \ D(x)]. }$$

Префиксная форма:$$\eqa*{ {\rm Pref}(H_1)\colon \forall x \,\exists y [E(x) \ \neg P(x) \to [R(x, y) \ D(y)]],\\ {\rm Pref}(H_2)\colon \exists x \,\forall y [E(x) \ M(x) \ [R(x, y) \to M(y)]],\\ {\rm Pref}(H_3)\colon \forall x [M(x) \to \neg P(x)],\\ {\rm Pref}(C)\colon \exists x [M(x) \ D(x)]. }$$

Сколемовская форма:$$\eqa*{ {\rm Sk}(H_1)\colon \forall x [E(x) \ \neg P(x) \to [R(x, f(x)) \ D(f(x))]],\\ {\rm Sk}(H_2)\colon \forall y [E(a) \ M(a) \ [R(a, y) \to M(y)]],\\ {\rm Sk}(H_3)\colon \forall x [M(x) \to \neg P(x)],\\ {\rm Sk}(\neg C)\colon \forall x [\neg M(x) \vee \neg D(x)]. }$$

Клаузальная форма (опускаем кванторы общности, а бескванторные части приводим к КНФ и из каждого сомножителя получаем клаузу):$$\eqa*{ {\rm Cla}(H_1)\colon [\neg E(x) \vee P(x) \vee R(x, f(x)] \ [\neg E(x) \vee P(x) \vee D(f(x))],\\ {\rm Cla}(H_2)\colon M(a) \ E(a) \ [\neg R(a, y) \vee M(y)],\\ {\rm Cla}(H_3)\colon \neg P(x) \vee \neg M(x),\\ {\rm Cla}(C)\colon \neg M(x) \vee \neg D(x). }$$

Доказательство с использованием правила резолюции:

$$\eqa*{ 1.\ \neg E(x) \vee P(x) \vee R(x, f(x)) \t{— из гипотезы}\ H_1,\\ 2.\ \neg E(x) \vee P(x) \vee D(f(x)) \t{— из гипотезы}\ H_1,\\ 3.\ M(a), \t{— из гипотезы}\ H_2,\\ 4.\ E(a), \t{— из гипотезы}\ H_2,\\ 5.\ \neg R(a, y) \vee M(y), \t{— из гипотезы}\ H_2,\\ 6.\ \neg P(x) \vee \neg M(x), \t{— из гипотезы}\ H_3,\\ 7.\ \neg M(x) \vee \neg D(x), \t{— из заключения}\ C,\\ 8.\ P(a) \vee R(a, f(a)), \t{— из 1, 4 с помощью подстановки}\ (x/a),\\ 9.\ P(a) \vee D(f(a)), \t{— из 2, 4 с помощью подстановки}\ (x/a),\\ 10.\ \neg P(a), \t{— из 3, 6 с помощью подстановки}\ (x/a),\\ 11.\ D(f(a)), \t{— из 9, 10},\\ 12.\ \neg M(f (a)) \t{— из 7, 11 с помощью подстановки}\\ \q (x/f(a)),\\ 13.\ R(a, f(a)), \t{— из 8, 10},\\ 14.\ M(f(a)), \t{— из 5, 13 с помощью подстановки}\\ \q (y/f(a)),\\ 15.\ \square \t{— из 12, 14} }$$

Пример. Рассмотрим предикаты с интерпретацией:$$\eqa*{ F(x, y) \Leftrightarrow x\ \t{является отцом для}\ y,\\ S(x, y) \Leftrightarrow x, y\ \t{— дети одного отца},\\ M(x) \Leftrightarrow x\ \t{— мужчина},\\ B(x, y) \Leftrightarrow x\ \t{брат для}\ y. }$$ В качестве аксиом рассмотрим формулы$$\eqa*{ A_1\colon \forall x\, \forall y [F(x, y) \to M(x)],\\ A_2\colon \forall x\, \forall y \, \forall w [F(x, y) \ F(x, w) \to S(y, w)],\\ A_3\colon \forall x\, \forall y [S(x, y) \ M(x) \to B(x, y)]. }$$ Пусть из интерпретации известны факты$$\eqa*{ A_4\colon F(\t{'Иван'}, \t{'Харитон'}),\\ A_5\colon F(\t{'Иван'}, \t{'Василий'}),\\ A_6\colon F(\t{'Василий'}, \t{'Елена'}). }$$ Вопрос: "Есть ли брат у Харитона?" — на языке предикатов записывается как $$\eq*{ A_7\colon \exists z\, B(z, \t{'Харитон'})? }$$

Доказательство$$\eqa*{ 1.\ \neg F(x, y) \vee M(x) \t{— из формулы}\ A_1,\\ 2.\ \neg F(x, y) \vee \neg F(x, w) \vee S(y, w) \t{— из формулы}\ A_2,\\ 3.\ \neg S(x, y) \vee \neg M(x) \vee B(x, y) \t{— из формулы}\ A_3,\\ 4.\ F(\t{'Иван'}, \t{'Харитон'}) \t{— формула}\ A_4,\\ 5.\ F(\t{'Иван'}, \t{'Василий'}) \t{— формула}\ A_5,\\ 6.\ F(\t{'Василий'}, \t{'Елена'}) \t{— формула}\ A_6,\\ 7.\ \neg B(z, \t{'Харитон'}) \t{— отрицание запроса}\ A_7,\\ 8.\ \neg F(\t{'Иван'}, w) \vee S(\t{'Василий'}, w) \t{— из 2, 5, подстановка}\\ \q (x/\t{'Иван'}, y/\t{'Василий'}),\\ 9.\ S(\t{'Василий'}, \t{'Харитон'}) \t{— из 4, 8, подстановка}\\ \q (w/\t{'Харитон'}),\\ 10.\ M(\t{'Василий'}) \t{— из 6, 1, подстановка}\\ \q (x/\t{'Василий'}, y/\t{'Елена'}),\\ 11.\ \neg S(\t{'Василий'}, y) \vee B(\t{'Василий'}, y) \t{— из 10, 3, подстановка}\\ \q (x/\t{'Василий'}),\\ 12.\ B(\t{'Василий'}, \t{'Харитон'}) \t{— из 9, 11, подстановка}\\ \q (y/\t{'Харитон'}),\\ 13.\ \square \t{— из 12, 7, подстановка}\\ (z/\t{'Василий'}) }$$

Фактически мы не только получили ответ на наш запрос, но и подтвердили его конкретным значением переменной $$z$$. Приведенный вывод можно модифицировать, если ввести предикат $${\rm answer}(z)$$ и вместо цели

$$\eq*{ \t{"}7.\ \neg B(z, \t{'Харитон'})\t{"}\vspace{-1mm} }$$

поставить новую цель

$$\eqa*{ 7'.\ \neg B(z, \t{'Харитон'}) \vee {\rm answer}(z).\ \t{Тогда шаг 13 превратится в 13'}.\\ 13'.\ {\rm answer}(\t{'Василий'})\t{ — из 12, 7', подстановка}\ (z/\t{'Василий'}). }$$

Упражнение

Рассмотрите вывод, в котором первые 7 формул являются посылками. Для остальных формул выпишите пояснения к применению правила резолюции.$$\eqa*{ 1.\ \neg A(z),\\ 2.\ A(x) \vee \neg P(x) \vee \neg Q(x, y),\\ 3.\ A(x) \vee \neg R(y) \vee \neg Q(y, x),\\ 4.\ P(a),\\ 5.\ Q(b, c),\\ 6.\ R(a),\\ 7.\ R(b),\\ 8.\ \neg P(z) \vee \neg Q(z, y),\\ 9.\ \neg Q(a, y),\\ 10.\ \neg R(y) \vee \neg Q(y, z),\\ 11.\ \neg Q(a, z),\\ 12.\ \neg Q(b, z),\\ 13.\ \square }$$

Элементы языка Пролог

Основным элементом языка Пролог является терм. Термы строятся из переменных, атомов, чисел и функторов с использованием круглых скобок.

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

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

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

Функтор синтаксически совпадает с атомом.

Терм — это либо переменная, либо атом, либо число, либо выражение вида$$\eq*{ f(t_1, t_2\dts t_k), }$$ где $$f$$ — функтор, а $$t_1, t_2\dts t_k$$ — термы.

Для некоторых специальных функторов, например знаков арифметических операций, отношений сравнения и других, в Прологе, как в традиционной математике, используется инфиксная форма записи. Например, выражение $$X + 1$$ рассматривается как терм с функтором $$+$$ и двумя аргументами $$X$$ и $$1$$.

Среди термов ввиду особой важности выделяются термы для представления списков. Канонически список представляется двухместным термом, первым аргументом которого является головной элемент списка, а вторым — его хвост, то есть список, полученный из исходного удалением головного элемента. Функтором в такой записи часто используется символ точка. Альтернативным представлением списка является выражение вида $$[t_1, t_2\dts t_k]$$ или $$[t \,|\, L]$$, где $$t$$ — головной элемент, а $$L$$ — хвост списка. Допустимо также выражение вида $$[t_1, t_2\dts t_k \,|\, L]$$.

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

Подстановкой называется набор пар $$\ta = (x_1/t_1, x_2/t_2 \dts x_n/t_n)$$, где $$x_1, x_2\dts x_n$$ — переменные, а $$t_1, t_2\dts t_n$$ — термы.

Через $$E\ta$$ обозначим результат подстановки термов $$t_1, t_2\dts t_n$$ в выражение $$E$$ вместо переменных $$x_1, x_2\dts x_n$$.

Пусть $$\pi = (y_1/u_1, y_2/u_2\dts y_m/u_m)$$ — еще одна подстановка. Композиция $$\ta \pi$$ двух подстановок $$\ta$$ и $$\pi$$ определяется следующим образом:$$\eq*{ E(\ta \pi) = (E \ta)\pi. }$$ Подстановка $$\ta \pi$$ может быть вычислена следующим образом. Составим из подстановок $$\ta$$ и $$\pi$$ последовательность$$\eq*{ (x_1/t_1 \pi, x_2/t_2 \pi \dts x_n/t_n\pi, y_1/u_1, y_2/u_2\dts y_m/u_m) }$$ и проведем следующие две операции:

Если некоторое $$y_i$$ совпадает с некоторым $$x_j$$, то вычеркиваем пару $$y_i/u_i$$.

Если $$t_i \pi = x_i$$, то вычеркиваем пару $$x_i/t_i \pi$$.

Пример. Пусть $$\ta = (x/f(y), y/z),\ \pi = (x/a, y/b, z/y)$$. Рассмотрим последовательность$$\eq*{ (x/f(y) \pi, y/z \pi, x/a, y/b, z/y) = (x/f(b), y/y, x/a, y/b, z/y) }$$ и по первому правилу вычеркиваем пары $$x/a$$ и $$y/b$$, затем по второму правилу — пару $$y/y$$. В результате получим$$\eq*{ \ta \pi = (x/f(b), z/y). }$$

Подстановка $$\ta$$ называется унификатором термов $$E_1$$, $$E_2$$, если $$E_1 \ta = E_2 \ta$$.

Наиболее общим унификатором термов $$E_1$$, $$E_2$$ называется подстановка $$\sigma$$, такая, что любой другой их унификатор $$\ta$$ представляется в виде $$\ta = \sigma \pi$$.

Пример. Для термов $$P(a, y)$$, $$P(x, f(b))$$ унификатором будет подстановка$$\eq*{ (x/a, y/f(b)). }$$ Будет ли она наиболее общим унификатором?

Пример.

Для термов $$P(a, x, f (g(y)))$$ и $$P(z, f(z), f(u))$$ наиболее общим унификатором будет подстановка $$(z/a, x/f(a), u/g(y))$$. Результатом унификации будет терм $$P(a, f(a), f(g(y)))$$