/* BOYER. Leon Sterling Updated: 24 July 81 A simple Boyer-Moore theorem prover as in Chap. 11 The Productive Use of Failure in 'Artificial Mathematicians'. The code written here is a simplified version of the algorithm described in a paper of J Moore 'Computational Logic: Structure Sharing and Proof of Program Properties', Xerox report CSL 75-2, which appeared also as Dept. of Computational Logic memo no. 68, and the second part of Moore's Ph.D. thesis. This is a simplified version of the theorem-prover described in the book 'A Computational Logic' by Boyer and Moore. Variable and procedure names have been chosen to be the same as much as possible, and the mini-projects will be aided by the description in the paper. */ %% PROOF STRATEGY %% % To prove a theorem use the following algorithm % (on p. of 'Artificial Mathematicians') : % 1.-2. Try symbolic evaluation, recording the % reasons for failure in the list Analysis. % 3.-4. If unsuccessful, try proof by induction % using the previously generated failure list % to suggest the induction scheme. % 5. Finally try generalising the theorem if the % induction was unsuccessful. prove(A) :- writef('\nTrying to prove %t\n',[A]), symbol_eval(A,B,Analysis), % Try symbolic evaluation prove1(B,Analysis). prove1(tt,_) :- % Symbolic evaluation was successful !, writef('Expression evaluated to tt\n'). prove1(A,Analysis) :- pickindvars(A,Analysis,Var), % find induction candidate prove_by_induction(A,Var). prove1(A,Analysis) :- generalise(A,New), !, prove(New=tt). %% SYMBOLIC EVALUATION %% % Symbolic evaluation is performed by the procedure % symbol_eval(A,New,Analysis) which evaluates % expression A into expression New producing % failure bag Analysis. % Primitive pure LISP functions, i.e. car,cdr,cond % and equal are handled by an evaluator if they % can be simplified. Otherwise function arguments % are symbolically evaluated bottom-up, % bottoming out on atomic expressions. Function % definitions are expanded according to the criteria % described in the section of code % %% EXPANSION OF FUNCTION DEFINITIONS %% % symbol_eval(tt,tt,[]) :- !. % Finished if expression evaluates to tt symbol_eval([],[],[]) :- !. symbol_eval(A,B,Analysis) :- eval(A,A1), % Evaluate primitive expressions !, symbol_eval(A1,B,Analysis). symbol_eval(A,B,Analysis) :- % Recursively rewrite terms A=..[Pred|Args], % bottom-up. rewrite(Args,Args1,Anal), A1=..[Pred|Args1], expand(Pred,A1,A2,Fault), % Expand recursively defined merge(Fault,Anal,Analysis), % non-primitive functions def_eval(A2,B). rewrite([],[],[]) :- !. rewrite(X,X,[]) :- atomic(X), !. rewrite([H|T],[H1|T1],Analysis) :- symbol_eval(H,H1,Fault), rewrite(T,T1,Desc), merge(Fault,Desc,Analysis). % Evaluator eval(car([]),[]) :- !. eval(cdr([]),[]) :- !. eval(car(cons(H,T)),H) :- !. eval(cdr(cons(H,T)),T) :- !. eval(cond([],U,V),V) :- !. eval(cond(cons(X,Y),U,V),U) :- !. eval(equal(X,X),tt) :- !. %% EXPANSION OF FUNCTION DEFINITIONS %% % Functions that can be expanded according to % their function definition are contained in an % open_fn predicate. In rewriting expressions % functions are expanded where possible % using the predicate open_eval unless % ugly expressions are found. In this case the % fault description is returned as described % in section 3.2 of Moore's paper. % expand(Pred,Clause,Clause,Fault) :- open_fn(Clause,Newclause), ugliness(Pred,Newclause,Bomb), Bomb\==[], !, make_fault(Bomb,Fault). expand(Pred,Clause,Newclause,[]) :- open_eval(Clause,Newclause). expand(Pred,Clause,Clause,[]). open_fn(append(X,Y),cond(X,cons(car(X),append(cdr(X),Y)),Y)) :- !. open_eval(append(X,Y),Clause) :- def_eval(car(X),C1), def_eval(cdr(X),C2), def_eval(cond(X,cons(C1,append(C2,Y)),Y),Clause). def_eval(X,Y) :- eval(X,Y), !. def_eval(X,X). % Make up a fault description from the faults % returned when trying to expand a recursively % defined function. make_fault([],[]) :- !. make_fault([fault(B,F)|Bombs],[fault(B,F)|Faults]) :- make_fault(Bombs,Faults). make_fault([bomb(X)],[fault(bomb(X),fail([]))]). make_fault([fail(X)],[fault(bomb([]),fail(X))]). make_fault([bomb(X),fail(Y)],[fault(bomb(X),fail(Y))]). make_fault([fail(Y),bomb(X)],[fault(bomb(X),fail(Y))]). % Is expression ugly? ugliness(Pred,X,[]) :- atomic(X), !. ugliness(Pred,X,Analysis) :- nasty_car_or_cdr(X), !, analyse(Pred,X,Analysis). ugliness(_,X,Analysis) :- X=..[Pred|Args], find_ugly(Pred,Args,Analysis). find_ugly(_,[],[]) :- !. find_ugly(Pred,[H|T],Analysis) :- ugliness(Pred,H,H1), find_ugly(Pred,T,T1), append(H1,T1,Analysis), !. nasty_car_or_cdr(car(X)) :- nontrivial(X), !. nasty_car_or_cdr(cdr(X)) :- nontrivial(X), !. add_bomb(X,[],X) :- !. add_bomb(Y,X,Z) :- append(Y,[X],Z). analyse(Pred,X,[bomb(X)]) :- loop_threat(Pred,X), !. analyse(Pred,X,[fail(X)]). loop_threat(append,car(X)). loop_threat(append,cdr(X)). nontrivial(X) :- memberchk(X,[cons(U,V),[]]), !, fail. nontrivial(X). %% PROOF BY INDUCTION %% % Find induction candidate % A simple majority vote is used to decide % which list to induct on. % This is calculated by max. pickindvars(_,Bag,Var) :- max(Bag,[],Term,0,N), Term = fault(bomb(cdr(Var)),fail(_)). max([],A,A,N,N) :- !. max([pair(Pred,M)|Rest],Current,Ans,N,Num_ans) :- M > N, !, max(Rest,Pred,Ans,M,Num_ans). max([_|Rest],Current,Ans,N,Num_ans) :- max(Rest,Current,Ans,N,Num_ans). % Successively prove the base and step cases prove_by_induction(A,Literal) :- prove_base(A,Literal), prove_step(A,Literal). % To prove the base case, substitute the nil list % for the induction variable, and try to prove % the resultant clause prove_base(A,Literal) :- writef('\n Base case'), subst(Literal=[],A,New), prove(New), !. % To prove the step case, substitute the appropriate % cons expression into the clause, symbolically % evaluate as much as possible, then fertilise % to prove the expression prove_step(A,Literal) :- writef('\nStep case'), subst(Literal=cons(a1,Literal),A,New), symbol_eval(New,Clause,_), fertilise(A,Clause,Newclause), prove(Newclause). fertilise(equal(X,Y),Clause,New) :- subst(X=Y,Clause,New). %% PROOF BY GENERALISATION %% % Code to be written % test cases z :- prove(equal(append([],x),x)). y :- prove(equal(append(a,append(b,c)),append(append(a,b),c))). /* Mini-projects 1. Add definitions of functions like reverse and copy to enable the theorem-prover to work on other examples. Explain how the theorem-prover might be modified to overcome any small problems that might arise. 2. Use more sophisticated criteria to choose the induction variable, or more generally the induction schema to be used. This will probably involve changing the way the failures are returned in the variable Analysis. 3. Write a more powerful version of fertilise. 4. Write code to perform generalise. */ % merge merges two bags merge([],Bag,Bag) :- !. merge(Bag,Var,Hack) :- var(Var), !, merge(Bag,[variable],Hack). merge([pair(Ugly,K)|T],Bag,Newbag) :- select(pair(Ugly,N),Bag,Rest), !, M is N + K, merge(T,[pair(Ugly,M)|Rest],Newbag). merge([pair(Ugly,N)|T],Bag,Newbag) :- !, merge(T,[pair(Ugly,N)|Bag],Newbag). merge([H|T],Bag,Newbag) :- select(pair(H,N),Bag,Rest), !, M is N + 1, merge(T,[pair(H,M)|Rest],Newbag). merge([H|T],Bag,Newbag) :- merge(T,[pair(H,1)|Bag],Newbag).