Ответы на вопросы “почему?” - это простое средство объяснения, описывающее одну локальную цепочку рассуждений. Следующая программа дополняет программу 4 возможностью объяснения, поясняющего полное доказательство решенного вопроса.
% программа 8
% how(Goal) - объясняет как была доказана цель Goal
how(Goal):-
solve(Goal,Proof),
interpret(Proof).
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).
interpret((ProofA,ProofB)):-!,
interpret(ProofA),
interpret(ProofB).
interpret((A:-'как было сказано')):-!,
nl,write(A),write(' <= как было сказано'),nl.
interpret('не доказуемо'(A)):-!,
nl,write(A),write(' <= не доказуемо'),nl.
interpret(Proof):-
fact(Proof,Fact),
nl,write(Fact),write(' - это факт'),nl.
interpret(Proof):-
rule(Proof,Head,Body,Proof1),
display_rule(rule(Head,Body)),
interpret(Proof1).
fact((Fact:-true),Fact).
rule((Goal:-Proof),Goal,Body,Proof):-
not(Proof=true),
extract_body(Proof,Body).
extract_body((ProofA,ProofB),(BodyA,BodyB)):-
!,
extract_body(ProofA,BodyA),
extract_body(ProofB,BodyB).
extract_body((Goal:-Proof),Goal).
extract_body('не доказуемо'(B),not(B)).
display_rule(rule(A,B)):-
nl,write('Если '),
write_conjunction(B),
write(' то '),
write(A),nl.
write_conjunction((A,B)):-
!,write(A),write(' и '),
write_conjunction(B).
write_conjunction(A):-
write(A),nl.
Основная идея состоит в интерпретации доказательства цели, где доказательство представлено в метаинтерпретаторе программы 4.
Формирование объяснения:
?- how(member(X,[a,b,c])).
member(a, [a,b,c]) - это факт
X = a ;
Если member(b, [b,c])
то member(b, [a,b,c])
member(b, [b,c]) - это факт
X = b ;
Если member(c, [b,c])
то member(c, [a,b,c])
Если member(c, [c])
то member(c, [b,c])
member(c, [c]) - это факт
X = c ;
No
Определим предикат для нахождения факториала.
f(0,1).
f(X,Y):-
X>0,
X1 is X-1,
f(X1,Y1),
Y is X*Y1.
Посмотрим как метаинтерпретатор объяснит, что 2! = 2 :
?- how(f(2,X)).
Если 2 > 0 и 1 is 2 - 1 и f(1, 1) и 2 is 2 * 1
то f(2, 2)
2 > 0 - это факт
1 is 2 - 1 - это факт
Если 1 > 0 и 0 is 1 - 1 и f(0, 1) и 1 is 1 * 1
то f(1, 1)
1 > 0 - это факт
0 is 1 - 1 - это факт
f(0, 1) - это факт
1 is 1 * 1 - это факт
2 is 2 * 1 - это факт
X = 2
Yes
|
Главная
Каталог файлов
