%% NEXT FILE %% nextfl ,dska:emas4.ccl ,nextfl ,dska:infer.[400,405,teach] ,nextfl ,dska:mandc.[400,405,teach] ,nextfl ,dska:random.[400,405,teach] ,nextfl ,dska:random.old[400,405,teach] ,nextfl ,dska:read.[400,405,teach] ,nextfl ,dska:readin.[400,405,teach] ,nextfl ,dska:figure.[400,405,teach,evans] ,nextfl ,dska:figure.sol[400,405,teach,evans] ,nextfl ,dska:evans.[400,405,teach,evans] ,nextfl ,dska:evans.mss[400,405,teach,evans] ,nextfl ,dska:eliza.[400,405,teach,nl] ,nextfl ,dska:eliza.new[400,405,teach,nl] ,nextfl ,dska:atn.[400,405,teach,nl] ,nextfl ,dska:atn.old[400,405,teach,nl] ,nextfl ,dska:qa.[400,405,teach,nl] ,nextfl ,dska:parse.[400,405,teach,nl] ,nextfl ,dska:isol.sol[400,405,teach,winst] ,nextfl ,dska:arch.sol[400,405,teach,winst] ,nextfl ,dska:arch1.sol[400,405,teach,winst] ,nextfl ,dska:arch.prb[400,405,teach,winst] ,nextfl ,dska:arch1.prb[400,405,teach,winst] ,nextfl ,dska:winst.[400,405,teach,winst] ,nextfl ,dska:isol.prb[400,405,teach,winst] ,nextfl ,dska:block.prb[400,405,teach,winst] ,nextfl ,dska:pair.prb[400,405,teach,winst] ,nextfl ,dska:wplanc.[400,405,teach,plan] ,nextfl ,dska:wpo.[400,405,teach,plan] ,nextfl ,dska:expon.[400,405,teach,plan] ,nextfl ,dska:heuris.sol[400,405,teach,math] ,nextfl ,dska:breadt.sol[400,405,teach,math] ,nextfl ,dska:semant.sol[400,405,teach,math] ,nextfl ,dska:formul.[400,405,teach,math] ,nextfl ,dska:skolem.sol[400,405,teach,math] ,nextfl ,dska:divide.[400,405,teach,math] ,nextfl ,dska:model.[400,405,teach,math] ,nextfl ,dska:equal.[400,405,teach,math] ,nextfl ,dska:rewrit.sol[400,405,teach,math] ,nextfl ,dska:unify.[400,405,teach,math] ,nextfl ,dska:simple.[400,405,teach,math] ,nextfl ,dska:semant.[400,405,teach,math] ,nextfl ,dska:rewrit.[400,405,teach,math] ,nextfl ,dska:skolem.[400,405,teach,math] ,nextfl ,dska:breadt.[400,405,teach,math] ,nextfl ,dska:heuris.[400,405,teach,math] ,nextfl ,dska:boyer.[400,405,teach,math] %% NEXT FILE %% /*infer*/ /*LOGO type inference package Alan Bundy 16.11.79*/ /*infer fact by backwards inference*/ infer(Goal) :- infer(Goal,now). infer(Goal,Sit) :- fact(Goal,Sit). infer(Goal,Sit) :- backward_rule(Ant,Goal), infer(Ant,Sit). infer(Goal1&Goal2,Sit) :- infer(Goal1,Sit), infer(Goal2,Sit). /*assert fact and trigger forwards inference*/ assert_fact(Fact) :- assert_fact(Fact,now). assert_fact(Fact,Sit) :- assert(fact(Fact,Sit)), writef('asserting %t in situation %t\n',[Fact,Sit]), forall(forward_rule(Fact,New),assert_fact(New,Sit)). %% NEXT FILE %% /*mandc Missionaries and Cannibals program Alan Bundy 6.11.79*/ /*top level*/ mandc :- gofrom([3,3,1],[0,0,0],[]). gofrom([0,0,0],Right,OldLefts) :- writef('which is goal state\n \n',[]). gofrom(Left,Right,OldLefts) :- legal(Left), legal(Right), not(member(Left,OldLefts)), applymove(Left,Right,[ML,CL,BL],[MR,CR,BR]), writef('\nThe left bank now contains %t missionaries and %t cannibals \n',[ML,CL]), writef('The right bank now contains %t missionaries and %t cannibals \n',[MR,CR]), gofrom([ML,CL,BL],[MR,CR,BR],[Left|OldLefts]). gofrom(_,_,_) :- writef('Backing up one move \n',[]), fail. /*decide which way to move*/ applymove([ML,CL,BL],Right,NewL,NewR) :- (BL=1 -> moveload([ML,CL,BL],Right,NewL,NewR); moveload(Right,[ML,CL,BL],NewR,NewL) ). /*move boatload over*/ moveload(Source,Target,NewS,NewT) :- move(BoatLoad), maplist(>=, Source, BoatLoad), mlmaplist(minus,[Source,BoatLoad,NewS]), mlmaplist(add,[Target,BoatLoad,NewT]), BoatLoad=[M,C,B], writef('\n move %t missionaries and %t cannibals \n',[M,C]). /*the moves*/ move([0,1,1]). move([2,0,1]). move([0,2,1]). move([1,1,1]). move([1,0,1]). /*is situation legal*/ legal([M,C,B]) :- (M=0; M >= C), !. legal([M,C,B]) :- writef('%t cannibals can eat %t missionaries \n',[C,M]), fail. /*add and minus are + and - on lists*/ add([X,Y,Z]) :- Z is X+Y. minus([X,Y,Z]) :- Z is X-Y. %% NEXT FILE %% /*random*/ /*Random number generator Alan Bundy 22.11.79*/ /*Get Num from Seed and update seed*/ random(Range,Num) :- seed(Seed), Num is (Seed mod Range) + 1, retract(seed(Seed)), NewSeed is 125*Seed+1, assert(seed(NewSeed)). /*random number seed*/ seed(13). /*Choose random element of list*/ random_pick(List,El) :- length(List,L), random(L,N), nth(N,List,El). /*find nth element of a list*/ nth(1,[Hd|Tl],Hd) :- !. nth(N,[Hd|Tl],El) :- N>1, !, N1 is N-1, nth(N1,Tl,El). %% NEXT FILE %% /*random*/ /*Random number generator Alan Bundy 22.11.79*/ /*Get random Num in Range*/ random(Range,Num) :- seed(Seed), random(Range,Seed,Num). /*Get Num ffrom Seed first time*/ random(Range,Seed,Num) :- Num is (Seed mod Range) + 1. /*Grow Num on subsequent occasions*/ random(Range,Seed,Num) :- NewSeed is 125*Seed + 1, random(Range,NewSeed,Num). /*random number seed*/ seed(13). /*Choose random element of list*/ random_pick(List,El) :- length(List,L), random(L,N), nth(N,List,El). /*find nth element of a list*/ nth(1,[Hd|Tl],Hd) :- !. nth(N,[Hd|Tl],El) :- N>1, !, N1 is N-1, nth(N1,Tl,El). %% NEXT FILE %% /*read file term by term*/ foo :- see(mandc), repeat, read(T), write(T), nl, T=(:-end), seen. %% NEXT FILE %% /* Read a sentence */ :- mode initread(-). :- mode readrest(+,-). :- mode word(-,?,?). :- mode words(-,?,?). :- mode alphanum(+,-). :- mode alphanums(-,?,?). :- mode digits(-,?,?). :- mode digit(+). :- mode lc(+,-). :- module(readin,[read_in(1)]). /* Read sentence */ read_in(P):-initread(L),words(P,L,[]),!. initread([K1,K2|U]):-get(K1),get0(K2),readrest(K2,U). readrest(46,[]):-!. readrest(63,[]):-!. readrest(33,[]):-!. readrest(K,[K1|U]):-K=<32,!,get(K1),readrest(K1,U). readrest(K1,[K2|U]):-get0(K2),readrest(K2,U). words([V|U]) --> word(V),!,blanks,words(U). words([]) --> []. word(U1) --> [K],Elc(K,K1)L,!,alphanums(U2),Ename(U1,[K1|U2])L. word(nb(N)) --> [K],Edigit(K)L,!,digits(U),Ename(N,[K|U])L. word(V) --> [K],Ename(V,[K])L. alphanums([K1|U]) --> [K],Ealphanum(K,K1)L,!,alphanums(U). alphanums([]) --> []. alphanum(K,K1):-lc(K,K1). alphanum(K,K):-digit(K). digits([K|U]) --> [K],Edigit(K)L,!,digits(U). digits([]) --> []. blanks--> [K],EK=<32L,!,blanks. blanks --> []. digit(K):-K>47,K<58. lc(K,K1):-K>64,K<91,!,K1 is K\/8'40. lc(K,K):-K>96,K<123. %% NEXT FILE %% /*figures*/ /*test descriptions for evans program*/ /*Alan Bundy 26.10.79*/ problem1(Ans) :- evans(figa,figb,figc,[fig1,fig2,fig3,fig4,fig5],Ans). problem2(Ans) :- evans(figa,figb,figc,[fig1,fig2,fig3,fig4a,fig5],Ans). problem3(Ans) :- evans(figa,figb,figc,[fig1,fig2,fig3,fig5],Ans). objects(figa,[tri1,tri2]). relations(figa,[[inside,tri1,tri2]]). objects(figb,[tri3]). relations(figb,[]). similarities(figa,figb,[[tri2,tri3,direct], [tri1,tri3,[scale,2]]]). objects(figc,[square,circle]). relations(figc,[[inside,square,circle]]). objects(fig1,[circle2,circle3]). relations(fig1,[[inside,circle2,circle3]]). similarities(figc,fig1,[[circle,circle3,direct], [circle,circle2,[scale,half]]]). objects(fig2,[square2]). relations(fig2,[]). similarities(figc,fig2,[[square,square2,direct]]). objects(fig3,[tri4,circle4]). relations(fig3,[[inside,tri4,circle4]]). similarities(figc,fig3,[[circle,circle4,direct]]). objects(fig4,[circle5]). relations(fig4,[]). similarities(figc,fig4,[[circle,circle5,direct]]). objects(fig4a,[square3]). relations(fig4a,[]). similarities(figc,fig4a,[[square,square3,[scale,2]]]). objects(fig5,[tri5]). relations(fig5,[]). similarities(figc,fig5,[]). %% NEXT FILE %% yes | ?- problem1(A). Rule is: remove: [_527] add: [] match: [[_537,_547,direct]] source: [[inside,_527,_537]] target: [] Answer description is: objects: [_547] relations: [] similarities: [[circle,_547,direct]] Answer is fig4 A = fig4 yes | ?- problem2(A). Rule is: remove: [_527] add: [] match: [[_537,_547,direct]] source: [[inside,_527,_537]] target: [] Answer description is: objects: [_547] relations: [] similarities: [[circle,_547,direct]] Rule is: remove: [_527] add: [] match: [[_537,_547,[scale,2]]] source: [[inside,_537,_527]] target: [] Answer description is: objects: [_547] relations: [] similarities: [[square,_547,[scale,2]]] Answer is fig4a A = fig4a yes | ?- problem3(A). Rule is: remove: [_527] add: [] match: [[_537,_547,direct]] source: [[inside,_527,_537]] target: [] Answer description is: objects: [_547] relations: [] similarities: [[circle,_547,direct]] Rule is: remove: [_527] add: [] match: [[_537,_547,[scale,2]]] source: [[inside,_537,_527]] target: [] Answer description is: objects: [_547] relations: [] similarities: [[square,_547,[scale,2]]] Rule is: remove: [_381,_391] add: [_401] match: [] source: [[inside,_381,_391]] target: [] Answer description is: objects: [_401] relations: [] similarities: [] Answer is fig5 A = fig5 yes | ?- core 49664 (20480 lo-seg + 29184 hi-seg) heap 15360 = 14048 in use + 1312 free global 1187 = 16 in use + 1171 free local 1024 = 16 in use + 1008 free trail 511 = 0 in use + 511 free 0.06 sec. for 1 GCs gaining 144 words 0.08 sec. for 4 local shifts and 12 trail shifts 1.77 sec. runtime %% NEXT FILE %% /*evans*/ /*Evan's Geometric Analogy Program - Rational Reconstruction*/ /*Alan Bundy 26.10.79*/ /*top level program*/ evans(FigA,FigB,FigC,AnsList,Ans) :- find_rule(FigA,FigB,Rule), rule_is(Rule), apply_rule(Rule,FigC,AnsObjs,AnsRels,Sims), ans_desc(AnsObjs,AnsRels,Sims), select_result(FigC,AnsList,AnsObjs,AnsRels,Sims,Ans), ans_is(Ans). /*find rule given figures*/ find_rule(FigA,FigB,Rule) :- relations(FigA,Source), relations(FigB,Target), objects(FigA,Alist), objects(FigB,Blist), similarities(FigA,FigB,Triples), select_set(Triples,Matches), takeaway1(Alist,Matches,Removals), takeaway2(Blist,Matches,Adds), make_rule(Removals,Adds,Matches,Source,Target,Rule). /* Apply rule to figc to produce answer*/ apply_rule(rule(Removals,Adds,Matches,Source,Target), FigC, AnsObjs,Target,Matches) :- relations(FigC,FigDesc), objects(FigC,ObList), seteq(FigDesc,Source), maplist(second,Matches,NewList), append(NewList,Adds,AnsObjs). /* Select Result from those provided */ select_result(FigC,[FigN|Rest],AnsObjs,AnsRels,AnsSims,FigN) :- relations(FigN,NRels), seteq(NRels,AnsRels), similarities(FigC,FigN,NSims), seteq(NSims,AnsSims), objects(FigN,NObjs), seteq(NObjs,AnsObjs). select_result(FigC,[FigN|Rest],AnsObjs,AnsRels,AnsSims,Ans) :- select_result(FigC,Rest,AnsObjs,AnsRels,AnsSims,Ans). /*select legal subset of similarity triples for matches*/ select_set(Triple,Match) :- select_set1([],[],Triple,Match). select_set1(Aused,Bused,[],[]). select_set1(Aused,Bused,[[Aobj,Bobj,Trans]|Rest],[[Aobj,Bobj,Trans]|Rest1]) :- not(member(Aobj,Aused)), not(member(Bobj,Bused)), select_set1([Aobj|Aused],[Bobj|Bused],Rest,Rest1). select_set1(Aused,Bused,[[Aobj,Bobj,Trans]|Rest],Rest1) :- select_set1(Aused,Bused,Rest,Rest1). /*take away the triples from the list*/ takeaway1(List,Triples,Ans) :- maplist(first,Triples,Firsts), subtract(List,Firsts,Ans). takeaway2(List,Triples,Ans) :- maplist(second,Triples,Seconds), subtract(List,Seconds,Ans). /* First and second elements of a list */ first([A,B,C],A). second([A,B,C],B). /* Make rule from descriptions inherited from figs a & b*/ make_rule(Removals,Adds,Matches,Source,Target,Rule) :- maplist(first,Matches,Spairs), maplist(second,Matches,Tpairs), append(Removals,Spairs,L1), append(L1,Tpairs,L2), append(L2,Adds,Consts), unbind(Consts,Substs), subst(Substs,rule(Removals,Adds,Matches,Source,Target),Rule). /*find corresponding variable for each constant and produce substitution*/ unbind([],true). unbind([Const|Rest],Const=X & Rest1) :- unbind(Rest,Rest1). /* Messages */ /*----------*/ rule_is(rule(Removals,Adds,Matches,Source,Target)) :- writef('Rule is: remove: %t add: %t match: %t source: %t target: %t \n\n', [Removals,Adds,Matches,Source,Target]). ans_desc(Objs,Rels,Sims) :- writef('Answer description is: objects: %t relations: %t similarities: %t \n\n', [Objs,Rels,Sims]). ans_is(Ans) :- writef('Answer is %t\n\n\n',[Ans]). %% NEXT FILE %% @style(references STDalphabetic,spacing 1,linewidth 79, indent 0) @make(article) @device(lpt) @set(page=1) @define(romanize,use enumerate,numbered <(@i)>) @define(alphabetize,use enumerate,numbered <(@a)>) @use(Bibliography = Press.Bib) @heading(Department of Artificial Intelligence Prolog Program Library Program Specification) @begin(example) @tabdivide(4) @u(Program Name)@\The Evans Geometric Analogy Program@* @u(Source)@\Alan Bundy@* @u(Date of Issue)@\@value(date)@* @tabclear @end(example) @section(Description) This is a rational reconstruction of the second part of Evan's program to solve Geometric Analogy Problems @cite(evans,OccPaper22). It uses the descriptions of geometric figures to form a rule; applies this rule to form the description of an answer figure and then uses this description to select an answer from those provided. The first part of Evan's program, in which figure descriptions are formed from a cartesian representation, is not attempted. @section(Method of Use) To use the program, type @equation[run PLL: UTIL] and in response to the prompt type @equation[consult('PLL: EVANS').] The top level predicate, @b(evans), will then be available. @b(evans) takes 5 arguments: the names of figures A, B, C; a list of possible answer figures and a variable. If it succeeds then @b(evans) binds this variable to one of the answer figures. As it runs @b(evans) prints descriptions of the rules it forms and the answer figures these suggest. For the program to work, assertions must be present in the database describing the figures A, B, C and the possible answer figures and relating objects in figure A to objects in figure B and objects in figure C to objects in each of the answer figures. Some examples of the sort of assertions required are given in file PLL: FIGURE and a selection are reproduced in example @ref(figures) below. @begin(figure) @begin(example) objects(figa,[tri1,tri2]). relations(figa,[[inside,tri1,tri2]]). objects(figb,[tri3]). relations(figb,[]). similarities(figa,figb,[[tri2,tri3,direct], [tri1,tri3,[scale,2]]]). objects(figc,[square,circle]). relations(figc,[[inside,square,circle]]). @end(example) @caption(Assertions to Describe Input Figures) @tag(figures) @end(figure) @begin(itemize) @b(objects) takes a figure name and a list of the objects occuring in the figure. @b(relations) takes a figure name and a list of symbolic descriptions describing the figure. @b(similarities) takes two figure names and a list of similarities betwen objects in the two figures. @end(itemize) The file, PLL: FIGURE, can be input by typing @equation[consult('PLL: FIGURE').] The particular assertions defining figa, figb and figc given above, plus similar ones for fig1-5 will then be in the database and the call @equationE_evans(figa,figb,figc,[fig1,fig2,fig3,fig4,fig5],Ans).L will then succeed and bind Ans to fig4. @section(How it Works) The top level predicate,@b(evans), is defined as follows (omitting print messages): @begin(example) evans(FigA,FigB,FigC,AnsList,Ans) :- find_rule(FigA,FigB,Rule), apply_rule(Rule,FigC,AnsObjs,AnsRels,Sims), select_result(FigC,AnsList,AnsObj,AnsRels,Sims,Ans). @end(example) @b(find_rule) takes the names of figures A and B and forms a description of the rule relating them. @b(apply_rule) takes this rule and applies it to figure C, producing a description of the answer figure and similarities between figure C and the answer figure. @b(select_result) takes these descriptions and compares them to the available answer figures until it finds a match. @b(find_rule) is defined as follows: @begin(example) find_rule(FigA,FigB,Rule) :- relations(FigA,Source), relations(FigB,Target), objects(FigA,Alist), objects(FigB,Blist), similarities(FigA,FigB,Triples), select_set(Triples,Matches), takeaway1(Alist,Matches,Removals), takeaway2(Blist,Matches,Adds), make_rule(Removals,Adds,Matches,Source,Target,Rule). @end(example) The first five subprocedures pick up the prestored descriptions of the two figures. The predicate @b(select_set) picks a legal subset, Matches, of the similarity descriptions between objects in figure A and B. The rule description is based on this subset. On backup a different subset will be chosen and a different rule formed. Objects occuring in figure A, but not involved in a match are then selected by @b(takeaway1) and these become the Removals. Similarly, @b(takeaway2) finds those objects occurring in figure B, but not involved in a match and these become the Adds. A rule description is then formed from these components by @b(make_rule). @b(select_set) and the two @b(takeaway)s are fairly straightforward list manipulation, but @b(make_rule) requires some explanation. It is defined as follows: @begin(example) make_rule(Removals,Adds,Matches,Source,Target,Rule) :- maplist(first,Matches,Spairs), maplist(second,Matches,Tpairs), append(Removals,Spairs,L1), append(L1,Tpairs,L2), append(L2,Adds,Consts), unbind(Consts,Substs), subst(Substs,rule(Removals,Adds,Matches,Source,Target),Rule). @end(example) A rule description consists of the predicate rule with five arguments: @begin(itemize) A list of objects to be removed; A list of objects to be added; A list of matches between objects; The relations in the source figure and The relations in the target figure. @end(itemize) These are pretty much as supplied to @b(make_rule) except that the actual constants inherited from the initial figure descriptions have to be changed for Prolog variables, so that the rule can be applied to figure C. The first five subprocedures of the @b(make_rule) definition consist of making a list, Consts, of all the object names appearing in the Removal, Adds and Matches. A substitution is then built by @b(unbind), in which each of these object names is associated with a different Prolog variable. @b(subst) then substitutes these variables for the objects in the rule description. The definitions of @b(unbind), @b(first) and @b(second) are straightforward and the definitions of @b(maplist) and @b(subst) are given in the Mecho utility program library. The definition of @b(apply_rule) is given below. @begin(example) apply_rule(rule(Removals,Adds,Matches,Source,Target), FigC, AnsObjs,Target,Matches) :- relations(FigC,FigDesc), objects(FigC,ObList), seteq(FigDesc,Source), maplist(second,Matches,NewList), append(NewList,Adds,AnsObjs). @end(example) The first two subprocedures recover the description of figure C. The predicate @b(seteq) then pattern matches the relations in figure C with the rule source description, which binds the first half of the similarity descriptions in Matches. @b(seteq) is set equality and is described in the Mecho utilities library. The objects in the answer figure are calculated by appending the Adds to the objects in the second half of the similarity descriptions in Matches. The definiton oif @b(select_result) is: @begin(example) select_result(FigC,[FigN|Rest],AnsObjs,AnsRels,AnsSims,FigN) :- relations(FigN,NRels), seteq(NRels,AnsRels), similarities(FigC,FigN,NSims), seteq(NSims,AnsSims), objects(FigN,NObjs), seteq(NObjs,AnsObjs). select_result(FigC,[FigN|Rest],AnsObjs,AnsRels,AnsSims,Ans) :- select_result(FigC,Rest,AnsObjs,AnsRels,AnsSims,Ans). @end(example) @b(select_result) is defined by recursion on the list of available answers. If it recurses to the ends of this list then it fails, and @b(evans) backs up to form a new rule. The second clause is merely the recursive step: the first clause makes the interesting comparisons. FigN is the first answer figure name in the list. In turn the relations, objects and similarities of FigN are found in the database, and these are compared with FigC using @b(seteq). FigN is returned as the answer iff the clause succeeds. Otherwise @b(select_result) recurses. @section(Program Requirements) The Prolog system takes 30K words and PLL: UTIL, PLL: EVANS, PLL: FIGURE and working space require an additional 21K words. The following predicates are used by the program: @begin(example) ans_desc(3) ans_is(1) append(3) apply_rule(5) evans(5) find_rule(3) first(2) make_rule(6) maplist(3) member(2) objects(2) problem1(1) problem2(1) problem3(1) relations(2) rule_is(1) second(2) select_result(6)select_set(2) select_set1(4) seteq(2) similarities(3) subst(3) subtract(3) takeaway1(3) takeaway2(3) unbind(2) writef(2) @end(example) @heading(References) @bibliography %% NEXT FILE %% /*eliza*/ /*natural language conversational program Alan Bundy 15.11.79*/ /*variable marker*/ :- op(500,fx,[?]). /*top level*/ eliza :- read_in(Input), eliza(Input). eliza([bye,.]) :- !. eliza(Input) :- sr_pair(S,R), match(Input,S,off,Subst), replace(R,Subst,Output), print_list(Output), eliza. /*associative one way matcher*/ match([],[],off,[]). match([Word|RestSent],[Word|RestPatt],off,Subst) :- match(RestSent,RestPatt,off,Subst). match([Word|RestSent],[?Var|RestPatt],off,[[Word|Phrase]/Var|Subst]) :- match(RestSent,RestPatt,?Var,[Phrase/Var|Subst]). match(Sent,Patt,?Var,[[]/Var|Subst]) :- match(Sent,Patt,off,Subst). match([Word|RestSent],RestPatt,?Var,[[Word|Phrase]/Var|Subst]) :- match(RestSent,RestPatt,?Var,[Phrase/Var|Subst]). /*substitute text for variables*/ replace([],Subst,[]). replace([?Var|Rest],Subst,New) :- !, member(Phrase/Var,Subst), replace(Rest,Subst,Old), append(Phrase,Old,New). replace([Word|RestPatt],Subst,[Word|RestSent]) :- replace(RestPatt,Subst,RestSent). /*print list of words without brackets or commas*/ print_list([]) :- writef('\n \n',[]). print_list([Hd|Tl]) :- writef('%t ',[Hd]), print_list(Tl). /*stimulus response table*/ sr_pair([i,am,?x,.],[how,long,have,you,been,?x,?]). sr_pair([?x,you,?y,me,.],[what,makes,you,think,i,?y,you,?]). sr_pair([?x],[please,go,on,.]). %% NEXT FILE %% /* Simple ELIZA -- a natural language misunderstander -- Alan Bundy 15-Nov-79, Richard O'Keefe 17-Feb-81 */ :- [readin]. % load read_in(-) adn its support. :- public eliza/0. :- mode eliza. eliza :- read_in(Input), mandatory_substitutions(Input, Clean), Clean \== [bye,.], rule(Given, Yield), match(Given, Clean), reply(Yield), nl, !, eliza. eliza :- write('I hope I have helped you.'), nl. :- mode mandatory_substitutions(+, -), idiom(+, -). mandatory_substitutions(Given, Yield) :- idiom(Phrase, Translation), append(Phrase, Rest_of_Given, Given), append(Translation, Rest_of_Yield, Yield), !, mandatory_substitutions(Rest_of_Given, Rest_of_Yield). mandatory_substitutions([Period], [.]) :- !. mandatory_substitutions([Word|Rest_of_Given], [Word|Rest_of_Yield]) :- !, mandatory_substitutions(Rest_of_Given, Rest_of_Yield). idiom([i], [you]). idiom([me], [you]). idiom([we], [you]). idiom([us], [you]). idiom([you], [i]). idiom([my], [your]). idiom([mine], [yours]). idiom([our], [your]). idiom([ours], [yours]). idiom([your], [my]). idiom([yours], [mine]). idiom([am], [are]). idiom([you,are],[i,am]). idiom([stop], [bye]). idiom([quit], [bye]). idiom([goodbye],[bye]). idiom([please], []). :- mode match(+, +), append(?, ?, ?). match([Head|Rest], Fragment) :- append(Head, Leftover, Fragment), match(Rest, Leftover). match([Head|Rest], [Head|Leftover]) :- !, match(Rest, Leftover). match([], []). append([], List, List). append([Head|Tail], List, [Head|Rest]) :- !, append(Tail, List, Rest). :- mode reply(+). reply([Head|Tail]) :- reply(Head), !, reply(Tail). reply([]). reply(Proper_Word) :- write(' '), write(Proper_Word). rule([you,are,X,.], [how,long,have,you,been,X,?]). rule([X,i,Y,you,.], [what,makes,you,think,i,Y,you,?]). rule([you,like,Y,.], [does,anyone,else,in,your,family,like,Y,?]). rule([you,feel,X,.], [do,you,often,feel,that,way,?]). rule([X], [please,go,on,.]). %% NEXT FILE %% /*atn*/ /*generation of random sentences from an ATN Alan Bundy 19.11.79 use with random*/ /*Top Level*/ generate :- generate(sentence,start), writef('\n\n',[]), generate. generate(ATN,finish). generate(ATN,Node) :- arc(ATN,Node,Choices), random_pick(Choices,[NewNode,Label,Type]), gen(Type,Label,ATN,NewNode). gen(atn,SubATN,ATN,NewNode) :- generate(SubATN,start), generate(ATN,NewNode). gen(word,Word,ATN,NewNode) :- writef('%t ',[Word]), generate(ATN,NewNode). /*ATNs*/ /*Sentence ATN*/ arc(sentence,start,[[a,nounphrase,atn]]). arc(sentence,a,[[b,verb,atn]]). arc(sentence,b,[[c,nounphrase,atn]]). arc(sentence,c,[[finish,stop_mark,atn]]). /*nounphrase ATN*/ arc(nounphrase,start,[[finish,proper_noun,atn], [a,determiner,atn]]). arc(nounphrase,a,[[finish,noun,atn], [a,adjective,atn]]). /*verb ATN*/ arc(verb,start,[[finish,is,word], [finish,kisses,word], [finish,kills,word]]). /*determiner ATN*/ arc(determiner,start,[[finish,a,word], [finish,an,word], [finish,the,word]]). /*noun ATN*/ arc(noun,start,[[finish,fascist,word], [finish,dictator,word]]). /*adjective ATN*/ arc(adjective,start,[[finish,happy,word], [finish,fascist,word], [finish,italian,word]]). /*Proper Noun ATN*/ arc(proper_noun,start,[[finish,benito,word]]). /*Stop Mark ATN*/ arc(stop_mark,start,[[finish,(.),word], [finish,(?),word], [finish,(!),word]]). %% NEXT FILE %% /*atn*/ /*generation of random sentences from an ATN Alan Bundy 19.11.79 use with eliza (for print_list)*/ /*Top Level*/ generate :- generate(sentence,start,Sentence), print_list(Sentence), fail. generate(ATN,finish,[]). generate(ATN,Node,[Word|Rest]) :- arc(ATN,Node,NewNode,Word,t), generate(ATN,NewNode,Rest). generate(ATN,Node,Sent) :- arc(ATN,Node,NewNode,SubATN,nt), generate(SubATN,start,SubBit), generate(ATN,NewNode,Rest), append(SubBit,Rest,Sent). /*ATNs*/ /*Sentence ATN*/ arc(sentence,start,a,nounphrase,nt). arc(sentence,a,b,verb,nt). arc(sentence,b,c,nounphrase,nt). arc(sentence,c,finish,stop_mark,nt). /*nounphrase ATN*/ arc(nounphrase,start,a,determiner,nt). arc(nounphrase,a,finish,noun,nt). arc(nounphrase,a,a,adjective,nt). arc(nounphrase,start,finish,proper_noun,nt). /*verb ATN*/ arc(verb,start,finish,is,t). arc(verb,start,finish,kills,t). arc(verb,start,finish,kisses,t). /*determiner ATN*/ arc(determiner,start,finish,a,t). arc(determiner,start,finish,an,t). arc(determiner,start,finish,the,t). /*noun ATN*/ arc(noun,start,finish,fascist,t). arc(noun,start,finish,dictator,t). /*adjective ATN*/ arc(adjective,start,finish,happy,t). arc(adjective,start,finish,fascist,t). arc(adjective,start,finish,italian,t). /*Proper Noun ATN*/ arc(proper_noun,start,finish,benito,t). /*Stop Mark ATN*/ arc(stop_mark,start,finish,(.),t). arc(stop_mark,start,finish,(?),t). arc(stop_mark,start,finish,(!),t). %% NEXT FILE %% /*qa*/ /*Question Answering system based on Eliza Alan Bundy 16.11.79 use with readin, eliza and infer*/ /*top level*/ qa :- read_in(Input), qa(Input). qa([bye,.]) :- !. qa(Input) :- translate(Input,Desc,Type), answer(Type,Desc), qa. /*translation*/ translate(Input,Desc,Type) :- sm_triple(S,D,Type), match(Input,S,off,Subst), replace1(Subst,D,Desc). /*replace variables by phrases in description*/ replace1(Subst,Word,Word) :- (atomic(Word); var(Word)), !. replace1(Subst,?Var,Phrase) :- !, member(Phrase/Var,Subst). replace1(Subst,D,Desc) :- D =.. [Sym|Args], not(Args = []), !, maplist(replace1(Subst),Args,NewArgs), Desc =.. [Sym|NewArgs]. /*answer writer on basis of type and description*/ answer(assertion,Desc) :- assert_fact(Desc), writef('ok\n',[]). answer(rule-assertion,(Ant->Consq)) :- assert(backward_rule(Ant,Consq)), writef('asserting rule %t implies %t \n',[Ant,Consq]), writef('ok\n',[]). answer(yes/no-question,Desc) :- (infer(Desc) -> writef('yes\n',[]); writef('dont know\n',[]) ). answer(wh-question,Desc) :- variables(Desc,Vars), (infer(Desc) -> checklist(print_list,Vars); writef('dont know\n',[]) ). /*stimulus meaning table*/ sm_triple([all,?p,are,?q,.],([?p,X] -> [?q,X]),rule-assertion). sm_triple([is,?t,?p,?],[?p,?t],yes/no-question). sm_triple([who,is,a,?p,?q,?],[?p,X] & [?q,X],wh-question). sm_triple([?t,is,?p,.],[?p,?t],assertion). %% NEXT FILE %% /*parse*/ /*acceptor and parser for sentences from ATN Alan Bundy 29.11.79 use with readin*/ /*Acceptor Top Level*/ accept :- read_in(Text), accept(Text). accept(Text) :- accept_part(Text,sentence,start,[]). /*Accept part of a sentence*/ accept_part(Text,ATN,finish,Text) :- !. accept_part([Word|Rest],ATN,start,Rest) :- arc(ATN,start,finish,Word,t). accept_part(Text,ATN,Node,Rest) :- arc(ATN,Node,Next,SubATN,nt), accept_part(Text,SubATN,start,Text1), accept_part(Text1,ATN,Next,Rest). /*Parse top level*/ parse :- read_in(Text), parse(Text,Tree), print_tree(0,Tree). parse(Text,Tree) :- parse_part(Text,sentence,start,[],Trees), Tree =.. [sentence|Trees]. /*parse part of text*/ parse_part(Text,ATN,finish,Text,[]) :- !. parse_part([Word|Rest],ATN,start,Rest,[Word]) :- arc(ATN,start,finish,Word,t). parse_part(Text,ATN,Node,Rest,[SubTree|Trees]) :- arc(ATN,Node,Next,SubATN,nt), parse_part(Text,SubATN,start,Text1,SubTrees), SubTree =.. [SubATN|SubTrees], parse_part(Text1,ATN,Next,Rest,Trees). /*print a syntax tree*/ print_tree(N,Tip) :- atomic(Tip), !, indent_write(N,Tip). print_tree(N,Tree) :- Tree =.. [Node|SubTrees], indent_write(N,Node), N1 is N+1, checklist(print_tree(N1),SubTrees). /*write indented line*/ indent_write(N,Text) :- N5 is 5*N, tab(N5), write(Text), nl. /*ATNs*/ /*Sentence ATN*/ arc(sentence,start,a,nounphrase,nt). arc(sentence,a,b,verb,nt). arc(sentence,b,c,nounphrase,nt). arc(sentence,c,finish,stop_mark,nt). /*nounphrase ATN*/ arc(nounphrase,start,a,determiner,nt). arc(nounphrase,a,finish,noun,nt). arc(nounphrase,a,a,adjective,nt). arc(nounphrase,start,finish,proper_noun,nt). /*verb ATN*/ arc(verb,start,finish,is,t). arc(verb,start,finish,kills,t). arc(verb,start,finish,kisses,t). /*determiner ATN*/ arc(determiner,start,finish,a,t). arc(determiner,start,finish,an,t). arc(determiner,start,finish,the,t). /*noun ATN*/ arc(noun,start,finish,fascist,t). arc(noun,start,finish,dictator,t). arc(noun,start,finish,italian,t). /*adjective ATN*/ arc(adjective,start,finish,friendly,t). arc(adjective,start,finish,misunderstood,t). arc(adjective,start,finish,happy,t). arc(adjective,start,finish,fascist,t). arc(adjective,start,finish,italian,t). /*Proper Noun ATN*/ arc(proper_noun,start,finish,benito,t). arc(proper_noun,start,finish,sophie,t). /*Stop Mark ATN*/ arc(stop_mark,start,finish,(.),t). arc(stop_mark,start,finish,(?),t). arc(stop_mark,start,finish,(!),t). %% NEXT FILE %% Utilities package Prolog-10 version 3 | ?- [winst1,isol]. winst1 consulted 2230 words 0.90 sec. isol consulted 1610 words 0.45 sec. yes | ?- winston(isol). Please give me an example of a isol |: isol1. Please give me an example or near miss of a isol. |: isol2. Is this example (yes./no.)? |: no. This limits my idea of isol. Please give me an example or near miss of a isol. |: isol3. Is this example (yes./no.)? |: no. This limits my idea of isol. Please give me an example or near miss of a isol. |: isol4. Is this example (yes./no.)? |: no. This limits my idea of isol. Please give me an example or near miss of a isol. |: isol5. Is this example (yes./no.)? |: no. This limits my idea of isol. Please give me an example or near miss of a isol. |: isol6. Is this example (yes./no.)? |: no. [ Execution aborted ] | ?- grey(isol). Grey areas in isol are: define([plato1,expr_at([1,2],plato2)],occurtree,[],[2,1]) define([expr_at([2],plato2),expr_at([2,2],plato3)],simtree,[],[2]) define([sym_at([1],plato2),sym([2],plato3)],simtree,[],[1,2]) yes | ?- winston1(isol). Please give me an example or near miss of a isol. |: isol6. Is this example (yes./no.)? |: no. This limits my idea of isol. Please give me an example or near miss of a isol. |: isol7. Is this example (yes./no.)? |: no. This limits my idea of isol. Please give me an example or near miss of a isol. |: isol8. Is this example (yes./no.)? |: no. This limits my idea of isol. I have learnt the concept of isol now. yes | ?- grey(isol). Grey areas in isol are: yes | ?- core 51712 (23552 lo-seg + 28160 hi-seg) heap 18432 = 14955 in use + 3477 free global 1218 = 16 in use + 1202 free local 1024 = 16 in use + 1008 free trail 511 = 0 in use + 511 free 22.49 sec. for 25 GCs gaining 46683 words 1.98 sec. for 12 local shifts and 110 trail shifts 38.49 sec. runtime %% NEXT FILE %% Sample of Session with Prolog Winston | ?- winston(arch). Please give me an example of a arch |: arch1. Please give me an example or near miss of a arch. |: arch2. Is this example (yes./no.)? |: yes. This is a new sort of arch. Please give me an example or near miss of a arch. |: arch3. Is this example (yes./no.)? |: yes. This is a new sort of arch. Please give me an example or near miss of a arch. |: archn1. Is this example (yes./no.)? |: no. This limits my idea of arch. Please give me an example or near miss of a arch. |: archn2. Is this example (yes./no.)? |: no. This limits my idea of arch. Please give me an example or near miss of a arch. |: archn3. Is this example (yes./no.)? |: no. I have seen one of these before. Please give me an example or near miss of a arch. | ?- grey(arch). Grey areas in arch are: define([plato1],shapetree,[],[1,2]) define([plato2],shapetree,[],[1]) define([plato3],shapetree,[],[1,2]) define([plato1,plato2],touchtree,[],[2]) define([plato2,plato1],touchtree,[],[2]) define([plato3,plato1],touchtree,[],[1]) define([plato2,plato3],touchtree,[],[2]) define([plato3,plato2],touchtree,[],[2]) define([plato1],orienttree,[],[2]) define([plato2],orienttree,[],[1]) define([plato3],orienttree,[],[2]) define([plato1,plato3],directiontree,[],[1]) define([plato3,plato2],supporttree,[],[1]) %% NEXT FILE %% | ?- winston(arch). Please give me an example of a arch |: arch1. Please give me an example or near miss of a arch. |: arch2. Is this example (yes./no.)? |: yes. This is a new sort of arch. Please give me an example or near miss of a arch. |: arch3. Is this example (yes./no.)? |: yes. This is a new sort of arch. Please give me an example or near miss of a arch. |: archn1. Is this example (yes./no.)? |: no. This limits my idea of arch. Please give me an example or near miss of a arch. |: archn2. Is this example (yes./no.)? |: no. Please give me an example or near miss of a arch. |: archn3. Is this example (yes./no.)? |: no. This limits my idea of arch. Please give me an example or near miss of a arch. |: Is this example (yes./no.)? |: [ Execution aborted ] | ?- grey(arch). Grey areas in arch are: define([lp(plato1)],shapetree,[],[1,2]) define([rp(plato1)],shapetree,[],[1,2]) define([tm(plato1)],shapetree,[],[1]) define([lp(plato1)],orienttree,[],[2]) define([rp(plato1)],orienttree,[],[2]) define([tm(plato1)],orienttree,[],[1]) define([lp(plato1),rp(plato1)],directiontree,[],[1]) define([rp(plato1),tm(plato1)],supporttree,[],[1]) define([lp(plato1),tm(plato1)],touchtree,[],[2]) define([rp(plato1),tm(plato1)],touchtree,[],[2]) yes %% NEXT FILE %% /*arch.prb Winston arch domain Alan Bundy 5.12.80 use with winston */ /* space of description trees */ space(arch,[shapetree,touchtree,orienttree,directiontree,supporttree]). /* description tree */ tree(shapetree,1,shape(prism(wedge,block),pyramid)). tree(touchtree,2,touchrel(separate,touch(marries,abuts))). default(touchtree,separate). % default predicate tree(orienttree,1,orientation(lying,standing)). tree(directiontree,2,direction(leftof,rightof)). tree(supporttree,2,undef(supports,unsupports)). /* Examples and near misses */ specimen(arch1, [block(a), block(b), block(c), standing(a), standing(b), lying(c), leftof(a,b), supports(a,c), supports(b,c), marries(a,c), marries(c,a), marries(b,c), marries(c,b)]). specimen(arch2, [block(a), block(b), wedge(c), standing(a), standing(b), lying(c), leftof(a,b), supports(a,c), supports(b,c), marries(a,c), marries(c,a), marries(b,c), marries(c,b)]). specimen(arch3, [block(a), block(b), block(c), standing(a), standing(b), lying(c), leftof(a,b), supports(a,c), supports(b,c), abuts(a,c), abuts(c,a), abuts(b,c), abuts(c,b)]). specimen(archn1, [block(a), block(b), block(c), standing(a), standing(b), lying(c), leftof(a,b), supports(a,c), supports(b,c), marries(a,c), marries(c,a), marries(b,c), marries(c,b), marries(a,b), marries(b,a)]). specimen(archn2, [block(a), block(b), block(c), standing(a), standing(b), lying(c), leftof(a,b), marries(a,c), marries(c,a), marries(b,c), marries(c,b)]). specimen(archn3, [block(a), block(b), block(c), standing(a), standing(b), lying(c), leftof(a,b)]). %% NEXT FILE %% /*arch1.prb Winston arch domain Alan Bundy 5.12.80 use with winston version with functions */ /* description trees */ tree(shapetree,1,shape(prism(wedge,block),pyramid)). tree(touchtree,2,touchrel(separate,touch(marries,abuts))). default(touchtree,separate). % default predicate tree(orienttree,1,orientation(lying,standing)). tree(directiontree,2,direction(leftof,rightof)). tree(supporttree,2,undef(supports,unsupports)). /* Examples and near misses */ specimen(arch1, [block(lp(a)), block(rp(a)), block(tm(a)), standing(lp(a)), standing(rp(a)), lying(tm(a)), leftof(lp(a),rp(a)), supports(lp(a),tm(a)), supports(rp(a),tm(a)), marries(lp(a),tm(a)), marries(rp(a),tm(a)) ] ). specimen(arch2, [block(lp(a)), block(rp(a)), wedge(tm(a)), standing(lp(a)), standing(rp(a)), lying(tm(a)), leftof(lp(a),rp(a)), supports(lp(a),tm(a)), supports(rp(a),tm(a)), marries(lp(a),tm(a)), marries(rp(a),tm(a)) ] ). specimen(arch3, [block(lp(a)), block(rp(a)), block(tm(a)), standing(lp(a)), standing(rp(a)), lying(tm(a)), leftof(lp(a),rp(a)), supports(lp(a),tm(a)), supports(rp(a),tm(a)), abuts(lp(a),tm(a)), abuts(rp(a),tm(a)) ] ). specimen(archn1, [block(lp(a)), block(rp(a)), block(tm(a)), standing(lp(a)), standing(rp(a)), lying(tm(a)), leftof(lp(a),rp(a)), supports(lp(a),tm(a)), supports(rp(a),tm(a)), marries(lp(a),tm(a)), marries(rp(a),tm(a)), marries(lp(a),rp(a)) ] ). specimen(archn2, [block(lp(a)), block(rp(a)), block(tm(a)), standing(lp(a)), standing(rp(a)), lying(tm(a)), leftof(lp(a),rp(a)), marries(lp(a),tm(a)), marries(rp(a),tm(a)) ] ). specimen(archn3, [block(lp(a)), block(rp(a)), block(tm(a)), standing(lp(a)), standing(rp(a)), lying(tm(a)), leftof(lp(a),rp(a))]). %% NEXT FILE %% /*winst Rational Reconstruction of Winston Learning Program Alan Bundy 1.12.80 Version for functions */ /* Top Level Program - learn new concept */ /* ------------------------------------- */ /*First time only accept an example */ winston(Concept) :- !, writef('Please give me an example of a %t \n', [Concept]), read(Ex), nl, make_rec(Concept,Ex,EObjs,ERec), maplist(gensym1(plato),EObjs,CObjs), make_subst(EObjs,CObjs,Subst), subst(Subst,ERec,CRec), maplist(add_ups,CRec,CDefn), assert(definition(Concept,CObjs,CDefn)), winston1(Concept). /* Is grey area in definition eliminated? */ winston1(Concept) :- definition(Concept,CObjs,CDefn), checklist(same,CDefn), !, writef('I have learnt the concept of %t now. \n', [Concept]). /*Subsequently accept either examples or near misses */ winston1(Concept) :- !, writef('Please give me an example or near miss of a %t. \n', [Concept]), read(Ex), nl, writef('Is this example (yes./no.)? \n',[]), read(YesNo), nl, learn(Concept,Ex,YesNo), winston1(Concept). /* add default upper bounds in concept record */ add_ups(record(Args,Name,Posn), define(Args,Name,[],Posn)). /* slight modify to gensym, so it can be used in maplist */ gensym1(Prefix,_,NewConst) :- !, gensym(Prefix,NewConst). /* are upper and lower bound of concept definition the same? */ same(define(Args,Name,Posn,Posn)). /* learn from this example or near miss */ learn(Concept, Example, YesNo) :- !, definition(Concept,CObjs,CDefn), make_rec(Concept,Example,EObjs,ERec), classify(CObjs,EObjs,CDefn,ERec,Diff,Verdict), learn1(Concept,Diff,YesNo,Verdict). /* Make records from list of relations */ /* ------------------------------------ */ make_rec(Concept,Example,EObjs,ERec) :- !, specimen(Example,Relns), maplist(consts_in,Relns,CL), flatten(CL,EObjs), maplist(convert,Relns,ERec). /* Find all constants in terms */ consts_in([],[]). consts_in(N,[]) :- integer(N), !. consts_in(Const,[Const]) :- atom(Const), !. consts_in(Exp,Consts) :- Exp =.. [Sym|Args], maplist(consts_in,Args,CL), flatten(CL,Consts). /*Flatten List */ flatten([],[]). flatten([Hd|Tl],Ans):- flatten(Tl,Rest), union(Hd,Rest,Ans). /* Convert input relation style into internal representation as predicate tree */ convert(Reln, record(Args,Name,ExPosn)) :- Reln =.. [Pred|Args], length(Args,N), tree(Name,N,Tree), position(Pred,Tree,ExPosn). /* Find Position of Node in Tree */ position(Node,Tree,[]) :- Tree =.. [Node|SubTrees]. position(Node,Tree,[N|Posn]) :- Tree =.. [Root|SubTrees], nth_el(N,SubTrees,SubTree), position(Node,SubTree,Posn). /* find nth element of list */ nth_el(1,[Hd|Tl],Hd). nth_el(N,[Hd|Tl],El) :- nth_el(PN,Tl,El), N is PN + 1. /* Is this example, non-example or in grey area, by my definition? */ /* --------------------------------------------------------------- */ classify(CObjs,EObjs,CDefn,ERec,BestDiff,Verdict) :- !, findall(Diff, make_diff(CObjs,EObjs,CDefn,ERec,Diff), Diffs), best(Diffs,BestDiff), verdict(BestDiff,Verdict). /* Find the difference between example and concept */ make_diff(CObjs,EObjs,CDefn,ERec,Diff) :- !, perm(EObjs,EObjs1), make_subst(EObjs1,CObjs,Subst), subst(Subst,ERec,ERec1), pair_off(CDefn,ERec1,Diff). /*Pair off concept definition and example record to make differences */ pair_off([],[],[]) :- !. pair_off([],ERec,Diff) :- !, maplist(new_defn,ERec,Diff). pair_off(CDefn,[],Diff) :- !, maplist(extra_rec,CDefn,Diff). pair_off([define(Args,Name,UpPosn,LowPosn) | CDefn], ERec, [differ(Args,Name,UpPosn,ExPosn,LowPosn,Verdict) | Diff]) :- select(record(Args,Name,ExPosn),ERec,Rest), !, compare(UpPosn,ExPosn,LowPosn,Verdict), pair_off(CDefn,Rest,Diff). /* invent new bits of definition as necessary */ new_defn(record(Args,Name,ExPosn), differ(Args,Name,[],ExPosn,DfPosn,Verdict)) :- default_posn(Name,DfPosn), compare([],ExPosn,DfPosn,Verdict). /* invent extra bits of example record as necessary */ extra_rec(define(Args,Name,UpPosn,LowPosn), differ(Args,Name,UpPosn,DfPosn,LowPosn,Verdict)) :- default_posn(Name,DfPosn), compare(UpPosn,DfPosn,LowPosn,Verdict). /* Find position of default predicate on tree */ default_posn(TreeName,Posn) :- default(TreeName,Pred), !, tree(TreeName,_,Tree), position(Pred,Tree,Posn). default_posn(TreeName,[]). /* Compare positions in tree to give verdict */ compare(U,E,L,yes) :- append(L,_,E), !. compare(U,E,L,grey) :- append(U,_,E), !. compare(U,E,L,no) :- !. /* Find best difference and return it */ best(Diffs,Diff) :- !, maplist(score,Diffs,Scores), lowest(Diffs,Scores,Diff,Score). /* Return difference with lowest score */ lowest([Diff],[Score],Diff,Score) :- !. lowest([Diff1|Diffs], [Score1|Scores], Diff2, Score2) :- lowest(Diffs,Scores,Diff2,Score2), Score2 (1/x)>m))), Ans). %% NEXT FILE %% yes | ?- test1(A). A = a*f1(c,b,a)f2+b*f1(c,b,a)+c=0 yes | ?- test2(A). A = (abs(x)=1/x>m yes | ?- core 60416 (31232 lo-seg + 29184 hi-seg) heap 26112 = 23809 in use + 2303 free global 1177 = 16 in use + 1161 free local 1024 = 16 in use + 1008 free trail 511 = 0 in use + 511 free 1.00 sec. runtime %% NEXT FILE %% /* DIVIDE. Test example for SEMANT and MODEL Clauses and Model for not divides example (see notes p124) Alan Bundy 22.6.81 */ /* Clauses */ clause(right, [not_div(X*Z,Y)], [not_div(X,Y)], input). % Input clauses clause(left, [not_div(Z*X,Y)], [not_div(X,Y)], input). clause(thirty, [equal(30,2*3*5)], [], input). clause(hypothesis, [not_div(5,a)], [], input). clause(conclusion, [], [not_div(30,a)], topclause). % Top clause /* Models */ /* arith2 */ interpretation(arith2). % arith2 is an interpretation interpret(arith2, a, 2). % meaning of a interpret(arith2, not_div(X,Y), false) :- % meaning of not_div 0 is Y mod X, !. interpret(arith2, not_div(X,Y), true). interpret(arith2, equal(X,Y), true) :- % meaning of equal X =:= Y, !. interpret(arith2, equal(X,Y), false). interpret(arith2, X*Y, Z) :- Z is X*Y. % meaning of * /* arith3 */ interpretation(arith3). % arith3 is an interpretation interpret(arith3, a, 3). % meaning of a interpret(arith3, not_div(X,Y), false) :- % meaning of not_div 0 is Y mod X, !. interpret(arith3, not_div(X,Y), true). interpret(arith3, equal(X,Y), true) :- % meaning of equal X =:= Y, !. interpret(arith3, equal(X,Y), false). interpret(arith3, X*Y, Z) :- Z is X*Y. % meaning of * %% NEXT FILE %% /* MODEL. How to evaluate a clause in an interpretation (provided it is variable free!!) use with SEMANT DIVIDE contains test examples Alan Bundy 22.6.81 */ /* Vet the clause in any interpretations */ vet(Clause) :- not satisfiable(Clause). % Clause has no model /* Clause is satisfiable in some Interpretation */ satisfiable(Clause) :- interpretation(Interp), % If there is an interpretation model(Interp,Clause), % in which Clause is true writef('%t rejected by %t\n\n',[Clause,Interp]). % tell user /* Interpretation is a model of a Clause */ model(Interp, Clause) :- clause(Clause,Consequent,Antecedent,_), % Get Clause definition checklist(is_true(Interp), Consequent), % Check all lhs literals are true checklist(is_false(Interp), Antecedent). % and all rhs ones are false /* Evaluate expression in Interpretation */ evaluate( Interp, Integer, Integer ) :- integer(Integer), !. % integers represent themselves evaluate( Interp, Constant, Value ) :- % other constants have values assigned atom(Constant), !, interpret(Interp, Constant, Value). evaluate( Interp, Complex, Value ) :- Complex =.. [Sym | Args], !, % recurse on arguments of maplist(evaluate(Interp), Args, Vals), % complex terms Complex1 =.. [Sym | Vals], % then interpret topmost interpret(Interp, Complex1, Value). % symbol /* Evaluation of clause (hacks for checklist) */ is_true(Interp, Literal) :- evaluate(Interp, Literal, true). is_false(Interp, Literal) :- evaluate(Interp, Literal, false). %% NEXT FILE %% /* EQUAL. Test example for BREADT and HEURIS. Symmetry can be inferred from reflexivity and twisted transitivity (notes p62). Alan Bundy 22.6.81 */ clause(hypothesis, [equal(x,y)], [], input ). % Input clauses clause(reflexive, [equal(X,X)], [], input ). clause(twisted, [equal(U,W)], [equal(U,V), equal(W,V)], input ). clause(goal, [], [equal(y,x)], topclause). % Top clause %% NEXT FILE %% yes | ?- go. af(2*0)*5+b*0 rewritten to af0*5+b*0 by rule 1 af0*5+b*0 rewritten to af0*5+0 by rule 1 af0*5+0 rewritten to 1*5+0 by rule 3 1*5+0 rewritten to 5+0 by rule 2 5+0 rewritten to 5 by rule 4 Normal Form is 5 5+0 rewritten to 5 by rule 4 1*5+0 rewritten to 1*5 by rule 4 1*5 rewritten to 5 by rule 2 Normal Form is 5 1*5 rewritten to 5 by rule 2 1*5+0 rewritten to 5+0 by rule 2 af0*5+0 rewritten to af0*5 by rule 4 af0*5 rewritten to 1*5 by rule 3 1*5 rewritten to 5 by rule 2 Normal Form is 5 1*5 rewritten to 5 by rule 2 af0*5 rewritten to 1*5 by rule 3 af0*5+0 rewritten to 1*5+0 by rule 3 af0*5+b*0 rewritten to 1*5+b*0 by rule 3 1*5+b*0 rewritten to 1*5+0 by rule 1 1*5+0 rewritten to 5+0 by rule 2 5+0 rewritten to 5 by rule 4 Normal Form is 5 5+0 rewritten to 5 by rule 4 1*5+0 rewritten to 1*5 by rule 4 1*5 rewritten to 5 by rule 2 Normal Form is 5 1*5 rewritten to 5 by rule 2 1*5+0 rewritten to 5+0 by rule 2 1*5+b*0 rewritten to 5+b*0 by rule 2 5+b*0 rewritten to 5+0 by rule 1 5+0 rewritten to 5 by rule 4 Normal Form is 5 5+0 rewritten to 5 by rule 4 5+b*0 rewritten to 5+0 by rule 1 1*5+b*0 rewritten to 1*5+0 by rule 1 af0*5+b*0 rewritten to af0*5+0 by rule 1 af(2*0)*5+b*0 rewritten to af(2*0)*5+0 by rule 1 af(2*0)*5+0 rewritten to af0*5+0 by rule 1 af0*5+0 rewritten to 1*5+0 by rule 3 1*5+0 rewritten to 5+0 by rule 2 5+0 rewritten to 5 by rule 4 Normal Form is 5 5+0 rewritten to 5 by rule 4 1*5+0 rewritten to 1*5 by rule 4 1*5 rewritten to 5 by rule 2 Normal Form is 5 1*5 rewritten to 5 by rule 2 1*5+0 rewritten to 5+0 by rule 2 af0*5+0 rewritten to af0*5 by rule 4 af0*5 rewritten to 1*5 by rule 3 1*5 rewritten to 5 by rule 2 Normal Form is 5 1*5 rewritten to 5 by rule 2 af0*5 rewritten to 1*5 by rule 3 af0*5+0 rewritten to 1*5+0 by rule 3 af(2*0)*5+0 rewritten to af(2*0)*5 by rule 4 af(2*0)*5 rewritten to af0*5 by rule 1 af0*5 rewritten to 1*5 by rule 3 1*5 rewritten to 5 by rule 2 Normal Form is 5 1*5 rewritten to 5 by rule 2 af0*5 rewritten to 1*5 by rule 3 af(2*0)*5 rewritten to af0*5 by rule 1 af(2*0)*5+0 rewritten to af0*5+0 by rule 1 af(2*0)*5+b*0 rewritten to af0*5+b*0 by rule 1 no | ?- core 60416 (31232 lo-seg + 29184 hi-seg) heap 26112 = 23454 in use + 2658 free global 1175 = 16 in use + 1159 free local 1024 = 16 in use + 1008 free trail 511 = 0 in use + 511 free 0.00 sec. for 1 trail shift 3.02 sec. runtime %% NEXT FILE %% /* UNIFY. Unification procedure for first order logic (with occurs check) See p80 of Artificial Mathematicians. Alan Bundy 10.7.81 */ /* Top Level */ unify(Exp1, Exp2, Subst) :- % To unify two expressions unify(Exp1, Exp2, true, Subst). % Start with empty substitution /* Unify with output and input substitutions */ unify(Exp, Exp, Subst, Subst). % If expressions are identical, succeedd unify(Exp1, Exp2, OldSubst, AnsSubst) :- % otherwise disagree(Exp1,Exp2,T1,T2), % find first disagreement pair make_pair(T1,T2,Pair), % make a substitution out of them, if pos combine(Pair,OldSubst,NewSubst), % combine this with input subst subst(Pair,Exp1,NewExp1), % apply it to expressions subst(Pair,Exp2,NewExp2), unify(NewExp1,NewExp2,NewSubst,AnsSubst). % and recurse /* Find Disagreement Pair */ disagree(Exp1,Exp2,Exp1,Exp2) :- Exp1 =.. [Sym1|_], Exp2 =.. [Sym2|_], % If exps have different Sym1 \== Sym2, !. % function symbol, then succeed disagree(Exp1,Exp2,T1,T2) :- % otherwise Exp1 =.. [Sym|Args1], Exp2 =.. [Sym|Args2], % find their arguments find_one(Args1,Args2,T1,T2). % and recurse /* Find first disagreement pair in argument list */ find_one( [Hd | Tl1], [Hd | Tl2],T1,T2) :- !, % If heads are identical then find_one(Tl1,Tl2,T1,T2). % find disagreement in rest of list find_one( [Hd1 | Tl1], [Hd2 | Tl2],T1,T2) :- disagree(Hd1,Hd2,T1,T2), !. % else find it in heads. /* Try to make substitution out of pair of terms */ make_pair(T1,T2,T1=T2) :- % T1=T2 is a suitable substitution is_variable(T1), % if T1 is a variable and free_of(T1,T2). % T2 is free of T1 make_pair(T1,T2,T2=T1) :- is_variable(T2), % or if T2 is a variable and free_of(T2,T1). % T1 is free of T2 /* By convention: x,y,z,u,v and w are the only variables */ is_variable(u). is_variable(v). is_variable(w). is_variable(x). is_variable(y). is_variable(z). /* T is free of X */ free_of(X,T) :- occ(X,T,0). % if X occurs 0 times in T /* Combine new substitution pair with old substitution */ combine(Pair, OldSubst, NewSubst) :- mapand(update(Pair),OldSubst,Subst1), % apply new pair to old subst check_overlap(Pair,Subst1,NewSubst). % and delete ambiguous assigments /* Apply new pair to old substitution */ update(Pair, Y=S, Y=S1) :- % apply new pair to rhs of old subst subst(Pair,S,S1). /* If X is bound to something already then ignore it */ check_overlap(X=T,Subst,Subst) :- % Ignore X=T memberchk(X=S,Subst), !. % if there already is an X=S check_overlap(Pair,Subst,Pair & Subst). % otherwise don't /* MINI-PROJECTS 1. Simplify unify to a one way matcher, as per p76 of 'Artificial Mathematicians'. 2. Generalize Unify to a simultaneous unifier of a set of expressions, (gen_unify) as per p80 of 'Artificial Mathematicians'. 3. Build the associativity axiom into unify (assoc_unify), as per p82 of 'Artificial Mathematicians'. */ %% NEXT FILE %% /* SIMPLE. Using PROLOG as a theorem prover: An equality axioms example. Try goal 'equal(y,x).'. Alan Bundy 16.6.81 */ equal(x,y). % The Hypothesis equal(X,X). % The Reflexive Axiom equal(U,W) :- equal(U,V), equal(W,V). % The Twisted Transitivity Axiom /* MINI-PROJECTS 1. Try goal ?- equal(y,x). 2. Experiment by switching the order of the above axioms and trying the same goal. What sort of bad behaviour emerges? How could it be avoided? 3. Experiment with different axioms, e.g. the group theory example from p92 of 'Artificial Mathematicians'. */ %% NEXT FILE %% /* SEMANT. A Depth First Theorem Prover with vetting by use of interpretations and incorporating input restriction. Use with MODEL DIVIDE contains test example Alan Bundy 22.6.81 */ /* Top Goal */ go :- clause(Goal,_,_,topclause), % Find the top clause semantic(Goal). % and away you go /* Depth first theorem prover */ semantic(Old) :- successor(Old,New), % Find a successor to the current clause vet(New), % check that it is unsatisfiable semantic(New). % and recurse /* Clause is a resolvant of Current with an input clause */ successor(Current,Clause) :- clause(Input,_,_,input), % Pick an input clause ( resolve(Current,Input,Clause) ; % resolve it with the resolve(Input,Current,Clause) ; % current clause paramodulate(Current,Input,Clause) ; % or paramodulate it paramodulate(Input,Current,Clause) ). /* Resolution Step */ resolve( Parent1, Parent2, Resolvant) :- clause(Parent1, Consequent1, Antecedent1, _), % Get the two parents clause(Parent2, Consequent2, Antecedent2, _), select(Literal, Consequent1, RestConse1), % Select a common literal select(Literal, Antecedent2, RestAnte2), % and return the rest append(RestConse1, Consequent2, Consequent), % Join the odd bits together append(Antecedent1, RestAnte2, Antecedent), record_clause(Consequent,Antecedent,Resolvant). % Record the clause /* Paramodulation Step */ paramodulate( Parent1, Parent2, Paramodulant ) :- clause(Parent1, Consequent1, Antecedent1, _), % Get the two parents clause(Parent2, Consequent2, Antecedent2, _), select(equal(T,S), Consequent1, RestConse1), % select an equation replace(T,S,Consequent2,Antecedent2,NewConse2,NewAnte2),% put it in the other clause append(RestConse1,NewConse2,Consequent), % join the odd bits together append(Antecedent1,NewAnte2,Antecedent), record_clause(Consequent,Antecedent,Paramodulant). %record the clause /* Replace T by S (or S by T) in clause */ replace(T,S,OldConse,OldAnte,NewConse,OldAnte) :- % replace T by S in replace1(T,S,OldConse,NewConse). % the consequent replace(T,S,OldConse,OldAnte,OldConse,NewAnte) :- % or T by S in replace1(T,S,OldAnte,NewAnte). % the antecedent replace(S,T,OldConse,OldAnte,NewConse,OldAnte) :- % or S by T in replace1(S,T,OldConse,NewConse). % the consequent replace(S,T,OldConse,OldAnte,OldConse,NewAnte) :- % or S by T in replace1(S,T,OldAnte,NewAnte). % the antecedent /* Replace T by S in Old to get New */ replace1(T,S,Old,New) :- some(replace2(T,S),Old,New). % replace one of the literals replace2(T,S,T,S). % replace this occurence replace2(T,S,Old,New) :- % replace one of the arguments Old =.. [Sym | OldArgs], % get the arguments replace1(T,S,OldArgs,NewArgs), % replace one New =.. [Sym | NewArgs]. % put it all together again /* Record Existence of New Clause */ record_clause([],[],empty) :- % test for empty clause writef('Success! Empty Clause Found\n\n'), !, % tell user abort. % and stop record_clause(Consequent,Antecedent,Name) :- % test for loop clause(Name,Consequent,Antecedent,_), !. % i.e. clause with same innards record_clause(Consequent,Antecedent,Name) :- !, % record new clause gensym(clause,Name), % make up new name assert(clause(Name,Consequent,Antecedent,new)), % assert clause writef('%t is name of new resolvant %l <- %l \n\n', [Name,Consequent,Antecedent]). % tell user /* Apply Pred to just one element of list */ some(Pred, [Hd1 | Tl], [Hd2 | Tl]) :- apply(Pred, [Hd1,Hd2]). % apply it to this one some(Pred, [Hd | Tl1], [Hd | Tl2]) :- some( Pred, Tl1, Tl2). % or one of the others /* MINI-PROJECTS 1. Try out theorem prover with the arithmetic clauses and models of file DIVIDE. 2. Experiment with some clauses and models of your own devising (See chapter 10 for some ideas). 3. Modify the theorem prover so that it works by breadth first search (Compare with file BREADT). 4. Modify the theorem prover so that it works by heuristic search (Compare with file HEURIS). */ %% NEXT FILE %% /* REWRIT. Simple depth first search rewrite rule system see Artificial Mathematicians p 104. Use with UTIL Alan Bundy 10.7.81 */ /* Find Normal Form of Expression */ normalize(Expression, NormalForm) :- % To put an expression in normal form: rewrite(Expression, Rewriting), % Rewrite it once normalize(Rewriting, NormalForm). % and recurse normalize(Expression, Expression) :- % The expression is in normal form not rewrite(Expression, _). % if it cannot be rewritten /* Rewrite Rule of Inference */ rewrite(Expression, Rewriting) :- % To rewrite Expression rule(Name,LHS, RHS), % get a rule LHS => RHS replace(LHS, RHS, Expression, Rewriting), % replace LHS by RHS writef('%t rewritten to %t by rule %t\n', [Expression,Rewriting,Name]). /* Replace single occurrence of T by S in Old to get New */ replace(T,S,T,S). % replace this occurence replace(T,S,Old,New) :- % replace one of the arguments Old =.. [Sym | OldArgs], % get the arguments some(replace(T,S),OldArgs,NewArgs), % replace one New =.. [Sym | NewArgs]. % put it all together again /* Apply Pred to just one element of list */ some(Pred, [Hd1 | Tl], [Hd2 | Tl]) :- apply(Pred, [Hd1,Hd2]). % apply it to this one some(Pred, [Hd | Tl1], [Hd | Tl2]) :- some( Pred, Tl1, Tl2). % or one of the others /* Some rules */ rule(1,X*0, 0). % Algebraic Simplification rules rule(2,1*X, X). rule(3,Xf0, 1). rule(4,X+0, X). /* A Typical Problem */ go :- normalize( (af(2*0))*5 + b*0, NormalForm), writef('Normal Form is %t\n\n', [NormalForm]), fail. /* MINI-PROJECTS 1. Try out the system with the arithmetic rules given above. 2. Experiment with some rules of your own devising (Suggestions can be found in chapter 9 and section 5.2 of 'Artificial Mathematicians'). 3. Modify the system so that it works by: (a) call by value, (b) call by name (See p107 of 'Artificial Mathematicians'). */ %% NEXT FILE %% /* SKOLEM. Skolem Normal Form Procedure (FORMUL contains test examples) Alan Bundy 17.3.79 */ /*operator declarations*/ :- op(400,xfy,;). % Disjunction :- op(300,xfy,<->). % Double Implication :-op(400,xfy,->). % Implication /*skolem normal form*/ skolem(Sentence,NormalForm) :- !, % Normal calling pattern skolem(Sentence,NormalForm,[],0). % assume no free vars and being asserted skolem(P <-> Q, (P1->Q1)&(Q1->P1),Vars,Par) :- !, % Double implication skolem(P,P1,Vars,Par), skolem(Q,Q1,Vars,Par). skolem(all(X,P),P1,Vars,0) :- !, % Universal quantification skolem(P,P1,[X|Vars],0). skolem(all(X,P),P2,Vars,1) :- !, % Universal quantification gensym(f,Fs), univ(Fs,Vars,F), % dual case subst(X=F,P,P1), skolem(P1,P2,Vars,1). skolem(some(X,P),P2,Vars,0) :- !, % Existential quantification gensym(f,Fs), univ(Fs,Vars,F), subst(X=F,P,P1), skolem(P1,P2,Vars,0). skolem(some(X,P),P1,Vars,1) :- !, % Existential quantification skolem(P,P1,[X|Vars],1). % dual case skolem(P->Q,P1->Q1,Vars,Par) :- !, % Implication opposite(Par,Par1), skolem(P,P1,Vars,Par1), skolem(Q,Q1,Vars,Par). skolem(P;Q,P1;Q1,Vars,Par) :- !, % Disjunction skolem(P,P1,Vars,Par), skolem(Q,Q1,Vars,Par). skolem(P&Q,P1&Q1,Vars,Par) :- !, % Conjunction skolem(P,P1,Vars,Par), skolem(Q,Q1,Vars,Par). skolem(not P,not P1,Vars,Par) :- !, % Negation opposite(Par,Par1), skolem(P,P1). skolem(Pred,Pred,Vars,Par) :- !. % Atomic formula /*opposite parities*/ opposite(0,1). opposite(1,0). /*univ - apply args to symbol*/ univ(Fs,Vars,F) :- !, F =.. [Fs|Vars]. /* MINI-PROJECTS 1. Try out on various formulae. 2. Modify the program to deal with bounded quantification, e.g. all_in(X,Set,P) - meaning, for all X in Set, P is true. 3. Build programs for putting formulae in: (a) Prenex Normal Form, (b) Conjunctive Normal Form, as per section 5.2 of 'Artificial Mathematicians'. You may wish to use file REWRIT. */ %% NEXT FILE %% /* BREADTH. A Breadth First Search Theorem Prover. EQUAL contains test example. Alan Bundy 16.6.81 */ /* Top Goal */ go :- breadth(0). /* Breadth First Search Strategy */ breadth(N) :- N1 is N+1, % Calculate new depth repeat(resolve(input,N,N1)), % Form all resolvants at that depth repeat(resolve(N,input,N1)), breadth(N1). % and recurse /* Repeat as many times as possible */ repeat(Goal) :- Goal, fail. % Keep trying and failing repeat(Goal). % and succeed only when you run out of things to do /* Resolution Step */ resolve( N1, N2, N ) :- find_clause(Parent1, Consequent1, Antecedent1, N1), % Find clauses at find_clause(Parent2, Consequent2, Antecedent2, N2), % appropriate depths select(Literal, Consequent1, RestConse1), % find a common literal select(Literal, Antecedent2, RestAnte2), % return leftovers append(RestConse1, Consequent2, Consequent), % cobble leftovers together append(Antecedent1, RestAnte2, Antecedent), record_clause(Consequent,Antecedent,N). % record new clause /* Record Existence of New Clause */ record_clause([],[],N) :- % test for empty clause writef('Success! Empty Clause Found\n\n'), !, % tell user abort. % and stop record_clause(Consequent,Antecedent,N) :- % test for loop find_clause(Name,Consequent,Antecedent,M), !. % i.e. clause with same innards record_clause(Consequent,Antecedent,N) :- !, % record new clause gensym(clause,Name), % make up new name assert(clause(Name,Consequent,Antecedent,N)), % assert clause writef('%t is name of new resolvant %l <- %l at depth %t\n\n', [Name,Consequent,Antecedent,N]). % tell user /* Find a clause at depth N */ find_clause(Name,Consequent,Antecedent,0) :- clause(Name,Consequent,Antecedent,topclause), !. find_clause(Name,Consequent,Antecedent,N) :- clause(Name,Consequent,Antecedent,N). /* MINI-PROJECTS 1. Try this theorem prover with the clauses of file EQUAL. 2. Experiment by making up some clauses of your own and trying them out. 3. Modify the theorem prover to print out the solution when it has found it. 4. Modify the theorem prover to remove the input restriction. 5. Modify the theorem prover to incorporate the literal selection restriction. 6. Build a depth first theorem prover along the same lines. */ %% NEXT FILE %% /* HEURIS. A Heurisitic Search Theorem Prover. EQUAL contains test example. Alan Bundy 19.6.81 */ /* Top Goal */ go :- clause(Goal,_,_,topclause), heuristic([Goal]). /* Heuristic Search Strategy */ heuristic(Fringe) :- pick_best(Fringe,Current,Rest), % Pick the clause with best score findall(Clause,successor(Current,Clause),NewClauses), % findall its successors append(Rest,NewClauses,NewFringe), % Put them on fringe heuristic(NewFringe). % and recurse /* Clause is a resolvant of Current with an input clause */ successor(Current,Clause) :- clause(Input,_,_,input), % Pick an input clause ( resolve(Current,Input,Clause) ; resolve(Input,Current,Clause) ). % resolve it with the current clause /* Resolution Step */ resolve( Parent1, Parent2, Resolvant) :- clause(Parent1, Consequent1, Antecedent1, N1), % Get the two parents clause(Parent2, Consequent2, Antecedent2, N2), select(Literal, Consequent1, RestConse1), % Select a common literal select(Literal, Antecedent2, RestAnte2), % and return the rest append(RestConse1, Consequent2, Consequent), % Join the odd bits together append(Antecedent1, RestAnte2, Antecedent), record_clause(Consequent,Antecedent,Resolvant). % Record the clause /* Record Existence of New Clause */ record_clause([],[],empty) :- % test for empty clause writef('Success! Empty Clause Found\n\n'), !, % tell the user abort. % and stop record_clause(Consequent,Antecedent,Name) :- % test for loop clause(Name,Consequent,Antecedent,M), !, fail. record_clause(Consequent,Antecedent,Name) :- !, % record new clause gensym(clause,Name), % make up a name evaluate(Consequent,Antecedent,N), % get score of clause assert(clause(Name,Consequent,Antecedent,N)), % assert clause writef('%t is name of new resolvant %l <- %l with score %t\n\n', [Name,Consequent,Antecedent,N]). % tell user /* Evaluation Function on Clauses (length of clause) */ evaluate(Consequent,Antecedent,Score) :- length(Consequent,C), % add length of rhs length(Antecedent,A), % to length of lhs Score is C+A. % to get clause length /* Pick clause with best score (i.e.lowest) */ pick_best([Hd|Tl],Choice,Rest) :- clause(Hd,_,_,N), % Get score of first clause pick_best(Tl,Hd,N,Choice,Rest). % and run down list remembering best so far pick_best([],Hd,N,Hd,[]). % When you get to the end return running score pick_best([Hd1|Tl1],Hd,N,Choice,[Hd3|Rest]) :- clause(Hd1,_,_,N1), % Get score of first clause compare(Hd,N,Hd1,N1,Hd2,N2,Hd3,N3), % Compare with running score and order them pick_best(Tl1,Hd2,N2,Choice,Rest). % recurse with new best score compare(Hd,N,Hd1,N1,Hd,N,Hd1,N1) :- % put running score first N =< N1, !. % unless new score is best compare(Hd,N,Hd1,N1,Hd1,N1,Hd,N). % Otherwise put new score first /* Find a clause with score N */ find_clause(Name,Consequent,Antecedent,N) :- clause(Name,Consequent,Antecedent,topclause), !, evaluate(Consequent,Antecedent,N). find_clause(Name,Consequent,Antecedent,N) :- clause(Name,Consequent,Antecedent,N). /* MINI-PROJECTS 1. Try this theorem prover with the equality clauses of EQUAL. 2. Experiment with clauses of your own devising. 3. Modify the theorem prover to print out the solution when it has found it. 4. Modify the theorem prover to remove the input restriction. 5. Experiment with different versions of the evaluation function by modifying 'evaluate' (see section 6.5.3 of 'Artificial Mathematicians'). */ %% NEXT FILE %% /* 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).