% erforsche/3
erforsche(G,T,A) :- explore(G,T,A).

% Bratko Kap 15.3 (Fig. 15.6)
% 
% Procedure		explore( Goal, Trace, Answer )
% 
% finds Answer to a given goal. Trace is a chain of ancestor
% goals and rules. 'explore' tends to find a positivr anwer to a
% question. Answer is 'false' only when all the possibilities have
% been investigated and they all resulted in 'false'.

:- op(900, xfx, '::').  /* : */
:- op(800, xfx, was).
/* :- op(870, fx, if). */
:- op(880, xfx, then).
:- op(880, xfx, '-->').
:- op(550, xfy, or).
:- op(540, xfy, and).
:- op(300, fx, 'derived by').
:- op(600, xfx, from).
:- op(600, xfx, by).

% Program assumes: op(700,xfx,is), op(500,fx,not).
:- op(700,xfx,is).
:- op(500,fx,not).

explore(Goal, Trace, Goal is true was 'found as a fact') :-
  fact :: Goal.

% Assume only one rule about each type of goal

explore(Goal, Trace,
	Goal is TruthValue was 'derived by' RuleName from Answer) :-
  RuleName :: /*if*/ Condition /* then */ -->  Goal,					% Rule relevant to Goal
  explore( Condition, [Goal by RuleName | Trace], Answer),
  truth(Answer, TruthValue).

/* explore(Goal1 and Goal2, Trace, Answer) :- !, */
explore( and(Goal1, Goal2), Trace, Answer) :- !,
  explore(Goal1, Trace, Answer1 ),
  continue(Answer1, and(Goal1 , Goal2), Trace, Answer).

/* explore(Goal1 or Goal2, Trace, Answer) :- */
explore(or(Goal1 , Goal2), Trace, Answer) :-
  exploreyes(Goal1, Trace, Answer)				% Positive answer to Goal1
  ;
  exploreyes(Goal2, Trace, Answer).				% Positive answer to Goal2

/* explore(Goal1 or Goal2, Trace, Answer1 and Answer2) :- !, */
explore(or(Goal1 , Goal2), Trace, and(Answer1,Answer2)) :- !,
  not exploreyes( Goal1, Trace, _ ),
  not exploreyes( Goal2, Trace, _ ),				% No positive answer
  explore( Goal1, Trace, Answer1 ),				% Answer1 must be negative
  explore( Goal2, Trace, Answer2 ).				% Answer2 must be negative

explore( Goal, Trace, Goal is Answer was told ) :-
  useranswer( Goal, Trace, Answer ).				% User supplied answer

exploreyes( Goal, Trace, Answer ) :-
  explore(Goal, Trace, Answer),
  positive(Answer).

/* continue( Answer1, Goal1 and Goal2, Trace, Answer) :- */
continue( Answer1, and(Goal1 , Goal2), Trace, Answer) :-
  positive( Answer1 ),
  explore( Goal2, Trace, Answer2 ),
  ( positive( Answer2 ),
    Answer = and(Answer1 , Answer2)
    ;
    negative(Answer2),
    Answer = Answer2
  ).

/* continue( Answer1, Goal1 and Goal2, _, Answer1) :- */
continue( Answer1, and(Goal1 , Goal2), _, Answer1) :-
  negative(Answer1).

truth( Question is TruthValue was Found, TruthValue) :- !.

/* truth( Answer1 and Answer2, TruthValue) :- */
truth( and(Answer1 , Answer2), TruthValue) :-
  truth(Answer1, true),
  truth(Answer2, true),!,
  TruthValue = true
  ;
  TruthValue = false.

positive(Answer) :-
  truth(Answer, true).

negative(Answer) :-
  truth(Answer, false).