% =================================================================
% == ==
% == 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,
\+ 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.
