% Computational Intelligence: a logical approach.
% Prolog Code.
% Meta-interpreter for traversing proof trees (Appendix C.2)
% Copyright (c) 1998, Poole, Mackworth, Goebel and Oxford University Press.
% <- is the object-level `if'
:- op(1150, xfx, <- ).
% `&' is the object level conjunction.
:- op(950,xfy, &).
% show(G) means prove goal G and show how it was proved
show(G) :-
solve(G,T),
traverse(T).
% solve(Goal,Tree) is true if Tree is a proof tree for Goal
solve(true,true).
solve((A&B),(AT&BT)) :-
solve(A,AT),
solve(B,BT).
solve(H,if(H,builtin)) :-
builtin(H),
call(H).
solve(H,if(H,BT)) :-
( H <- B ),
solve(B,BT).
% builtin(G) is true if goal G is defined in Prolog
% (as opposed to being defined by rules in the
% object-level knowledge base.)
builtin((_ is _)).
builtin((_ =< _)).
builtin((_ >= _)).
builtin((_ = _)).
builtin((_ < _)).
builtin((_ > _)).
% traverse(T) true if T is a tree being traversed
traverse(if(H,true)) :-
!, % no other rules are applicable
writeln([H,' is a fact']).
traverse(if(H,builtin)) :-
!, % no other rules are applicable
writeln([H,' is built-in.']).
traverse(if(H,B)) :-
B \== true,
B \== builtin,
writeln([H,' :-']),
print_body(B,1,Max),
read(Comm),
interpret_command(Comm,B,Max,if(H,B)).
% print_body(B,N1,N2) is true if B is a body to be
% printed and N1 is the count of atoms before B
% N2 is the count after
print_body(true,N,N) :-
!. % no other rules are applicable
print_body((A&B),N1,N3) :-
!, % no other rules are applicable
print_body(A,N1,N2),
print_body(B,N2,N3).
print_body(if(H,_),N,N1) :-
writeln([' ',N,': ',H]),
N1 is N+1.
% interpret_command(Comm,B,Max,G) interprets the
% command Comm on body B where Max is the number of
% conjunctions in the body and G is the goal
interpret_command(N,B,Max,G) :-
integer(N),
N > 0,
N =< Max,
!, % no other rules are applicable
nths(B,N,E),
traverse(E),
traverse(G).
interpret_command(N,_,Max,G) :-
integer(N),
!, % no other rules are applicable
(N < 1 ; N > Max),
writeln(['Number out of range: ',N]),
traverse(G).
interpret_command(up,_,_,_) :-
!. % no other rules are applicable
interpret_command(C,_,_,G) :-
C \== retry,
writeln(['Give either a number, up or retry.']),
traverse(G).
% note that interpret_command(retry,_,_,_) fails.
% nths(S,N,E) is true if E is the N-th element of
% conjunction S. This assumes that `&' is left associated.
nths(A,1,A) :-
\+ (A = (_&_)).
nths((A&_),1,A).
nths((_&B),N,E) :-
N>1,
N1 is N-1,
nths(B,N1,E).