% Computational Intelligence: a logical approach.
% Prolog Code.
% Iterative Deepening Proof for Minimal Explanations in Horn Theorist
% Copyright (c) 1998, Poole, Mackworth, Goebel and Oxford University Press.
% Note that this asserts intermediate clauses and so may need to be reloaded
% between queries.
% `<-' is the object-level `if'
:- op(1150, xfx, <- ).
% `&' is the object level conjunction.
:- op(950,xfy, &).
% explain(G,A) is true if C is a minimal explanation of G.
% an iterative deepening search,
explain(G,A) :-
iprove(G,A,0).
% bhprove(G,Bound,C1,C2) is true if we can prove G given the assumables in C1
% resulting in the assumables in C2, and never exceeding the Bound on the
% number of assumables.
bhprove(true,_,D,D) :- !.
bhprove((A & B),Bnd,C1,C3) :- !,
bhprove(A,Bnd,C1,C2),
bhprove(B,Bnd,C2,C3).
bhprove(G,Bnd,C1,C2) :-
(G <- Body),
bhprove(Body,Bnd,C1,C2).
bhprove(G,_,C,C) :-
member(G,C).
bhprove(G,Bnd,C,[G|C]) :-
\+ member(G,C),
assumable(G),
length(C,LC),
LC < Bnd.
bhprove(G,Bnd,C,_) :-
\+ member(G,C),
assumable(G),
length(C,LC),
LC >= Bnd,
retract(failed(_)),
assert(failed(unnaturally)),
fail.
% iprove(G,A,Bnd) is true if we can prove A is an explanation of G using an
% iterative deepening search, starting from depth Bnd. At each depth we first
% look for nogoods at this depth and then for explanations of G.
iprove(_,_,Bnd) :-
retractall(failed(_)),
assert(failed(naturally)),
bhprove(false,Bnd,[],C),
\+ found(C),
assert(nogood(C)), fail.
iprove(G,A,Bnd) :-
bhprove(G,Bnd,[],A),
\+ found(A),
\+ explfound(G,A),
assert(minexpl(G,A)).
iprove(G,A,B) :-
failed(unnaturally),
B1 is B+1,
iprove(G,A,B1).
% found(C) is true if C has already been found as a conflict. It uses the
% relation nogood(C1) to record what conflicts have been found
:- dynamic nogood/1.
found(C) :-
nogood(C1),
subset(C1,C).
%explfound(G,A) is true if A has already been found as an explanation of G.
% It uses the relation minexpl(G,A1) to record what conflicts have been found
:- dynamic minexpl/2.
explfound(G,A) :-
minexpl(G,A1),
subset(A1,A).
% subset(L1,L2) is true if L1 is a subset of list L2
subset([],_).
subset([A|B],L) :-
member(A,L),
subset(B,L).
% member(X,L) is true if X is a member of list L
member(X,[X|_]).
member(X,[_|L]) :-
member(X,L).