%  =================================================================
%  ==                                                             ==
%  ==          An Introduction to ARTIFICIAL INTELLIGENCE         ==
%  ==                  Janet Finlay and Alan Dix                  ==
%  ==                       UCL Press, 1996                       ==
%  ==                                                             ==
%  =================================================================
%  ==                                                             ==
%  ==        chapter 3, pages 53-54:  addition proof graph        ==
%  ==                   pages 62-63:  closed lists                ==
%  ==                                                             ==
%  ==            Prolog example, Alan Dix, August 1996            ==
%  ==                                                             ==
%  =================================================================


%  The addition proof graph can be represnted extensionally
%  as in hanext.pl, but instead we will simply represent
%  general proof rules for addition:

adding_law(a,L+(M+N),(L+M)+N).    %  associative law
adding_law(c,M+N,N+M).            %  commutative law

%  This looks too good to be true, almost quoting
%  the laws from the book!
%  This is because Prolog very kindly matches expressions
%  like x+(y+z) for us.
%
%  Note that when you enter something like x+y, or even X+Y,
%  Prolog does not do the arithmatic.  Instead, it simply
%  constructs a representation of the expression.

%  However, one extra rule is needed.  The commutative law is reflexive,
%  but the associative law really needs a second law of the form:

    adding_law(a,(L+M)+N,L+(M+N)).    %  associative law 2

%  to allow it to work in both directions.
%
%  Alternatively, we could have added a general rule of the form:
%    adding_law(R,X,Y) :- adding_law(R,Y,X).
%  This says that if law R says that X=Y then it also means
%  that Y=X  -  equality is symmetric.
%  However, this leads prolog into its own infinite stuttering search
%  and would need additional rukles to prevent this. 
%  So we'll stick to using associative law 2


%  Given such laws we can write a predicate which proves
%  such laws and keeps track of the train of reasoning:

bad_adding_proof(Start,Start,[Start]).

bad_adding_proof(Start,End,[Start,Law|Proof]) :-
        adding_law(Law,Start,Next),
        write('looking at '), write(Next), nl,
        bad_adding_proof(Next,End,Proof).

%  It is designed to generate proofs of the form:
%          [x+(y+z),c,(y+z)+x,a,y+(z+x)]

%  What is wrong with it?

%  Try running it to see - the 'write's will let
%  you see what is going on.

%  To make it work we need a 'closed list' (see pages 62/63) to
%  stop us stuttering.

adding_proof(Start,Start,[Start],Closed).

adding_proof(Start,End,[Start,Law|Proof],Closed) :-
        adding_law(Law,Start,Next),
        write('looking at '), write(Next), nl,
        not member(Next,Closed),
        write('not seen before'), nl,
        adding_proof(Next,End,Proof,[Next|Closed]).

%  The closed list stops it revisiting the same state and Prolog's
%  backtracking allows it to lok at alternative prrof paths when
%  it gets stuck.  This is a form of depth-first search
%  (see section 3.2.1, page 55 on).


%  RUNNING THIS CODE
%
%  Try the example in the book:
%
%          adding_proof(x+(y+z),y+(z+x),Proof,[x+(y+z)]).
%
%  Note the closed list starts off as the start state - the only
%  place you have visited so far.
%

%  The proof engine would work for any equality type proofs.
%  For example, we could include multiplication rules like:
%
%    adding_law(am,L*(M*N),(L*M)*N).  %  associativity of multiplication
%    adding_law(cm,M*N,N*M).          %  commutativity of multiplication
%    adding_law(d,L*(M+N),(L*M)+(L*N)).     %  distributivity
%

%  Two sorts of problem prevent this being able to solve all
%  mathematics (!)

%  First, some more general mathematical things need to be added.
%  For example, at the moment it doesn't look 'inside' brackets,
%  so it can't probe that x+(y+z)=x+(z+y)
%
%  This is not too difficult to solve - it needs some rules such as:
%      adding_law(R,X+Y,Z+Y) :- adding_law(R,X,Z).
%  This says that if X=Z then X+Y=X+Z

%  More fundamental is that the search space becomes very big.
%  Some things can be solved by brute force, but more difficult
%  problems require some insight.  Real automatic proof systems
%  include many heuristics, rules to help guide the proof along
%  (hopefully) fruitful lines.  This includes things like "bring
%  like terms together" so that they can cancel out or be grouped
%  together.