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

Рассмотрим реализацию простой программы автоматического доказательства тео­рем в виде системы, управляемой шаблонами. Эта программа автоматического дока­зательства будет основана на принципе резолюции; он представляет собой один из широко применяемых методов автоматического доказательства теорем. В этом опи­сании мы ограничимся доказательством теорем простой логики высказываний лишь для иллюстрации используемого принципа, хотя описанный механизм резолюции может быть легко расширен для обработки выражений исчисления предикатов пер­вого порядка (логических формул, которые содержат переменные). Дело в том, что сама основная система Prolog представляет собой особую разновидность программы автоматического доказательства теорем на основе принципа резолюции. Задачу дока­зательства теоремы можно определить следующим образом: дана некоторая формула; необходимо показать, что она является теоремой. Это означает, что формула всегда является истинной, независимо от интерпретации символов, которые встречаются в этой формуле. Например, формула

р v ~р

читается как "р или не р" и всегда остается истинной, независимо от значения сим­вола р. В качестве логических операторов будут использоваться следующие символы.

• ~. Отрицание, читается как "not" (не).

• S. Конъюнкция, читается как "and" (и).

• v. Дизъюнкция, читается как "сг" (или).

• =>. Импликация, читается как "implies" (следует из).

Для этих операторов определен такой приоритет, что "not" всегда связывает сильнее всех, за ним следует "and", затем "or" и после этого "implies".

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

Глава23, Метапрограммирование

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

Проиллюстрируем этот принцип на простом примере. Предположим, что перед нами стоит задача доказать, что следующая формула исчисления высказываний яв­ляется теоремой: (а => b) S (Ь => с) => (а => с)

Эта формула читается следующим образом: "если b следует из а и с следует из Ь, то с следует из а".

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

[p i v p j v...) & Iqi v qj v,.,) ь (r i v гг v...) 4...

В этой формуле все символы р, q и г представляют собой простые высказывания или их отрицания. Эта форма называется также формой представления в виде пред­ложений (под предложением здесь подразумевается конструкция, аналогичная про­стому грамматическому предложению в составе сложного), и каждый из ее дизъюнк­тов рассматривается как предложение. Поэтому составной терм (pi v p; v...) также является предложением. В эту форму может быть преобразована любая пропо­зициональная формула (формула исчисления высказываний). Для данной теоремы, рассматриваемой в качестве примера, такое преобразование может быть выполнено, как описано ниже. Сама эта теорема имеет следующий вид:

(а => Ь) ь [Ь =>с) -> [а => с)

Отрицание данной теоремы выглядит таким образом:

