Программа управляемая образцами для автоматического доказательства теорем
Рисунок 16. 7. Программа, управляемая образцами, для
автоматического доказательства теорем.
Остается еще один вопрос: как преобразовать заданную пропозициональную формулу в конъюнктивную нормальную форму? Это несложное преобразование выполняется с помощью программы, показанной на Рисунок 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).
