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




Простая программа для автоматического докаэательства теорем - часть 8


Процедура

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

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

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

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

line();

% Преобразование пропозициональной формулы в множество
% дизъюнктов с записью их в базу данных при помощи assert

        :- ор( 100, fy, ~).                                         % Отрицание
        :- ор( 110, xfy, &).                                      % Конъюнкция
        :- ор( 120, xfy, v).                                       % Дизъюнкция
        :- ор( 130, xfy, =>).                                     % Импликация




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