/******************************************************************/ /* INVERS.PRO */ /* Two versions of the two main operators of inverse resolution. */ /******************************************************************/ /* impl. by : Thomas Hoppe */ /* Mommsenstr. 50 */ /* 1000 Berlin 12 */ /* F.R.G. */ /* E-Mail: hoppet@db0tui11.pro */ /* 1989/90 */ /* */ /* reference : Muggleton, S., Buntine, W., Machine Invention */ /* of First-order Predicates by Inverting Resolu- */ /* tion, Proceedings of the International Workshop */ /* on Machine Learning, Ann Arbor, Morgan Kaufmann */ /* 1988. */ /* */ /* Rouveirol, C., Puget, J.-F., A Simple Solution */ /* For Inverting Resolution, in: K. Morik, Procee- */ /* dings of the 4th European Working Session on */ /* Machine Learning, Montpellier, Pitman Publishing*/ /* 1989. */ /* */ /* (c) copyright 1992 Thomas Hoppe */ /* */ /* You can use this program provided that it is */ /* not for commercial purposes or for publication */ /* and that the program -including all comments- */ /* is not modified (except for changes due to */ /* different prolog dialects). */ /* */ /* call : see invers_1.pro */ /* */ /******************************************************************/ /* This file contains two versions for the main operators of */ /* inverse resolution, absorption and intra-construction, as */ /* they are described by Stephen Muggleton and Wray Buntine. */ /* */ /* The versions numbered 1 are working on definite Horn-clauses */ /* without function symbols. The versions numbered 2 are working */ /* on definite Horn-clauses with function symbols. The basic */ /* difference is made up by the predicates 'flatten' and */ /* 'unflatten', and is described in Rouveirol & Puget. */ /* */ /* The main predicates 'absorption1', 'absorption2', 'intra- */ /* construction1' and 'intra-construction2' use some predicates */ /* importet from the library entry 'logic', which should be */ /* consulted befor runing the examples. */ /* */ /* Instead of using a generalisation algorithm based on the */ /* 'dropping condition rule' as described by Rouveirol & Puget */ /* I have developed a 'fast' generalisation routine, which in the*/ /* end gives the same results as 'dropping condition'. Its nice */ /* advantage is that it delivers the first generalisation in */ /* linear time, although this is an exponential problem. Of */ /* course in general, exponentiallity cannot be avoided. */ /* But through delaying it, we can save some time in easy cases. */ /******************************************************************/ /******************************************************************/ /* Some M-, C- and YAP-Prolog dependent declarations. */ /******************************************************************/ :- dynamic flat/1. :- dynamic internal/1. /******************************************************************/ /* */ /* call : absorption1(+Clause,+Resolvent,-InducedClause) */ /* */ /* arguments : Clause = definite clause */ /* Resolvent = definite clause */ /* InducedClause = induced definite clause */ /* */ /******************************************************************/ /* works on definite clauses without function-symbols */ /******************************************************************/ absorption1(Clause,Resolvent,InducedClause) :- split(Clause,ClauseHead,ClauseBody), split(Resolvent,ResolventHead,ResolventBody), step_1(ClauseBody,ResolventBody,RestClauseBody,Subst_2), subst([ClauseHead],Subst_2,[NewClauseHead]), step_2(NewClauseHead,RestClauseBody,IntermediaryBody), join(ResolventHead,IntermediaryBody,IntermediaryClause), copy(IntermediaryClause,InducedClause). split((Head :- true),Head,[]) :- !. split((Head :- Body),Head,BodyList) :- split(Body,_,BodyList), !. split((Prem,Prems),_,[Prem|RestPrems]) :- split(Prems,_,RestPrems), !. split(Prem,_,[Prem]). join(Head,PremList,(Head :- Prems)):- join(PremList,Prems). join([Prem],Prem) :- !. join([Prem|Prems],(Prem,RestPrems)) :- join(Prems,RestPrems). step_1(ClauseBody,ResolventBody,ResolventRest,Subst) :- choose_common_parts(ResolventBody,ClauseBody,Beta1,Beta2), not(not(subset(Beta1,ClauseBody))), substitution(ClauseBody,Beta1,Subst), subtract_v(Beta1,ResolventBody,ResolventRest). /********************************************************************/ /* Determination of the most special subsets of two non-ground */ /* predicate sets, on backtracking it delivers the next more general*/ /* subsets. The nice property, of this routine is, that the first */ /* common_subpart is found in linear time, although the determina- */ /* tion of all common_subparts needs exponential time. */ /********************************************************************/ choose_common_parts(List1,List2,Sublist1,Sublist2) :- findall(MGT,(member(Pred,List1), functor(Pred,N,A), functor(MGT,N,A)),MGTS1), findall(MGT,(member(Pred,List2), functor(Pred,N,A), functor(MGT,N,A)),MGTS2), !, dropping_condition_intersection(MGTS1,MGTS2,MGTS), copy(MGTS,Sublist1), copy(MGTS,Sublist2), subset(Sublist1,List1), subset(Sublist2,List2). dropping_condition_intersection([],_,[]). dropping_condition_intersection([X|R],Y,[X|Z]) :- member(X1,Y), not(not(X = X1)), !, dropping_condition_delete(X,Y,Y1), dropping_condition_intersection(R,Y1,Z). dropping_condition_intersection([X|R],Y,Z) :- dropping_condition_intersection(R,Y,Z). dropping_condition_delete(X,[Y|Ys],Ys) :- not(not(X = Y)), !. dropping_condition_delete(X,[Y|Ys],[Y|Zs]) :- dropping_condition_delete(X,Ys,Zs) . step_2(ClauseHead,RestClauseBody,IntermediaryBody) :- % Union_v helps us to avoid some redundant premisses union_v([ClauseHead],RestClauseBody,IntermediaryBody). /******************************************************************/ /* */ /* call : absorption2(+Clause,+Resolvent,-InducedClause) */ /* */ /* arguments : Clause = definite clause */ /* Resolvent = definite clause */ /* InducedClause = induced definite clause */ /* */ /******************************************************************/ /* works on definite clauses with function-symbols */ /******************************************************************/ absorption2(Clause,Resolvent,InducedClause) :- flatten(Clause,ClauseHead,ClauseBody), flatten(Resolvent,ResolventHead,ResolventBody), step_1(ClauseBody,ResolventBody,RestClauseBody,Subst_2), subst([ClauseHead],Subst_2,[NewClauseHead]), step_2(NewClauseHead,RestClauseBody,IntermediaryBody), unflatten([ResolventHead],IntermediaryBody,IntermediaryClause), copy(IntermediaryClause,InducedClause). /********************************************************************/ /* Representation change procedures for inverse resolution. */ /* The basic idea behind these procedures is to re-represent n-ary */ /* function symbols by n+1-ary predicate symbols, where the */ /* additional argument delivers the value of the function. A */ /* discussion of this can be found in Rouveirol & Puget's paper. */ /********************************************************************/ flatten((Conclusion :- Conjunction),NewConclusion,NewPremisses) :- flatten(Conclusion,[NewConclusion],FunctionPrems1,Dictionary), flatten(Conjunction,Prems,FunctionPrems2,Dictionary), union_v(FunctionPrems1,FunctionPrems2,FunctionPrems), union_v(FunctionPrems,Prems,NewPremisses), !. flatten((Prem,Prems),NewPremisses,FunctionPrems,Dictionary) :- flatten(Prem,NewPrem,FunctionPrems1,Dictionary), flatten(Prems,NewPrems,FunctionPrems2,Dictionary), union_v(NewPrem,NewPrems,NewPremisses), union_v(FunctionPrems1,FunctionPrems2,FunctionPrems), !. flatten([],[],[],_). flatten([Const|Terms],[Var|NewVars],ResultPrems,Dictionary) :- atomic(Const), lookup(Const,Dictionary,Var), conc(Const,'_p',NewName), flat_assertion(NewName,Const), Pred =..[NewName,Var], flatten(Terms,NewVars,NewPrems,Dictionary), !, union_v([Pred],NewPrems,ResultPrems). flatten([Term|Terms],[Term|NewVars],NewPrems,Dictionary) :- var(Term), !, flatten(Terms,NewVars,NewPrems,Dictionary). flatten([Term|Terms],[NewVar|NewVars],NewPrems,Dictionary) :- Term =.. [N|Args], conc(N,'_p',NN), flatten(Args,NewTerms,Prems,Dictionary), append(NewTerms,[NewVar],NewArgs), NewTerm =.. [NN|NewArgs], flat_assertion(NN,NewTerms,N,NewTerms), flatten(Terms,NewVars,NP,Dictionary), !, union_v([NewTerm],NP,ERG), union_v(Prems,ERG,NewPrems). flatten(true,[],[],_) :- !. flatten(false,[],[],_) :- !. flatten(not(Pred),[not(NewPred)],NewPrems,Dictionary) :- !, flatten(Pred,[NewPred],NewPrems,Dictionary). flatten(Pred,[Pred],[],Dictionary) :- atomic(Pred), !. flatten(Pred,[NewPred],NewPrems,Dictionary) :- !, Pred =.. [N|Args], flatten(Args,NewArgs,NewPrems,Dictionary), NewPred =.. [N|NewArgs]. flat_assertion(Name,Term) :- NewRelation =.. [Name,Term], copy(NewRelation,NR), skolemize([NR],0,_), clause(flat(NR),true), clause(flat(NewRelation),true), !. flat_assertion(Name,Term) :- NewRelation =.. [Name,Term], asserta(flat(NewRelation)), !. flat_assertion(Name1,Args,Name2,Terms):- OldTerm =.. [Name2|Terms], append(Args,[OldTerm],NewArgs), NewRelation =.. [Name1|NewArgs], copy(NewRelation,NR), skolemize([NR],0,_), clause(flat(NR),true), clause(flat(NewRelation),true), !. flat_assertion(Name1,Args,Name2,Terms):- OldTerm =.. [Name2|Terms], append(Args,[OldTerm],NewArgs), NewRelation =.. [Name1|NewArgs], asserta(flat(NewRelation)). unflatten([Head],BodyList,(Head :- Body)) :- unflatten(BodyList,Body), !. unflatten([],true). unflatten([Prem],Prem) :- functor(Prem,N,A), functor(P,N,A), not(clause(flat(P),true)), !, not(clause(flat(Prem),true)), !. unflatten([Prem|Prems],(Prem,RestPrems)) :- functor(Prem,N,A), functor(P,N,A), not(clause(flat(P),true)), !, not(clause(flat(Prem),true)), unflatten(Prems,RestPrems), !. unflatten([Prem|Prems],RestPrems) :- clause(flat(Prem),true), unflatten(Prems,RestPrems). /******************************************************************/ /* */ /* call : intra_construction1(+Resolvent1,+Resolvent2, */ /* -InducedRules) */ /* */ /* arguments : Resolvent1 = definite clause */ /* Resolvent2 = definite clause */ /* InducedRules = list of three induced definite */ /* clauses */ /* */ /******************************************************************/ /* works on definite clauses without function-symbols */ /******************************************************************/ intra_construction1(Resolvent1,Resolvent2,InducedRules) :- split(Resolvent1,Resolvent1Head,Resolvent1Body), split(Resolvent2,Resolvent2Head,Resolvent2Body), step_1(Resolvent1Head,Resolvent1Body,Resolvent2Head,Resolvent2Body, ClauseHead,Alpha,Resolvent1BodyRest,Resolvent2BodyRest, Subst1,Subst2), step_2(ClauseHead,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2,Vars), step_3_1(ClauseHead,Vars,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2, InducedRules). step_1(Resolvent1Head,Resolvent1Body,Resolvent2Head,Resolvent2Body, [ClauseHead],Alpha,Resolvent1BodyRest,Resolvent2BodyRest, Subst1,Subst2) :- choose_common_parts(Resolvent1Body,Resolvent2Body,AlphaTheta1,AlphaTheta2), % if AlphaTheta is empty we gain nothing, thus length(AlphaTheta1,X), length(AlphaTheta2,X), X > 0, subtract_v(AlphaTheta1,Resolvent1Body,Resolvent1BodyRest), subtract_v(AlphaTheta2,Resolvent2Body,Resolvent2BodyRest), % lgg doesn't take the order of literals into account, initially it was % only designed for terms, that doesn't matter because choose_common_subpart % ensures a common predicate order through copying the MGT and instantiating % afterwards. lgg([Resolvent1Head,AlphaTheta1], [Resolvent2Head,AlphaTheta2],[ClauseHead,Alpha]), % At least we determine the substitutions theta 1 and theta 2 substitution([ClauseHead,Alpha],[Resolvent1Head,AlphaTheta1],Subst1), substitution([ClauseHead,Alpha],[Resolvent2Head,AlphaTheta2],Subst2). step_2(ClauseHead,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2,Vars) :- varlist(Resolvent1BodyRest,RBR1Vars), varlist(Resolvent2BodyRest,RBR2Vars), varlist(ClauseHead,CHVars), varlist(Alpha,AVars), inv_subst(RBR1,Subst1,RBR1Vars), inv_subst(RBR2,Subst2,RBR2Vars), % The head and the generalized body part must have (at least) % a variable in common (CHVars = []; intersection_v(CHVars,AVars,XI), not(XI == [])), % This is different as in the paper of Rouveirol/Puget. If we would % use their method, we couldn't even obtain their results, but % with this it works. This error was confirmed by Celine Rouveirol union_v(CHVars,AVars,Xs), union_v(RBR1,RBR2,RBRU), intersection_v(RBRU,Xs,Vars), !. step_3_1([ClauseHead],Vars,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2, [R1,R2,R3]) :- gensym(Name,'P'), X =.. [Name|Vars], subst([X],Subst1,[X1]), subst([X],Subst2,[X2]), join(X1,Resolvent1BodyRest,QR1), join(X2,Resolvent2BodyRest,QR2), copy(QR1,NQR1), copy(QR2,NQR2), numbervars(NQR1,0,_), numbervars(NQR2,0,_), nl, write(' Predicate invention'), nl, nl, tab(3), write(NQR1), nl, tab(3), write(NQR2), nl, nl, write(' Has this predicate a meaning (y/n)? '), read(Answer), nl, (Answer = n, !, fail; Answer = y, !), write(' How shall I name the predicate ? '), read(NewName), nl, NP =..[NewName|Vars], subst([NP],Subst1,[NP1]), subst([NP],Subst2,[NP2]), join(NP1,Resolvent1BodyRest,R1), join(NP2,Resolvent2BodyRest,R2), append([NP],Alpha,ClauseBody), join(ClauseHead,ClauseBody,R3), !. /******************************************************************/ /* */ /* call : intra_construction2(+Resolvent1,+Resolvent2, */ /* -InducedRules) */ /* */ /* arguments : Resolvent1 = definite clause */ /* Resolvent2 = definite clause */ /* InducedRules = list of three induced definite */ /* clauses */ /* */ /******************************************************************/ /* works on definite clauses with function-symbols */ /******************************************************************/ intra_construction2(Resolvent1,Resolvent2,InducedClauses) :- flatten(Resolvent1,Resolvent1Head,Resolvent1Body), flatten(Resolvent2,Resolvent2Head,Resolvent2Body), step_1(Resolvent1Head,Resolvent1Body,Resolvent2Head,Resolvent2Body, ClauseHead,Alpha,Resolvent1BodyRest,Resolvent2BodyRest, Subst1,Subst2), step_2(ClauseHead,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2,Vars), step_3_2(ClauseHead,Vars,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2, InducedClauses). step_3_2(ClauseHead,Vars,Alpha,Resolvent1BodyRest,Subst1, Resolvent2BodyRest,Subst2, [R1,R2,R3]) :- gensym(Name,'P'), X =.. [Name|Vars], subst([X],Subst1,X1), subst([X],Subst2,X2), unflatten(X1,Resolvent1BodyRest,QR1), unflatten(X2,Resolvent2BodyRest,QR2), copy(QR1,NQR1), copy(QR2,NQR2), numbervars(NQR1,0,_), numbervars(NQR2,0,_), nl, write(' Predicate invention'), nl, nl, tab(3), write(NQR1), nl, tab(3), write(NQR2), nl, nl, write(' Has this predicate a meaning (y/n)? '), read(Answer), nl, (Answer = n, !, fail; Answer = y, !), write(' How shall I name the predicate ? '), read(NewName), nl, NP =..[NewName|Vars], subst([NP],Subst1,NP1), subst([NP],Subst2,NP2), unflatten(NP1,Resolvent1BodyRest,R1), unflatten(NP2,Resolvent2BodyRest,R2), append([NP],Alpha,ClauseBody), unflatten(ClauseHead,ClauseBody,R3), !. /********************************************************************/ /* Some predicates for substituting and for inverse substituting */ /* terms according to a given Subst. */ /********************************************************************/ subst([],_,[]). subst([X|Xs],Subst,[Y|Ys]) :- member(U/V,Subst), X==U, Y=V, subst(Xs,Subst,Ys), !. subst([Prem|Prems],Subst,[NewPrem|NewPrems]) :- Prem =..[F|Args], subst(Args,Subst,NewArgs), NewPrem =.. [F|NewArgs], subst(Prems,Subst,NewPrems), !. subst([X|Xs],Subst,[X|Ys]) :- subst(Xs,Subst,Ys). inv_subst([],_,[]). inv_subst([X|Xs],Subst,[Y|Ys]) :- member(U/V,Subst), Y==V, X=U, inv_subst(Xs,Subst,Ys), !. inv_subst([Prem|Prems],Subst,[NewPrem|NewPrems]) :- NewPrem =.. [F|NewArgs], inv_subst(Args,Subst,NewArgs), Prem =..[F|Args], inv_subst(Prems,Subst,NewPrems), !. inv_subst([X|Xs],Subst,[X|Ys]) :- inv_subst(Xs,Subst,Ys). /******************************************************************/ /* Some set theoretical predicates, variables are not unified */ /******************************************************************/ union_v([],X,X). union_v([X|R],Y,Z) :- member(U,Y), U==X, !, union_v(R,Y,Z). union_v([X|R],Y,[X|Z]) :- union_v(R,Y,Z). intersection_v([],_,[]). intersection_v([X|R],Y,[X|Z]) :- member(U,Y), U==X, !, intersection_v(R,Y,Z). intersection_v([X|R],Y,Z) :- intersection_v(R,Y,Z). subset([],[]). subset([X|Subset],[X|List]) :- subset(Subset,List). subset(Subset,[_|List]) :- subset(Subset,List). subtract_v([X|Xs],Ys,Zs) :- member(Y,Ys), X == Y, delete_v(X,Ys,Y1s), subtract_v(Xs,Y1s,Zs), !. subtract_v([X|Xs],Ys,Zs) :- subtract_v(Xs,Ys,Zs). subtract_v([],Xs,Xs). delete_v(X,[Y|Ys],Ys) :- X == Y, !. delete_v(X,[Y|Ys],[Y|Zs]) :- delete_v(X,Ys,Zs) . /******************************************************************/ /* Creation of unique identifiers */ /******************************************************************/ count(VAR,X) :- dynamic(VAR/1), P1 =.. [VAR,N], retract(P1), X is N+1, P2 =.. [VAR,X], assert(P2), ! . count(VAR,1) :- dynamic(VAR/1), P =.. [VAR,1], assert(P). gensym(SYM,N) :- count(N,X), conc(N,X,SYM). /******************************************************************/ /* Making a copy of the variables occuring in a Prolog term */ /******************************************************************/ copy(A,B) :- (assert(internal(A)), retract(internal(B)), !; retract(internal(_)), fail) . /******************************************************************/ /* Construction and retrieval of an dictionary */ /******************************************************************/ lookup(Key,d(Key,X,Left,Right),Value) :- !, X = Value. lookup(Key,d(Key1,X,Left,Right),Value) :- Key @< Key1, lookup(Key,Left,Value). lookup(Key,d(Key1,X,Left,Right),Value) :- Key @> Key1, lookup(Key,Right,Value). /******************************************************************/ /* Concatenation of atoms */ /******************************************************************/ conc(STR1,STR2,STR3) :- nonvar(STR1), nonvar(STR2), name(STR1,S1), name(STR2,S2), append(S1,S2,S3), name(STR3,S3). conc(STR1,STR2,STR3) :- nonvar(STR1), nonvar(STR3), name(STR1,S1), name(STR3,S3), append(S1,S2,S3), name(STR2,S2). conc(STR1,STR2,STR3) :- nonvar(STR2), nonvar(STR3), name(STR2,S2), name(STR3,S3), append(S1,S2,S3), name(STR1,S1). /******************************************************************/ /* Determination of the set of vars occuring in a Prolog expression*/ /******************************************************************/ varlist(X,L) :- varlist(X,[],L), !. varlist(T,L,LO) :- nonvar(T), T =..[F|A], !, varlist1(A,L,LO). varlist(X,L,L) :- var(X), element_v(X,L), !. varlist(X,L,[X|L]) :- var(X), !. varlist1([T|A],L,LO) :- varlist1(A,L,L1), !, varlist(T,L1,LO). varlist1([],L,L).