Иван Братко - Программирование на языке Пролог для искусственного интеллекта

call( Усл), % условий

проверить( Остальные).

выполнить( [ стоп] ) :- !. % Прекратить выполнение

выполнить( []) :- % Пустое действие (цикл завершен)

пуск. % Перейти к следующему циклу

выполнить [Д | Остальные] ) :-

саll( Д),

выполнить( Остальные).

заменить( А, В) :- % Заменить в базе данных А на В

retract( A), !,

assert( В).

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

Простой интерпретатор для программ, управляемых образцами, показан на рис. 16.5. Следует признать, что в интерпретаторе допущены значительные упрощения. Так, например, в него заложено чрезвычайно простое и жесткое правило разрешения конфликтов: всегда запускать первый из потенциально активных модулей (в соответствии с тем порядком, в котором модули записаны в программе). Таким образом, программисту предоставлено единственное средство управления процессом интерпретации — он может указать тот или иной порядок следования модулей. Начальное состояние базы данных задается в виде прологовских предложений, записанных в исходной программе. Запуск программы производится при помощи вопроса

?- пуск.

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

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

p v ~ p

и означающее " p или не p ", верно всегда, независимо от смысла утверждения p .

Мы будем использовать в качестве операторов следующие символы:

~ отрицание, читается как "не"

& конъюнкцию, читается как "и"

v дизъюнкцию, читается как "или"

=> импликацию, читается как "следует"

Согласно правилам предпочтения операторов, оператор "не" связывает утверждения сильнее, чем "и", "или" и "следует".

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

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

( а => b ) & ( b => с ) => ( а => с )

Смысл этой формулы таков: если из а следует b и из b следует с , то из а следует с .

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

( р 1 v p 2 v …) & ( q 1 v q 2 v …)

& ( r 1 v r 2 v …) & …

Здесь р i , q i , r i — элементарные утверждения или их отрицания. Конъюнктивная нормальная форма есть конъюнкция членов, называемых дизъюнктами , например ( p 1 v p 2 v …) — это дизъюнкт.

Любую пропозициональную формулу нетрудно преобразовать в такую форму. В нашем случае это делается следующим образом. У нас есть исходная формула

( а => b ) & ( b => с ) => ( а => с )

Ее отрицание имеет вид

~(( а => b ) & ( b => с ) => ( а => с ))

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

(1) x => у эквивалентно ~x v у

(2) ~ ( x v y ) эквивалентно ~x & ~у

(3) ~ ( x & у ) эквивалентно ~x v ~у

(4) ~ ( ~x ) эквивалентно x

Применяя правило 1, получаем

~(~(( a => b ) & ( b => с )) v ( а => с ))

Далее, правила 2 и 4 дают

( а => b ) & ( b => с ) & ~( а => с )

Трижды применив правило 1, получаем

( ~а v b ) & ( ~b v с ) & ~ ( ~а v с )

И наконец, после применения правила 2 получаем искомую конъюнктивную нормальную форму

( ~а v b ) & ( ~b v с ) & а & ~с

состоящую из четырех дизъюнктов. Теперь можно приступить к резолюционному процессу.

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

p v Y и ~p v Z

Шаг резолюции порождает третий дизъюнкт:

Y v Z

Нетрудно показать, что этот дизъюнкт логически следует из тех двух дизъюнктов, из которых он получен. Таким образом, добавив выражение ( Y v Z ) к нашей исходной формуле, мы не изменим ее истинности. Резолюционный процесс порождает новые дизъюнкты. Появление "пустого дизъюнкта" (обычно записываемого как "nil") сигнализирует о противоречии. Действительно, пустой дизъюнкт nil порождается двумя дизъюнктами вида

x и ~x

которые явно противоречат друг другу.

Рис. 16.6. Доказательство теоремы ( а=>b )&( b=>с )=>( a=>с ) методом резолюции. Верхняя строка — отрицание теоремы в конъюнктивной нормальной форме. Пустой дизъюнкт внизу сигнализирует, что отрицание теоремы противоречиво.

На рис. 16.6 показан процесс применения резолюций, начинающийся с отрицания нашей предполагаемой теоремы и заканчивающийся пустым дизъюнктом.

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