%*****************************************************
% Simple Meta Interpreter
%
%  Attempts to prove a goal from a given set of facts.
%
%*****************************************************

%==========================================================
% Program: Prove
%   Try to prove a Goal in a given Agent's belief space.
%==========================================================

%-------------------------------------------------------
%If Goal has a BODY (derivation) then use it.
%
% 	Body of goal is assumed to be a set of facts.
% 	But what if the elements of Body are rule heads?
%		This simple interpreter can NOT handle that.
%	Assumes rules are expressed in terms of facts only.
%-------------------------------------------------------
prove(Goal,Agent) :-
      beliefs(Agent,Bs),         % "Get" Agent's belief space.
      clause(Goal,Body),         % "Get" goal's body.
      checkFactsIn(Body,Bs).     % Assumes body is just made-up of only facts!!


%-------------------------------------------------------
%If Goal has no BODY (derivation) assume
%   it is a fact and try to prove it explicitly.
%-------------------------------------------------------
prove(Goal,Agent) :- 
     \+(clause(Goal,Body)),
     beliefs(Agent,Bs),		%Gets all of agent's beliefs.
     checkFactIn(Goal,Bs).



%==========================================================
% Program: Check Facts In
%
% Check all Facts for their validity in a given belief space.
%==========================================================

checkFactsIn((Fact, Rest),Bs) :-
       checkFactIn(Fact,Bs),!,
       checkFactsIn(Rest,Bs).

checkFactsIn(Fact,Bs) :-
     checkFactIn(Fact,Bs),!.

checkFactsIn(Facts,Bs) :- fail.     


%==========================================================
% Program: Check Fact In
%
% Given A Fact and a set of beliefs (i.e., a belief space).
%   Check to see if the Fact is considered true in
%   the belief space.
%==========================================================

%-----------------------------------------------
% A Fact is FALSE in a given belief space if its 
%     negation is present.
%-----------------------------------------------
checkFactIn(Fact,Bs) :-
    negate(Fact,NegFact),
    member(NegFact,Bs),!,
    fail.

%-------------------------------------
% A Fact is TRUE in a given belief space 
%   if it is explicitly present.
%-------------------------------------
checkFactIn(Fact,Bs) :-
    member(Fact,Bs),!.

%-------------------------------------
% If neither a Fact nor its Negation is in
%   a given belief space it is considered false.
%-------------------------------------
checkFactIn(Fact,Bs) :- fail.