% Computational Intelligence: a logical approach.
% Prolog Code.
% Iterative-deepening Definite Clause Interpreter (Appendix C.2, page 502)
% 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, &).
% iprove(G) is true if we can prove G using
% iterative deepening search
iprove(G) :-
iprove_from(G,1).
% bprove(G,Bound,CL1,CL2) is true if we can prove G
% with a proof tree of depth less than Bound where
% CL1 is the closest that we came to the bound before
% proving G, and CL2 is the closest we came to the
% bound after proving G.
bprove(true,Bnd,In,Out) :- !,
min(Bnd,In,Out).
bprove((A&B),Bnd,C1,C3) :- !,
bprove(A,Bnd,C1,C2),
bprove(B,Bnd,C2,C3).
bprove(G,Bnd,C1,C2) :-
Bnd > 1, !,
B1 is Bnd-1,
(G <- Body),
bprove(Body,B1,C1,C2).
bprove(_,1,_,_) :-
retract(failed(naturally)),
assert(failed(unnaturally)),
fail.
% iprove_from(G,Bnd) is true if we can prove G using
% an iterative deepening search, starting from depth
% Bnd. We succeed if there is a number, such that
% iprove previously failed unnaturally, such that
% bprove can prove G, getting within one of the depth
% of the previous search (so it must have failed for
% the previous iteration).
iprove_from(G,Bnd) :-
retractall(failed(_)),
assert(failed(naturally)),
bprove(G,Bnd,Bnd,1).
iprove_from(G,B) :-
failed(unnaturally),
B1 is B+1,
iprove_from(G,B1).
% cleanup needs to be done between proofs so the
% proofs do not interfere with each other.
cleanup :-
retractall(failed(_)).