Назад | Содержание| Вперёд 16. 3. Простая программа дляавтоматического дока...

Назад | Содержание| Вперёд

16. 3. Простая программа дляавтоматического докаэательства теорем

В настоящем разделе мы реализуем простуюпрограмму для

автоматического доказательства

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

принципе резолюции

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

пропозициональной логики

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

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

р v ~ р

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

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

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

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

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

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

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

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

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

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

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

Прежде чем начать применять процесс резолюции("резолюционный процесс"), необходимопредставить

отрицание нашей формулы внаиболее приспособленной для этого форме. Такойформой является

конъюнктивнаянормальная форма

, имеющая вид

(р₁ v p₂ v ...) & (q₁ v q₂ v ...)

& (r₁ v r₂ v ...) & ...

Здесь р_i, q_i, r_i - элементарные утверждения

илиих отрицания. Конъюнктивная нормальная формаесть конъюнкция членов, называемых

дизъюнктами

,например (

p₁

p₂

v ...) - это дизъюнкт.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

р v Y и ~р v

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

Y v Z

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

x и ~x

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

Рис. 16. 6. Доказательство теоремы (а=>b)&(b=>с)=>(a=>с) методом

резолюции. Верхняя строка - отрицание теоремы вконъюнктивной

нормальной форме. Пустой дизъюнкт внизусигнализирует, что

отрицание теоремы противоречиво.

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

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

если

существуют два таких дизъюнкта С1 и С2, что

P является (дизъюнктивным)подвыражением С1,

а ~Р - подвыражением С2

то

удалить Р из С1 (результат- СА), удалить ~Р

из С2 (результат - СВ) идобавить в базу

данных новый дизъюнкт СА v СВ.

На нашем формальном языке это можно записатьтак:

[ дизъюнкт( С1),удалить( Р, Cl, CA),

дизъюнкт( С2),удалить( ~Р, С2, СВ) ] --->

[ assert( дизъюнкт( СА v СВ) ) ].

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

сделано( Cl, C2, Р)

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

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

a v b v a

в более простое выражение a v b. Другое правило распознает те дизъюнкты,которые всегда истинны, например,

a v b v ~а

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

% Продукционные правила для задачиавтоматического

% доказательства теорем

% Противоречие

[ дизъюнкт( X),дизъзюнкт( ~Х) ] --->

[ write( 'Обнаруженопротиворечие'), стоп].

% Удалить тривиально истинный дизъюнкт

[ дизъюнкт( С),внутри( Р, С), внутри( ~Р, С) ] --->

[ retract( С) ].

% Упростить дизъюнкт

[ дизъюнкт( С),удалить( Р, С, С1), внутри( Р, С1) ] --->

[ заменить( дизъюнкт( С),дизъюнкт( С1) ) ].

% Шаг резолюции, специальный случай

[ дизъюнкт( Р),дизъюнкт( С), удалить( ~Р, С, С1),

not сделано( Р, С, Р) ] --->

[ аssеrt( дизъюнкт( С1)), аssert(сделано( Р, С, Р))].

% Шаг резолюции, специальный случай

[ дизъюнкт( ~Р),дизъюнкт( С), удалить( Р, С, С1),

not сделано( ~Р, С, Р) ] --->

[ assert( дизъюнкт( C1)), аssert(сделано( ~Р, С, Р))].

% Шаг резолюции, общий случай

[ дизъюнкт( С1),удалить( Р, С1, СА),

дизъюнкт( С2),удалить( ~Р, С2, СВ),

not сделано( Cl, C2, Р) ]--->

[ assert( дизъюнкт( СА v СВ) ),

assert( сделано( Cl, C2, Р)) ].

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

[ ] ---> [ write( 'Нетпротиворечия'), стоп ].

% удалить( Р, Е, Е1) означает, получить извыражения Е

% выражение Е1, удалив из него подвыражение Р

удалить( 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).

% внутри( Р, Е) означает Р есть дизъюнктивноеподвыражение

% выражения Е

внутри( X, X).

внутри( X, Y) :-

удалить( X, Y, _ ).

Рис. 16. 7. Программа,управляемая образцами, для

автоматического доказательства теорем.

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

транс( Формула)

транслирует заданную формулу в множестводизъюнктов Cl, C2 и т.д. и записывает ихпри помощи assert в базу данных в видеутверждений

дизъюнкт( С1).

дизъюнкт( С2).

. . .

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

% Преобразование пропозициональной формулыв множество

% дизъюнктов с записью их в базу данных при помощиassert

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

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

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

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

транс( F & G) :- !, % Транслировать конъюнктивную формулу

транс( F),

транс( G).

транс( Формула) :-

тр( Формула, НовФ), !, % Шаг трансформации

транс( НовФ).

транс( Формула) :- %Дальнейшая трансформация невозможна

assert( дизъюнкт( Формула) ).

% Правила трансформаций дляпропозициональных формул

тр( ~( ~Х), X) :- !. % Двойное отрицание

тр( X => Y, ~Х v Y) :- !. %Устранение импликации

тр( ~( X & Y), ~Х v ~Y) :- !. % Закон де Моргана

тр( ~( X v Y), ~Х & ~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), !.

тр( ~Х, ~Х1) :- % Трансформация подвыражения

тр( X, X1).

Рис. 16. 8. Преобразование пропозициональных формул вмножество

дизъюнктов с записью их в базу данных при помощи assert.

?- транс( ~(( а=>b)& ( b=>c) => ( а=>с)) ), пуск.

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

Назад | Содержание| Вперёд

Оглавление