Простым примером использования метаинтерпретатора являетсяпостроение дерева доказательства в процессе решения определенной цели. Дерево доказательства полезно для средств объяснения в экспертных системах.
% программа 2
solve(true,true):-!.
solve((A,B),(ProofA,ProofB)):-
solve(A,ProofA),
solve(B,ProofB).
solve(A,(A:-Proof)):-
clause(A,B),
solve(B,Proof).
Основным отношением метаинтерпретатора является отношение solve(Goal,Tree), где Tree - дерево доказательства для решения цели Goal .
Дерево доказательства представляется структурой Goal:-Proof, где Proof - конъюнкция ветвей (подцелей) доказываемой цели Goal. Программа 2, реализующая предикат solve/2, является простым расширением программы 1. Три её предложения точно соответствуют трем предложениям метаинтерпретатора для чистого Пролога.
Факт solve утверждает, что пустая цель истинна и имеет тривиальное дерево доказательства, представляемое атомом true. Во втором предложении утверждается, что дерево доказательства конъюнктивной цели (A,B) представляет собой конъюнкцию деревьев доказательства целей A и B. Последнее предложение solve строит дерево доказательства A:-Proof для цели A, в котором Proof строится рекурсивно при решении тела предложения, используемого для редукции цели A.
Рассмотрим пример использования программы 2 для интерпретации предиката member:
?- solve(member(X,[a,b,c]),P).
P = member(a, [a,b,c]) :- true
X = a ;
P = member(b, [a,b,c]) :- (member(b, [b,c]) :- true)
X = b ;
P = member(c, [a,b,c]) :- (member(c, [b,c]) :- (member(c, [c]) :- true))
X = c ;
No
|