Метаинтерпретатор для построения дерева доказательства, представленный в программе 2, также может быть расширен добавлением специальных предложений для системных целей и отрицания.
% программа 4
solve(true,true):-!.
solve((A,B),(ProofA,ProofB)):-!,
solve(A,ProofA),
solve(B,ProofB).
solve(not(A),'не доказуемо'(A)):-!,
not(solve(A,_)).
solve(A,(A:-Proof)):-
not system(A),
clause(A,B),
solve(B,Proof).
solve(A,(A:-true)):-
system(A),
A.
system(is(_,_)).
system(_=_).
system(_<_).
system(_>_).
system(write(_)).
system(nl).
Интерпретируем сложную цель:
?- solve((member(X,[a,b,c]),not member(X,[c,d])),Y).
X = a
Y = (member(a, [a,b,c]) :- true), 'не доказуемо'(member(a, [c,d])) ;
X = b
Y = (member(b, [a,b,c]) :- (member(b, [b,c]) :- true)), 'не доказуемо'(member(b, [c,d])) ;
No
|
Главная
Каталог файлов