-((a =>b) 6 (Ь=>с) -> (а =>сМ

Ниже перечислены известные правила эквивалентности, которые могут приме­няться при преобразовании этой формулы в конъюнктивную нормальную форму.

1. Выражение х=>у эквивалентно -х v у.

2. Выражение --{х v у) эквивалентно ~х & -у.

3. Выражение -{х & у) эквивалентно -х v -у,

4. Выражение ~(~х) эквивалентно х.

Применив правило 1 к рассматриваемой формуле, получим следующее:

- (- [ [а => Ы & (Ь => с)) v (а => с))

С помощью правил 2 и 4 преобразуем формулу в такую форму: {а -> Ь) ь (Ь «о с] 5 ~(а = > с!

Несколько раз воспользовавшись правилом 1, получим: (~а v b) t (-b v с) б -(-a v с)

Применив правило 2, наконец, получим требуемую форму представления в виде предложений:

(-a v Ь) & [~Ь v с) & а & -с

Это предложение состоит из четырех термов: [~а v b), (~b v с), а, --с. Теперь можно приступить к выполнению процесса резолюции.

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

р v y и -р v z

584 Часть II. Применение языка Prolog в области искусственного интеллекта

 

где р - высказывание, a Y и Z - формулы исчисления высказываний. В таком слу­чае этап резолюции, выполненный над этими двумя предложениями, приводит к по­лучению третьего предложения:

Y v 2

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

X И ~Х

Эта форма, безусловно, свидетельствует о противоречии.

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

Рис. 23.5. Доказательство теоремы (a => Ь) i (Ъ => с) => (а "> с) по методу резолюции. Верхняя строка пред­ставляет собой отрицание данной теоремы в форме ис­числения высказываний. Пустое предложение о пижнеп части свидетельствует о том, что отрицание этой тео­ремы приводит к противоречию

В листинге 23.10 показано, как можно реализовать этот процесс; резолюции с по­мощью программы, управляемой шаблонами. Эта программа оперирует с предложе­ниями, внесенными в базу данных. Весь ход осуществления принципа резолюции может быть сформулирован в виде процесса, управляемого шаблонами, как показано ниже.

Если • >•

имеются два предложения, С1 и С2, такие, что Р представляет собой
(дизъюнктивное) подвыражение С1,; 1 ~р • - подвыражение С2,
то "У*' • ^с~"

удалить Р из С1 (получив СА), удалить ~Р из С2 (получив СВ) и ввести в базу данных новое предложение: СА v СЗ

Листинг 23.10, Управляемая шаблонами простая программа для доказательства теорем с помощью метода резолюции

% Следующая директива требуется для некоторых версий Prolog

:- dynamic clause/1, done/3.

Глава 23. Метапрограммирование 585

% Порождающие правила для доказательства теоремы по методу резолюций % Взаимоисключающие предложения

[ clause! X), clause! -X) ] >

[ write['Contradiction found')» stop]. % Удалить истинное предложение

[ clause! С), in(P, С), in(-P, C] ] >

[ retract! C) ]. t

% Упростить предложение

[ clause! С], delete! P, C, CD, in (P, CD ]- >

[ replace! clause! C), clause! CD) ]. % Этап резолюции, частный случай

[ clause! P), clause! С), delete! -Р, С, Cl), net done (Р, С, Р) ] >

[ assert! clause! CD), assert! done [ P, С, Р)) ].

% Этап резолюции, частный случай

[ clause! -P), clause! С), delete! Р, С, CD, not done,- -P, С, Р) ] >

[ assert! clause! CD), assert! done (-P, C, P)) ]. % Этап резолюции, оОщий случай [ clause(Cl), delete I P, Cl, Cft),

clause[C2)_r delete! -P, C2, CB), not done{ C1,C2,P) ] -> [ assert! clause[CA v CB)), assert! done[ Cl, C2, P)) ].

% Последнее правило: процесс резолюции зашел в тупик

[]-- > [ writeCNot contradiction¹), stop].

* delete! P, E, £1) если

% удаление дизъюнктивного подвыражения Р из Е приводит к получению Е1

delete! X, X v Y, Y).

delete! X, Y v X, Y).

deletef X, Y v Z, Y v Zl):-

delete! X, Z, Zl). delete! x, Y v z, Yl v z)

delete! X, Y, YD.

% ini P, E] если Р - дизъюнктивное подвыражение в Е

in! X, X).

in! X, Y):-

delete! X, Y, _).

После оформления соответствующей конструкции на языке, управляемом шабло­нами, получим следующее правило:

[ clause! Cl), delete! P, Cl, CA),

clause! C2), delete! - P, C2, CB) ] >

[ assertz(clause! CA v CB))).

Часть If. Применение языка Prolog в области искусственного интеллекта

Это правило требует небольшой доработки в целях предотвращения возможности повторного выполнения действий над некоторыми предложениями, что может при­вести к созданию новых копий уже существующих предложений. Программа, приве­денная в листинге 23,10, регистрирует в базе данных операции, которые уже были выполнены, вводя в нее такой факт:

done(Cl, С2, Р)

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

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

a v b v -а

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

a v Ь v a

преобразовав его в предложение a v b.

Остается нерешенным вопрос о том, как преобразовать заданную формулу исчис­ления высказываний в форму представления в виде предложений. Эта задача являет­ся несложной, и ее выполняет программа, приведенная в листинге 23.11. Процедура translate(Formula}

преобразует формулу в множество предложений Cl, C2 и т.д. и вводит эти предложе­ния в базу данных, как показано ниже.

clause I CD. clause! C2).

