Простая программа для автоматического доказательства теорем
В настоящем разделе мы реализуем простую программу для автоматического доказательства теорем в виде системы, управляемой образцами. Эта программа будет основана на принципе резолюции — популярном методе, обычно используемом в машинном доказательстве теорем. Мы ограничимся случаем пропозициональной логики , поскольку нашей целью будет дать всего лишь простую иллюстрацию используемого принципа. На самом деле, принцип резолюции можно легко обобщить на случай исчисления высказываний первого порядка (с применением логических формул, содержащих переменные). Базовый Пролог можно рассматривать как частный случай системы доказательства теорем, основанной на принципе резолюции.
Задачу доказательства теорем можно сформулировать так: дана формула, необходимо показать, что эта формула является теоремой, т.е. она верна всегда, независимо от интерпретации встречающихся в ней символов. Например, утверждение, записанное в виде формулы
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 , qi , ri — элементарные утверждения или их отрицания. Конъюнктивная нормальная форма есть конъюнкция членов, называемых дизъюнктами , например (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 мы видим, как резолюционный процесс можно сформулировать в форме программы, управляемой образцами. Программа работает с дизъюнктами, записанными в базе данных. В терминах образцов принцип резолюции формулируется следующим образом:
если
существуют два таких дизъюнкта C1 и C2 , что P является (дизъюнктивным) подвыражением C1 , а ~P — подвыражением C2
|
|
|
то
удалить P из C1 (результат — CA ), удалить ~P из C2 (результат — CB ) и добавить в базу данных новый дизъюнкт CA v CB .
На нашем формальном языке это можно записать так:
[ дизъюнкт( C1), удалить( P, C1, CA),
дизъюнкт( C2), удалить( ~P, C2, CB) ] --->
[ assert( дизъюнкт( СА v СВ) ) ].
Это правило нуждается в небольшой доработке. Дело в том, что мы не должны допускать повторных взаимодействий между дизъюнктами, так как они порождают новые копии уже существующих формул. Для этого в программе рис. 16.7 предусматривается запись в базу данных информации об уже произведенных взаимодействиях в форме утверждений вида
сделано( C1, C2, P)
В условных частях правил производится распознавание подобных утверждений и обход соответствующих повторных действий.
Правила, показанные на рис. 16.7, предусматривают также обработку специальных случаев, в которых требуется избежать явного представления пустого дизъюнкта. Кроме того, имеются два правила для упрощения дизъюнктов. Одно из них убирает избыточные подвыражения. Например, это правило превращает выражение
a v b v a
в более простое выражение a v b . Другое правило распознает те дизъюнкты, которые всегда истинны, например,
a v b v ~а
и удаляет их из базы данных, поскольку они бесполезны при поиске противоречия.
% Продукционные правила для задачи автоматического
% доказательства теорем
% Противоречие
[ дизъюнкт( X), дизъзюнкт( ~X) ] --->
[ write( 'Обнаружено противоречие'), стоп].
% Удалить тривиально истинный дизъюнкт
[ дизъюнкт( С), внутри( P, С), внутри( ~P, С) ] --->
[ retract( С) ].
% Упростить дизъюнкт
[ дизъюнкт( С), удалить( P, С, C1), внутри( P, C1) ] --->
[ заменить( дизъюнкт( С), дизъюнкт( C1) ) ].
% Шаг резолюции, специальный случай
[ дизъюнкт( P), дизъюнкт( С), удалить( ~P, С, C1),
not сделано( P, С, P) ] --->
[ аssеrt( дизъюнкт( C1)), аssert( сделано( P, С, P))].
% Шаг резолюции, специальный случай
[ дизъюнкт( ~P), дизъюнкт( С), удалить( P, С, C1),
not сделано( ~P, С, P) ] --->
[ assert( дизъюнкт( C1)), аssert( сделано( ~P, С, P))].
% Шаг резолюции, общий случай
[ дизъюнкт( C1), удалить( P, C1, CA),
дизъюнкт( C2), удалить( ~P, C2, CB),
not сделано( C1, C2, P) ] --->
[ assert( дизъюнкт( CA v CB) ),
assert( сделано( C1, C2, P) ) ].
% Последнее правило: тупик
[] ---> [ write( 'Нет противоречия'), стоп ].
% удалить( P, E, E1) означает, получить из выражения E
% выражение E1, удалив из него подвыражение P
удалить( X, X v Y, Y).
удалить( X, Y v X, Y).
удалить( X, Y v Z, Y v Z1) :-
удалить( X, Z, Z1).
удалить( X, Y v Z, Y1 v Z) :-
удалить( X, Y, Y1).
% внутри( P, E) означает P есть дизъюнктивное подвыражение
% выражения E
внутри( X, X).
внутри( X, Y) :-
удалить( X, Y, _ ).
Рис. 16.7. Программа, управляемая образцами, для автоматического доказательства теорем.
Остается еще один вопрос: как преобразовать заданную пропозициональную формулу в конъюнктивную нормальную форму? Это несложное преобразование выполняется с помощью программы, показанной на рис. 16.8. Процедура
транс( Формула)
транслирует заданную формулу в множество дизъюнктов C1, C2 и т.д. и записывает их при помощи assert в базу данных в виде утверждений
дизъюнкт( C1).
дизъюнкт( C2).
...
Программа, управляемая образцами, для автоматического доказательства теорем запускается при помощи цели пуск. Таким образом, для того чтобы доказать при помощи этой программы некоторую теорему, мы транслируем ее отрицание в конъюнктивную нормальную форму, а затем запускаем резолюционный процесс. В нашем примере это можно сделать так:
?- транс(~(( а=>b) & ( b=>c) => ( а=>с)) ), пуск.
Ответ программы "Обнаружено противоречие" будет означать, что исходная формула является теоремой.
% Преобразование пропозициональной формулы в множество
% дизъюнктов с записью их в базу данных при помощи assert
:- op( 100, fy, ~). % Отрицание
:- op( 110, xfy, &). % Конъюнкция
:- op( 120, xfy, v). % Дизъюнкция
:- op( 130, xfy, =>). % Импликация
транс( F & G) :- !, % Транслировать конъюнктивную формулу
транс( F),
транс( G).
транс( Формула) :-
тр( Формула, НовФ), !, % Шаг трансформации
транс( НовФ).
транс( Формула) :- % Дальнейшая трансформация невозможна
assert( дизъюнкт( Формула) ).
% Правила трансформаций для пропозициональных формул
тр( ~( ~X), X) :- !. % Двойное отрицание
тр( X => Y, ~X v Y) :- !. % Устранение импликации
тр( ~( X & Y), ~X v ~Y) :- !. % Закон де Моргана
тр( ~( X v Y), ~X & ~Y) :- !. % Закон де Моргана
тр( X & Y v Z, (X v Z) & (Y v Z) ) :- !.
% Распределительный закон
тр( X v Y & Z, (X v Y) & (X v Z) ) :- !.
% Распределительный закон
тр( X v Y, X1 v Y) :- % Трансформация подвыражения
тр( X, X1), !.
тр( X v Y, X v Y1) :- % Трансформация подвыражения
тр( Y, Y1), !.
тр( ~X, ~Х1) :- % Трансформация подвыражения
тр( X, X1).
Рис. 16.8. Преобразование пропозициональных формул в множество дизъюнктов с записью их в базу данных при помощи assert.
Заключительные замечания
Нашего простого интерпретатора было вполне достаточно для того, чтобы проиллюстрировать некоторые идеи, лежащие в основе программирования в терминах образцов. Применение этого интерпретатора для более сложных приложений потребовало бы его доработки в целом ряде направлений. Ниже приводится несколько критических замечаний, а также ряд конкретных предложений по усовершенствованию алгоритма интерпретации.
Задача разрешения конфликтов была сведена в нашем интерпретаторе к введению заранее заданного фиксированного порядка рассмотрения модулей. Часто возникает необходимость в более гибких механизмах. Для обеспечения более тонкого управления интерпретацией следует подавать все обнаруженные потенциально активные модули на вход специального управляющего модуля, запрограммированного пользователем.
Когда база данных велика, а программа содержит большое количество модулей, процесс сопоставления с образцами становится крайне неэффективным. Неэффективность можно уменьшить, усложнив организацию базы данных. В частности, можно ввести индексирование информации, записанной в базе данных, или разбить эту информацию на отдельные "подбазы данных", или же разбить все множество модулей на отдельные подмножества. Идея разбиения — в каждый момент дать доступ только к некоторому подмножеству базы данных или набора модулей, ограничив тем самым сопоставление образцов только этим подмножеством. Разумеется, в этом случае механизм управления должен усложниться, поскольку он должен будет обеспечить переход от одних подмножеств к другим с целью их активизации либо деактивизации. Для этого можно применить специальные метаправила.
К сожалению, наш интерпретатор запрограммирован таким образом, что он блокирует механизм автоматических возвратов, так как для манипулирования базой данных он использует процедуры assert и retract. Это положение можно исправить, применив другой способ реализации базы данных, не требующий обращения к этим встроенным процедурам. Например, все состоять базы данных можно представить одним прологовским термом, передаваемым в процедуру пуск в качестве аргумента. Простейший способ реализации этой идеи — организовать этот терм в виде списка объектов базы данных. Тогда верхний уровень базы данных примет вид:
пуск( Состояние) :-
Условие ---> Действие,
проверить( Условие, Состояние),
выполнить( Действие, Состояние).
Задача процедуры выполнить — получить новое состояние базы данных и обратиться к процедуре пуск, подав на ее вход это новое состояние.
Проект
Запрограммируйте интерпретатор, который, в соответствии с приведенным выше замечанием, реализует базу данных как аргумент пусковой процедуры и не использует для этого внутренней базы данных пролог-системы (т.е. обходится без assert и retract). Эта новая версия интерпретатора будет допускать автоматические возвраты. Попытайтесь разработать такое представление базы данных, которое облегчало бы сопоставление с образцами.
Резюме
• Архитектура, ориентированная на типовые конфигурации (образцы), хорошо приспособлена для решения многих задач искусственного интеллекта.
• Программа, управляемая образцами, состоит из модулей, запускаемых при возникновении в базе данных тех или иных конфигураций.
• Прологовские программы можно рассматривать как частный случай систем, управляемых образцами.
• Параллельная реализация — наиболее естественный способ реализации систем, управляемых образцами. Реализация на последовательной машине требует разрешения конфликтов между модулями, содержащимися в конфликтном множестве.
• В этой главе был реализован простой интерпретатор для программ, управляемых образцами. Он был затем применен к задаче автоматического доказательства теорем пропозициональной логики.
• Были рассмотрены следующие понятия:
системы, управляемые образцами
архитектуры, ориентированные на образцы
программирование в терминах образцов
модули, управляемые образцами
конфликтное множество, разрешение конфликтов
принцип резолюции
автоматическое доказательство теорем на основе принципа резолюции
Литература
Waterman and Hayes-Roth (1978) — классическая книга по системам, управляемым образцами. В книге Nilsson (1980) можно найти фундаментальные понятия, относящиеся к задаче автоматического доказательства теорем, включая алгоритм преобразования логических формул в конъюнктивную нормальную форму. Прологовская программа для выполнения этого преобразования приведена в Clocksin and Mellish (1981).
Clocksin F. W. and Mellish С S. (1981). Programming in Prolog. Springer-Verlag. [Имеется перевод: Клоксин У., Мелиш К. Программирование на языке Пролог. — М.: Мир, 1987.]
Nilsson N. J. (1980). Principles of Artificial Intelligence. Tioga; Springer-Verlag.
Waterman D. A. and Hayes-Roth F. (1978, eds). Pattern-Directed Inference Systems. Academic Press.
Дата добавления: 2018-05-01; просмотров: 541; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!