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



              

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



  Доказательство теоремы  (а=>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   ~а

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

line();

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

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

        [ дизъюнкт( 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, _ ).

line();









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