% ================================================================= % == == % == 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.

% EXAMPLES %

%> adding_proof(x+(y+z),y+(z+x),Proof,[x+(y+z)]).