/**************************************************************************

Based on G&N Chapter 4, Problem 5, Page 93.

Vic has been murdered, and Art, Bert, and Carl are suspects.
Art says that he did not do it. He says that Bert was the 
victim's friend but that Carl hated the victim. Bert says
he was out of town the day of the murder, and besides he didn't even
know the guy. Carl says he is innocent and he saw art and bert with the 
victim just before the murder. 

Assuming that everyone- excpet possibly for the murderer- is telling the truth, build
a reasoning system in Prolog and use it to solve the crime.

***************************************************************************/



%:- ensure_loaded('murder_mystery_project.pj').



%******************************************
% Detective's Reasoning Strategy
%******************************************
% 1. Only one person is lying. 
% 2. Pick a suspect and Assume his/her story is true. This is the "prime" suspect.
% 3. Try to prove the other suspects' statments given these assumptions.
% 	If the other suspect's statements contradict with the Prime suspects one of them is lying. 
% 4. IF there are inconsistencies with ALL other suspects, THEN the prime suspect is
%    the liar and hence the murder (since ALL others can't be lying see 1).
%
% Remember the strategy only works if there is only
%   one suspect lying.


%******************************************
% Top-Down Design
%******************************************

%=====================
% MURDERER(Prime)
%=====================
%        1) Collect all suspects in list Ss
%        2) Non-Deterministically Choose a Prime suspect, Prime
%        3) Create list of all other suspects (exclude the Prime Suspect)
%        4) Collect those suspects whose stories don't jibe with Prime's
%                    --- use testPrimeSuspect
%        5) If ALL other suspects stories don't jibe with Prime then we've got him. 
%             Its Prime. Need not look any further.
%              5a) Then Output the Solution.
%              5b) Else Backtrack and try another suspect.


%--------------------------------------------------------------
% Program: murderer
%
% Finds the murderer based on 'Detective's Strategy' given above.
%--------------------------------------------------------------
murderer(P) :-
    allSuspects(Ss),       	       %Collect all the suspects in Ss                  
    suspect(P),                        %Choose one suspect P - The Prime Suspect               
    remove(P,Ss,OtherSuspects),        %Separate P from other suspects.
    setof(L,testPrimeSuspect(P,L),Ls), %Collect in Ls all other suspects whose stories are inconsisten with Ps  
    setEqual(Ls,OtherSuspects),        %Is P's stories inconsistent with ALL other suspect's stories?
    !,                                 %  IF so the program is done else program will backtrack to test another suspect            
    nl,nl,writeseqnl(['The Crime is Solved:',P,'DID IT!']),nl.


%================================
% TESTPRIMESUSPECT(Prime,Other)
%================================
%  1) Non-Deterministically Choose another suspect,OTHER, (other than Prime).
%  2) Try to SUBSTANTIATE the beliefs of OTHER assuming Prime's beliefs are true
%  3) Succeed if OTHER's beliefs are inconsistent with Prime's. One of them is lying.
%  4) Fail otherwise.
%
%   testPrimeSuspect will pair PRIME with every other suspect whose 
%    story is inconsistent with Prime's.
%


%--------------------------------------------------------------
% Program: testPrimeSuspect
%
% Succeeds for each suspect whose beliefs 
%   are found inconsistent with Prime Suspects beliefs.
%--------------------------------------------------------------
testPrimeSuspect(Prime,OtherSuspect) :-
    anotherSuspect(Prime,OtherSuspect),
    inconsistent(OtherSuspect,Prime).


%=====================================
% Program: allSuspects
%
%   Collects all suspects in a list.
%=====================================
allSuspects(Ss) :- findall(S,suspect(S),Ss).


%=====================================
% Program: anotherSuspect
%
% Given a suspect, finds another suspect that is NOT
%  the same one.
%=====================================
anotherSuspect(S,O) :-
     suspect(O), 	% find one
     \+(=(O,S)). 	% ensure not the same one.



%======================================================
% inconsistent(S,Prime) 
%
%    true if at least one of S's beliefs are inconsistent with Prime's beliefs.
%
% NB: Can make more efficient by stopping as soon as one inconsistent 
%     belief is found.
%
%======================================================
inconsistent(S,Prime) :-
    findall( Result, 
	      ( belief(S,B), 				%Get belief of Suspect's and put in B.
		substantiate(S,B,Prime,Result)),  	%Try substantiate2
	     Results),
    member(no,Results).



%=====================================================================
% Program: substantiate
%	+ S: Suspect
%	+ F: One of S's beliefs.
%	+ Prime: Prime suspect whose story is being checked against S's.
%	- Result: 'yes'  if Prime's beliefs substantiate S's belief F. (can prove F in Prime's belief space)
%		  'no'   if S's belief produce a contradiction in Prime's belief space
%		  'unk'  if if S's beleif can not be proven nor produces a contradition.
%
% A statement is substantiated (yes) in a belief
%      space if it can be proven in that space.
%
% A statement is unsubstantiated (unk) in a belief space 
%      if it can not be proven  or contradicted in that belief space.
%
%  A statement is inconsistent (no)   in a belief space
%      if in contradicts a statement in the belief space.
%
% Substantiates S's statements in Prime's belief space.
%====================================================================

%--------------------------------------------------------------
% True if F can be "proven" in Prime
%   Where F is a belief and Prime is a set of facts representing
%   a parciular "belief space"
%--------------------------------------------------------------
substantiate(S,F,Prime,yes) :-   
	prove(F,Prime),!. 

%--------------------------------------------------------------
% True if the explict negation of S's belief F can
% be proven in Prime's belief space.
%
%--------------------------------------------------------------
substantiate(S,F,Prime,no) :-
   negate(F,NF),
   prove(NF,Prime),!,  
   writeseqnl([Prime,'`s beliefs are INCONSISTENT with',S,'`s belief that:',F]).

%--------------------------------------------------------------
% Semantics relies on "cuts" in other substantiate claues.
% Assumes those failed and  could not prove F in Primes' belief space nor
% could it find a contradiction. This clause concludes that the
% S'd belief F is unknown in Prime's belief space.
%
%--------------------------------------------------------------
substantiate(S,F,Prime,unk) :- 
       writeseqnl([Prime,'`s beliefs do not substantiate or contradict',
                           S,'`s belief that',F]).



%*********************************************************
% substantiate2 
%   is logically equivalent to substantiate but 
%
%     1) exploites the betta-meta interpreter which succeeds for all search tree 
%           branches generating   proofs which can act as explanations and results.
%     2) Does not need to deal with negation as this issue is handled 
%           by the Betta-Meta
%     3) Betta-Meta allows Rules to  be defined with other rules not just facts.
%
%*********************************************************

substantiate2(S,F,Prime,yes) :-
   solve(F,Prime,Proof,true),!,
   writeseqnl([Prime,'`s beliefs substantiate',S,'`s belief that:',F]),
   writenl(consider),
   write('        '),
   writeseqnl(Proof),nl.

substantiate2(S,F,Prime,no) :-
   solve(F,Prime,Proof,false),!,
   writeseqnl([Prime,'`s beliefs are INCONSISTENT with',S,'`s belief that:',F]),
   writenl(consider),
   write('        '),
   writeseqnl(Proof),nl.

substantiate2(S,F,Prime,unk) :-
   solve(F,Prime,Proof,unk),
   writeseqnl([Prime,'`s beliefs don`t substantiate or contradict',S,'`s belief that',F]),
   writenl(consider),
   write('        '),
   writeseqnl(Proof),nl.
