Простая программа автоматического доказательства теорем, реализованная в виде программы, управляемой шаблонами
Рассмотрим реализацию простой программы автоматического доказательства теорем в виде системы, управляемой шаблонами. Эта программа автоматического доказательства будет основана на принципе резолюции; он представляет собой один из широко применяемых методов автоматического доказательства теорем. В этом описании мы ограничимся доказательством теорем простой логики высказываний лишь для иллюстрации используемого принципа, хотя описанный механизм резолюции может быть легко расширен для обработки выражений исчисления предикатов первого порядка (логических формул, которые содержат переменные). Дело в том, что сама основная система 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 contradiction1), 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 в области искусственного интеллекта
В данной главе реализован простой интерпретатор для программ, управляемых шаблонами, и применен для автоматического доказательства теорем логики высказываний по методу резолюции.
В этой главе рассматривались следующие понятия:
» метапрограммы, метаинтерпретаторы;
• обобщение на основе объяснения;
• объектно-ориентированное программирование:
• объекты, методы, сообщения;
• наследование методов;
• системы, управляемые шаблонами, архитектура, управляемая шаблонами;
• программирование, управляемое шаблонами;
• модуль, управляемый шаблонами;
• конфликтное множество, разрешение конфликтов;
• доказательство теорем на основе резолюции, принцип резолюции.