/* Solution to ES 1996 Homework 4 */

/*  Backward Chaining Propositional Logic Expert System Shell

    To use this rules must be entered. To run the rules for the animal
    example in Winston, enter:

    :-['shellPropBC.pro',sbcWin].
    :-start.
*/
:-[-'ask.pro'].       % Loads procedures for asking questions.

% Operand definitions necessary for rules. Note that operands must
% be defined before rules can be loaded.
%
:-op(900,xfx,:).        :-op(850,fx,if).        :-op(800,xfx,then).
:-op(750,xfy,or).       :-op(700,xfy,and).      :-op(650,fy,not).


% Rules for problem 2:
%

% 
% r1:if c then d.
% r1a:if not c then e.
% r2:if a then not c.
% r3:if b then c.
% askable(a,'Is a true?').
% askable(b,"Is b true?").
% aGoalList([c,d]).
% 

start:-wipe,deduce(vcrProblemFound).

askable(userSaysVCRbroken,'Is the VCR broken?').
askable(userSaysShowCancelled,'Was the show cancelled?').

aGoalList([vcrBroken,showCancelled]).

r1:if vcrBroken or showCancelled then vcrProblemFound.
r2:if userSaysVCRbroken then vcrBroken.
r3:if userSaysShowCancelled then showCancelled.

% Remove facts from previous run, if any.
%
wipe:-!,abolish(found,2);true.

% deduce(Goal) succeeds if Goal is proven true.
%
% Each deduce clause handles a different type of Goal; they are: Goal
% previously found, Goal deducible using a rule, Goal contains
% conjunction, Goal contains disjunction, Goal contains a negation,
% and Goal askable. If none of these clauses match Goal then a syntax
% error has occured (because the Goal is neither provable by a rule
% nor can the user be asked about its truth).
%

% Goal previously found.
%
deduce(Goal):-found(Goal,From),!,From=userTrue.

% Goal using rule.
%
deduce(Goal):-
        Rule:if Antecedent then not Goal,
        deduce(Antecedent),announce(Goal,false),!,fail.
          
% Goal using rule.
%
deduce(Goal):-
	atom(Goal),
        Rule:if Antecedent then Goal,
        deduce(Antecedent),announce(Goal,true),!.
          
% Goal contains conjunction.
%
deduce(Goal1 and Goal2):-
        deduce(Goal1),deduce(Goal2).

% Goal contains disjunction.
%
deduce(Goal1 or Goal2):-
        ( deduce(Goal1) ; deduce(Goal2) ),!.

% Goal contains negation.
%
deduce(not Goal):-
        deduce(Goal),!,fail
        ;
        true.

% Ask user and add answer to database.
%
deduce(Goal):-askable(Goal,Question),
        askAndCheck(Question,x,yesNo,A),
        ( 
            A=true,Resp=userTrue  ;  A=false,Resp=userFalse 
          ; A=unknown,Resp=userDN 
        ),
        asserta(found(Goal,Resp)),!,Resp=userTrue.

% Check for unprovable assertions.
%
deduce(Goal):-
        atom(Goal),not(_:if _ then Goal),
        sOut<<"Assertion "<<Goal<<" is unprovable."<<nl,!,fail.

% Print a message when selected facts are proven.
%
announce(Goal,Truth):-
	aGoalList(Goals),
	member(Goal,Goals),
	sOut<<"The proposition "<<Goal<<" has been proven "<<Truth<<"."<<nl.

announce(_,_).	% Succeed even if goal is not to be announced.