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




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


        тр( 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();

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

        ?-  транс( ~(( а=>b) & ( b=>c) => ( а=>с))  ),  пуск.

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

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




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