и записывает их при помощи

Процедура

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

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

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

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

        . . .

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

line();

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

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

        :- ор( 100, fy, ~).

                                        % Отрицание

        :- ор( 110, xfy, &).

                                     % Конъюнкция

        :- ор( 120, xfy, v).

                                      % Дизъюнкция

        :- ор( 130, xfy, =>).

                                    % Импликация


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

---

Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий

---

---

---