Листинг 23.11. Программа преобразования формулы исчисления высказываний в множество предложений (вводимых в базу данных)

* ... Трансляция '"пропозиционально

s- ор (100, fy, ~). % Отрицание

:- ор(110, xfy, &), % Конъюнкция

:- ор(120, xfy, v). Ч Дизъюнкция

:- ор(130, xfy, ->). % Иыпликаиия

% translate) Formula): транслировать пропозициональную формулу в предложения -л % ввести в Сазу данных каждое полученное в результате предложение С % как clausel С)

translate! FIG;:- h Транслировать конъюнктивную формулу

I, % Красный оператор отсечения

translate(F), translate(G).

translate(Formula):-

transforml Formula, NewFormula), % Этап преовраэования, выполняемый

Ъ над формулой Formula
!, % Красный оператор отсечения

translate(NewForraula).

translate! Formula):- % Дальнейшие преобразования невозможны

assert(clause(Formula)).

% Правила преобразования для сропоэициснальньз; формул

Глава 23. Метапрограммирование

* trans form! Formula]., FormulaZ) если

% Formula2 эквивалентна формуле Formulal, но Ближе к форме представления

к в виде предложений

transform* -1-Х), X).

transform! X => Y, -X v Y).

transform! - (X s YJ, ~X v -Y}.

transform< ~ (X v Y), -X £ -Y).

transform! X S Y v Z, [X v ZJ s IY v Z)) •

transform! X v Y S Z, [X v Y] fi (X v Z)).

transform! X v y, XI V Y):-transform! X, XI).

-

transform! X v Y, X v Yl):-transform! Y, Yl).

X, - XI) x, XI),

transform! -transform!

* Устранитв двойное отрицание
% Устранить импликацию

% Закон де Моргана % Закон де Моргана % Распределительный закон

* Распределительный закон

% Преобразовать подвыражение Ъ Преобразовать подвыражение % Преобразовать подвыражение

Теперь программа автоматического доказательства теорем, управляемая шаблона­ми, может быть вызвана на выполнение с помощью цели run. Итак, чтобы доказать предполагаемую теорему с помощью этих программ, необходимо преобразовать отри­цание этой теоремы в форму представления в виде предложений и приступить к вы­полнению процесса резолюции. Применительно к теореме, рассматриваемой в каче­стве примера, это можно выполнить с помощью следующего вопроса:?- translate! -((a=>b) S (b=>c)=>U=>O) >, run.

Программа в ответ сообщит "Contradiction found" (Обнаружено противоречие), а это означает, что первоначальная формула является теоремой.

Резюме

• В метапрогра.ммах другие программы рассматриваются как данные. Метаин­терпретатор Prolog представляет собой интерпретатор для языка Prolog на языке Prolog.

• Можно легко написать метаинтерпретаторы Prolog, которые вырабатывают трассировки выполнения, формируют деревья доказательства и предоставляют другие дополнительные возможности.

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

 

• Объектно-ориентированная программа состоит ил объектов, которые передают друг другу сообщения. Объекты отвечают на сообщения, вызывая на выполне­ние свои методы. Методы могут быть также унаследованы от других объектов.

• Программа, управляемая шаблонами, представляет собой коллекцию управ­ляемых шаблонами модулей, которые активизируются при обнаружении шаб­лонов, имеющихся в "базе данных". Как системы, управляемые шаблонами, могут рассматриваться и сами программы Prolog, Наиболее естественной была бы параллельная реализация систем, управляемых шаблонами, а при последо­вательной реализации необходимо обеспечить разрешение конфликтов между модулями в конфликтном множестве.

Часть II. Применение языка Prolog в области искусственного интеллекта

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

В этой главе рассматривались следующие понятия:

» метапрограммы, метаинтерпретаторы;

• обобщение на основе объяснения;

• объектно-ориентированное программирование:

• объекты, методы, сообщения;

• наследование методов;

• системы, управляемые шаблонами, архитектура, управляемая шаблонами;

• программирование, управляемое шаблонами;

• модуль, управляемый шаблонами;

• конфликтное множество, разрешение конфликтов;

• доказательство теорем на основе резолюции, принцип резолюции.