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




Программа, управляемая образцами, для автоматического доказательства теорем.



  Программа, управляемая образцами, для
автоматического доказательства теорем.

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

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

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

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

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

line();

% Преобразование пропозициональной формулы в множество
% дизъюнктов с записью их в базу данных при помощи 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).

line();









Начало  Назад  Вперед