Prolog

          дизъюнкт( С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) => ( а=>с))  ),  пуск.

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

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

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

16. 4.    Заключительные замечания

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

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