1% MODULE lgg EXPORTS
    2:- module( lgg,
    3	   [ subsumes_list/2,
    4             gen_msg/3,      % Buntine's most specific generalization
    5	     gen_msg/4,      %     "  with given bound for saturation
    6	     rlgg/3,         % rllg                 
    7	     rlgg/4,         % rllg with given head literal of preference
    8	     covered_clause/2,      
    9	     covered_clauses/4,
   10             reduce_complete/1,
   11	     reduce_complete/2,
   12	     reduce_approx/2,
   13             buildlgg/4,
   14             lgg/3, lgg/4, lgg/5,                    
   15             headed_lgg/3, headed_lgg/4, headed_lgg/5,   
   16             nr_lgg/3, nr_lgg/4, nr_lgg/5,               
   17             hnr_lgg/3, hnr_lgg/4, hnr_lgg/5,            
   18             lgg_terms/3, lgg_terms/5,                   
   19             lgg_terms/7, 
   20             set_lgg/2 ,                    
   21             gti/3,
   22             gti/5,
   23             lgti/3,
   24             lgti/5,
   25             lgti/6      
   26           ]).   27
   28% IMPORTS
   29:- use_module(home(kb),
   30              [get_clause/5,delete_clause/1,store_clause/4,get_example/3]).   31:- use_module(home(bu_basics),
   32              [assert_body_randomly/1,clear_mngr/0,subs_build_clause/1,
   33               reset_counts/0,assert_clause/1,assert_body/1,body/3,head/3,
   34               cover_assert_assumptions/1,assumption/3,msg_build_long_clause/1,
   35               msg_build_heads/1,msg_build_body/1]).   36:- use_module(home(var_utils),
   37              [skolemize/3,skolemize/4,deskolemize/3,clean_subst/3]).   38:- use_module(home(div_utils),
   39              [extract_body/2,convert_to_horn_clause/3,effaceall/3,subset_chk/2,
   40               maximum/2,identical_member/2,identical_make_unique/2]).   41:- use_module(home(interpreter),
   42              [prove1/2,prove5/2]).   43:- use_module(home(g1_ops),
   44              [saturate/2,saturate/3,inv_derivate1/2]).   45:- use_module(home(filter),
   46              [truncate_unconnected/2]).   47:- use_module(home(evaluation),
   48              [complexity/2]).   49:- use_module_if_exists(library(sets),
   50              [list_to_set/2,subtract/3]).   51:- use_module_if_exists(library(lists),
   52              [is_list/1,subseq0/2,nth1/4]).   53:- use_module_if_exists(library(basics),
   54              [member/2]).   55:- use_module_if_exists(library(random),
   56              [maybe/0]).   57:- use_module_if_exists(library(not),
   58              [(once)/1]).   59:- use_module_if_exists(library(occurs),
   60              [contains_var/2,free_of_var/2]).   61:- use_module_if_exists(library(subsumes),
   62              [subsumes_chk/2,variant/2]).   63
   64
   65% METAPREDICATES
   66% none
   67
   68
   69:- dynamic counter/1, shortsubst/2, iterate/1.   70
   71
   72
   73%***********************************************************************
   74%*	
   75%* module: lgg.pl        					
   76%*									
   77%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend              date:12/92	
   78%*									
   79%* changed:								
   80%*									
   81%* description: - clause reduction 
   82%*                reduce clause with no repect to background           
   83%*                knowledge (Plotkin,1970)                             
   84%*                reduce w.r.t. background knowledge (Buntine,1988)    
   85%*                Since reduction is in both cases NP-complete,           
   86%*                we provide 2 versions for each case:                    
   87%*                a correct, but higly inefficient solution               
   88%*                & an approximation.
   89%*              - clause_subsumption 
   90%*		- Buntine's most specific generalization under 
   91%*                generalized subsumption 
   92%*              - Plotkin's RLGG, with Muggleton's algorithm  
   93%*	        - Plotkins least general generalisation (lgg)
   94%*                under theta subsumption    
   95%*              - least general intersection lgti           
   96%*
   97%* see also: Buntine,88; Muggleton,90; Plotkin, 70;          
   98%*           module lgg.pl for msg 
   99%*                                                           
  100%***********************************************************************
  101
  102
  103
  104%***********************************************************************
  105%*                                                                      
  106%* predicates: reduce_complete/2
  107%*                                                                      
  108%* syntax: reduce_complete(+Clause,-ReducedClause)                      
  109%*                                                                      
  110%* args: Clause:        input clause in list form                       
  111%*       ReducedClause: reduced, minimal clause equivalent to Clause    
  112%*                                                                      
  113%* description: do not consider bg, i.e. reduction wrt theta subsumption
  114%*                                                                      
  115%* example:                                                             
  116%*                                                                      
  117%* peculiarities:                                                       
  118%*                                                                      
  119%* see also:                                                            
  120%*									
  121%***********************************************************************
  122
  123
  124reduce_complete(ID):-
  125        get_clause(ID, _,_,C,_),
  126        reduce_complete(C,D),
  127        delete_clause(ID),
  128        store_clause(_,D,reduce,ID),!.
  129
  130
  131reduce_complete(Clause,Reduced):-
  132	clear_mngr,
  133	skolemize(Clause,S,SClause),
  134	assert_clause(SClause),
  135	reduce_complete1(Clause,S,SReduced0),
  136        list_to_set(SReduced0,SReduced),
  137	deskolemize(SReduced,S,Reduced),
  138        !.        % No backtracking allowed (solution is unique)
  139
  140
  141%***********************************************************************
  142%*									
  143%* predicate:	reduce_complete1/3							
  144%*									
  145%* syntax: reduce_complete1(+CL,+Subst,-ReducedCL)
  146%*									
  147%* args: CL,ReducedCL: clauses in list notation
  148%*       Subst: skolem substitution
  149%*									
  150%* description:	reduces CL by matching it on the skolemized head and
  151%*		body literals of the reduced clause in the kb
  152%*									
  153%* example:								
  154%*									
  155%* peculiarities:	none				
  156%*									
  157%* see also:								
  158%*									
  159%***********************************************************************
  160
  161reduce_complete1(C,S,RC):-
  162	copy_term(C,ToShow),
  163	prove1(ToShow,SProof),
  164	(   reduce_complete_test(SProof) ->
  165            clear_mngr,
  166            list_to_set(SProof, SProof1), 
  167            assert_clause( SProof1),                 
  168            copy_term( S, S1),
  169            deskolemize( SProof1,S1,Proof),
  170            reduce_complete1(Proof,S,RC)
  171	;   reset_counts,
  172            fail   % backtrack, find another proof
  173	).
  174reduce_complete1(_,_S,RC):-
  175	!,    % there is no shorter proof, the minimal clause is found.
  176	subs_build_clause(RC).
  177
  178
  179reduce_complete_test(P):-
  180   findall(H:p,head(H,_,_),HL),
  181   setof(B:_,body(B,_,_),BL),
  182   append(HL,BL,L),
  183   list_to_set(L,L0),
  184   list_to_set(P,P0),
  185   subtract(L0,P0,D),!,
  186   D \== [].
  187
  188
  189
  190%***********************************************************************
  191%*									
  192%* predicate:	reduce_approx/2							
  193%*									
  194%* syntax: reduce_approx(+Clause,-ReducedClause)                      
  195%*                                                                      
  196%* args: Clause:        input clause in list form                       
  197%*       ReducedClause: reduced, minimal clause equivalent to Clause    
  198%*                                                                      
  199%* description: as reduce_complete except that the number of single 
  200%*              reduction steps is bound 
  201%*
  202%* example:								
  203%*									
  204%* peculiarities:	none				
  205%*									
  206%* see also:								
  207%*									
  208%***********************************************************************
  209
  210reduce_approx(Clause,Reduced):-
  211	clear_mngr,
  212	copy_term(Clause,Copy),
  213	skolemize(Copy,S,SClause),
  214	assert_clause(SClause),
  215	reduce_approx1(S,1,50),
  216        reduce_get_current_clause(SReduced0),
  217        list_to_set(SReduced0,SReduced),
  218	deskolemize(SReduced,S,Reduced).
  219
  220reduce_approx1(S,Counter,Bound):-
  221	Counter =< Bound,
  222        copy_term( S, S1),
  223        reduce_get_current_clause(C),
  224        deskolemize(C,S1,ToShow),
  225        
  226        prove1(ToShow,SProof),
  227        
  228        clear_mngr,
  229        assert_body_randomly( SProof),
  230        J is Counter + 1,                 
  231        reduce_approx1(S,J,Bound).
  232
  233	
  234reduce_approx1(_,_,_).
  235
  236
  237
  238
  239%***********************************************************************
  240%*									
  241%* predicate:	reduce_get_current_clause/1
  242%*									
  243%* syntax: reduce_get_current_clause(-CL)
  244%*									
  245%* args: CL: clause in list notation
  246%*									
  247%* description:	returns current skolemized clause that is stored via 
  248%*              head/3 and body/3 in the kb						
  249%*									
  250%* example:								
  251%*									
  252%* peculiarities:	none				
  253%*									
  254%* see also:								
  255%*									
  256%***********************************************************************
  257
  258reduce_get_current_clause(CL):-
  259      findall(H:p,head( H,_,_),Heads),
  260      findall(L:n, body(L,_,_), Body),
  261      append(Heads,Body,CL).
  262
  263
  264%*********************************************************************
  265%*                                                              
  266%* predicate: covered_clause/2                                 
  267%*                                                              
  268%* syntax: covered_clause(+RULES, +ID)                          
  269%*                                                              
  270%* args:  RULES: list of kb references (integers)               
  271%*        ID:    id of clause to be tested                      
  272%*                                                              
  273%* description:  Test, if a clause is a specialization of RULES.
  274%*                                                              
  275%* example: let RULES refer to clauses                          
  276%*          member(A,[A|B]).                                    
  277%*          member(A,[B|C]):- member(A,C).                      
  278%*       then                                                   
  279%*          member(3,[1,2,3]):- member(3,[2,3])               
  280%*       is covered by RULES                                   
  281%*                                                            
  282%* see also:                                                  
  283%*									
  284%********************************************************************
  285
  286covered_clause(RULES,ID):-
  287       nonvar(RULES),
  288       member(ID,RULES).
  289
  290
  291covered_clause(RULES,ID):-
  292       nonvar(RULES),
  293       retractall( assumption(_,_,_) ),
  294       get_clause(ID,_,_,Clause,_),
  295       skolemize(Clause,_,[H:p|Body]),
  296       cover_assert_assumptions(Body),
  297       prove5( H, RULES),     
  298       !.
  299
  300
  301%****************************************************************
  302%*                                                              
  303%* predicate: covered_clauses/4                                
  304%*                                                             
  305%* syntax: covered_clauses(+RULES,+ToTest,-Covered,-Uncovered) 
  306%*                                                             
  307%* args: RULES: list of kb references (integers)               
  308%*       ToTest: either label of kb entries (lgg, sat, ex ..)  
  309%*               or a list of kb references                    
  310%* description: test if RULES explain all example clauses      
  311%*              denoted by ToTest.                             
  312%*              Or: RULES |= clauses(ToTest)                   
  313%*                                                             
  314%* example:                                                    
  315%*                                                             
  316%* peculiarities:                                              
  317%*                                                             
  318%* see also:                                                   
  319%*									
  320%****************************************************************
  321
  322covered_clauses(RULES,LABEL,Covered,Uncovered):-
  323        nonvar(RULES),
  324        atom(LABEL),
  325        findall( ID, get_clause( ID,_,_,_,LABEL), ToTest),
  326        covering( RULES, ToTest, [],Covered, [], Uncovered).
  327
  328covered_clauses(RULES,ToTest,Covered,Uncovered):-
  329        nonvar(RULES),
  330        is_list(ToTest),
  331        covering( RULES, ToTest, [],Covered, [], Uncovered).
  332
  333
  334covering( RULES, [ID|ToTest], Covered1, Covered2, Uncovered1, Uncovered2):-
  335        retractall( assumption(_,_,_) ),
  336        get_clause( ID, _,_,Clause,_),     
  337        \+ ( member(ID, Covered1) ; member(ID, Uncovered1) ),
  338        skolemize( Clause, _, [H:p | Body ]),
  339        cover_assert_assumptions(Body), 
  340        !,
  341        ( member(ID,RULES)  -> Covered3 = [ ID | Covered1 ],
  342                               Uncovered3 = Uncovered1
  343
  344        ;  
  345          prove5( H, RULES) -> Covered3 = [ ID | Covered1 ],
  346                               Uncovered3 = Uncovered1
  347        
  348        | otherwise         -> Covered3 = Covered1,
  349                               Uncovered3 = [ ID | Uncovered1 ]
  350        ),
  351        covering(RULES, ToTest, Covered3,Covered2,Uncovered3,Uncovered2).
  352
  353covering( _,[],Covered,Covered,Uncovered,Uncovered):-!.
  354
  355
  356%***************************************************************
  357%*                                                              
  358%* predicates: gen_msg/3/4                                      
  359%*                                                              
  360%* syntax: gen_msg(+ID1,+ID2,-ID)                               
  361%*         gen_msg(+ID1,+ID2,-ID,+Bound)                        
  362%*                                                              
  363%* args: ID1,ID2,ID:integers, references to clauses in kb       
  364%*           Bound :integer, depth bound for saturation         
  365%*                                                              
  366%* description: Approximation of Buntine's most specific        
  367%*              generalization. We saturate the 2 input clauses 
  368%*              & build the lgg over them.                      
  369%*              Our procedure differs from Buntine's in that    
  370%*              saturation does not construct all generalizing  
  371%*              clauses under generalized subsumption: if some  
  372%*              head literal entailed by the body contains      
  373%*              unbound variables, saturation adds it to the    
  374%*              body as it is, whereas Buntine instead adds all 
  375%*              of its ground instances. 
  376%*                       
  377%* example:                                                     
  378%*                                                              
  379%* peculiarities: the resulting clause is not yet reduced       
  380%*                                                              
  381%* see also:                                                    
  382%*									
  383%***************************************************************
  384
  385gen_msg(ID1,ID2,ID):-
  386       get_clause(ID1,H1,_,_,_),
  387       get_clause(ID2,H2,_,_,_),
  388       functor(H1,F,N),
  389       functor(H2,F,N),
  390       saturate(ID1,A),
  391       saturate(ID2,B),
  392       % lgg(A,B,ID),
  393       lgti(A,B,ID),                % changed !
  394       delete_clause(A),
  395       delete_clause(B).
  396
  397gen_msg(ID1,ID2,ID,Bound):-
  398       get_clause(ID1,H1,_,_C1,_),
  399       get_clause(ID2,H2,_,C2,_),
  400       functor(H1,F,N),
  401       functor(H2,F,N),
  402       delete_clause(ID2),
  403       
  404       saturate(ID1,A,Bound),
  405       delete_clause(ID1),
  406       get_clause(A,_,_,C1sat,_),
  407       delete_clause(A),
  408       store_clause(_,C2,genmsg,ID2),
  409       
  410       saturate(ID2,B,Bound),
  411       store_clause(_,C1sat,sat,A),
  412       delete_clause(ID2),
  413
  414       nr_lgg(A,B,ID),
  415       % lgti(A,B,ID).               % changed !
  416       delete_clause(A),
  417       delete_clause(B).
  418
  419
  420%***************************************************************
  421%*                                                              
  422%* predicate: rllg/3/4                                          
  423%*                                                              
  424%* syntax: rllg(+ID1,+ID2,-ID)                                  
  425%*         rllg(+ID1,+ID2,+PrefHead,-ID)                        
  426%*                                                              
  427%* args: ID1,ID2,ID: integers, references to clauses in kb      
  428%*       PrefHead:   prolog literal                             
  429%*                                                              
  430%* description: Plotkin's relative leat general generalization. 
  431%*              Implementation thru Muggleton's alg. :          
  432%*              Construct 2 inverse linear derivations,         
  433%*              then build lgg over them.                       
  434%*                                                              
  435%*              If PrefHead is given & it is possible to find   
  436%*              a rllg who's head matches PrefHead, rllg will   
  437%*              construct this clause.
  438%*                          
  439%* example:                                                     
  440%*                                                              
  441%* peculiarities: no reduction yet                              
  442%*                                                              
  443%* see also:                                                    
  444%*									
  445%***************************************************************
  446
  447rlgg(ID1,ID2,ID):-
  448      rlgg(ID1,ID2,_,ID).
  449
  450rlgg(ID1,ID2,PrefHead,ID):-
  451      ( get_clause(ID1,_,_,Clause1,_) 
  452      ; get_example(ID1,Ex1,'+'), Clause1 = [Ex1:p] ),
  453      clear_mngr,
  454      skolemize(Clause1,S1,C1),
  455      assert_clause(C1),
  456      inv_derivate1(ID1,1),
  457      msg_build_long_clause(D1),
  458      deskolemize(D1,S1,A1),
  459
  460      ( get_clause(ID2,_,_,Clause2,_)  
  461      ; get_example(ID2,Ex2,'+'), Clause2 = [Ex2:p]  ),
  462      clear_mngr,
  463      skolemize(Clause2,S2,C2),
  464      assert_clause(C2),
  465      inv_derivate1(ID2,1),
  466      msg_build_long_clause(D2),
  467      deskolemize(D2,S2,A2),
  468
  469
  470      lgg_gen_clause(A1,A2,D,_,[],[],_,_),
  471      !,                             % thru backtracking different
  472      convert_to_horn_clause(PrefHead,D,E),% heads may be obtained
  473      truncate_unconnected(E,F),
  474      store_clause(_,F,rlgg,ID).
  475
  476
  477%***********************************************************************
  478%*									
  479%* predicate: subsumes_list/2
  480%*
  481%* syntax: subsumes_list(+General,+Specific)
  482%*       			
  483%* args:  clauses in list notation					
  484%*									
  485%* description:	checks for theta subsumption by list matching.		
  486%*		No proofs, no substitutions are returned.		
  487%* 		General will not be instantiated.	
  488%*
  489%* example:
  490%*
  491%* peculiarities:
  492%*
  493%* see also:		
  494%*									
  495%***********************************************************************
  496
  497subsumes_list( Gen, Spec):-
  498      copy_term(Gen, Gen1),
  499      copy_term(Spec, Spec1),
  500      numbervars(Spec1,1,_),
  501      subsumes_list1(Gen1,Spec1).
  502
  503subsumes_list1([],_).
  504subsumes_list1([L|Rest], Spec):-
  505      member(L,Spec),
  506      subsumes_list1(Rest,Spec).
  507
  508
  509%********************************************************************************
  510%*                                                                       
  511%* predicates: lgg_terms/3, lgg_terms/5, lgg_terms/7
  512%*                                                                       
  513%* syntax: lgg_terms( + Term1, + Term2, - GenTerm )                  
  514%*         lgg_terms( + Term1, + Term2, - GenTerm,                   
  515%*                    - Subst_Term1, - Subst_Term2 )
  516%*         lgg_terms( + Term1, + Term2, - GenTerm,                   
  517%*                    - Subst1, - Subst2,                         
  518%*                    + Init_Subst1, + Init_Subst2 )                                   
  519%*
  520%* args: Term1,Term2,GenTerm: prolog terms
  521%*       Subst_termi: [Var/Fi,..] substitution such that Termi = GenTerm Subst_termi
  522%*
  523%* description: Plotkins least general generalisation wrt theta-subsumption
  524%*              on terms
  525%*
  526%* example:
  527%*
  528%* peculiarities:
  529%*
  530%************************************************************************
  531
  532lgg_terms(Term1, Term2, GTerm) :-
  533        lgg_terms(Term1, Term2, GTerm, _, _, [], []).
  534
  535lgg_terms(Term1, Term2, GTerm, Subst1, Subst2) :-
  536        lgg_terms(Term1, Term2, GTerm, Subst1, Subst2, [], []).
  537
  538lgg_terms(Term1, Term2, GTerm, S1, S2, Accu1, Accu2) :-
  539    % if same functor, same arity
  540        nonvar(Term1), nonvar(Term2),
  541        functor(Term1,F,N), functor(Term2,F,N)
  542    ->  
  543    % then: build new term by generalizing arguments
  544        functor(GTerm,F,N),
  545        generalize_arguments(Term1,Term2,N,GTerm,Accu1,Accu2,S1,S2)
  546    ;
  547    % else if same instantiation
  548        Term1 == Term2
  549    ->
  550    % then: no problem
  551        S1 = Accu1, S2 = Accu2, GTerm = Term1
  552    ;
  553    % else if substitution has already been applied
  554        substituted(Accu1, Accu2, Term1, Term2, Variable)
  555    ->
  556    % then: again, no problem
  557        S1 = Accu1, S2 = Accu2, GTerm = Variable
  558    ;
  559    % else if neither is true
  560    % then: substitute with a new variable
  561        S1 = [NewVar/Term1 | Accu1],
  562        S2 = [NewVar/Term2 | Accu2],
  563        GTerm = NewVar.
  564
  565% generalize argument-terms (loop from position n to position 0)
  566generalize_arguments(_,_,0,_,Ac1,Ac2,Ac1,Ac2) :- !.
  567generalize_arguments(Term1,Term2,N,GTerm,Ac1,Ac2,S1,S2) :-
  568        arg(N, Term1, ArgN1),
  569        arg(N, Term2, ArgN2),
  570        arg(N, GTerm, ArgNG),
  571        lgg_terms(ArgN1,ArgN2,ArgNG,Ac1new,Ac2new,Ac1,Ac2),
  572        K is N-1,
  573        generalize_arguments(Term1,Term2,K,GTerm,Ac1new,Ac2new,S1,S2).
  574
  575% test whether two terms at the same position have already a common generalised term
  576substituted([X/T1|_], [X/T2|_], Term1, Term2, X) :-
  577        T1 == Term1, T2 == Term2, !.
  578substituted([_|Accu1], [_|Accu2], Term1, Term2, X) :-
  579        substituted(Accu1, Accu2, Term1, Term2, X).
  580
  581
  582%************************************************************************
  583%*
  584%* predicate: set_lgg/2
  585%*
  586%* syntax: set_lgg(+List_of_Terms,-GenTerm)   
  587%*
  588%* args:
  589%*
  590%* description: lgg of a list of terms
  591%*
  592%* example:
  593%*
  594%* peculiarities:
  595%*
  596%* see also:
  597%*
  598%************************************************************************
  599
  600set_lgg([L],L):- !.
  601set_lgg([X,Y|R],Lgg):-
  602   lgg_terms(X,Y,Lgg0),
  603   set_lgg([Lgg0|R],Lgg).
  604
  605
  606
  607%************************************************************************
  608%*
  609%* predicate: headed_lgg/3, headed_lgg/4
  610%*
  611%* syntax: headed_lgg(+ID1,+ID2,-IDG)
  612%*         headed_lgg(+ID1,_ID2,-IDG,?Label)
  613%*
  614%* args: ID1,ID2,IDG: clauseIDs, Label: atom
  615%*
  616%* description: returns lgg of clauses ID1 ID2 in IDG, if both clauses
  617%*              have a compatible head literal (i.e. same pred, same
  618%*              arity). Fails else.
  619%*              Default label is hlgg
  620%*
  621%* example:
  622%*
  623%* peculiarities:
  624%*
  625%* see also:
  626%*
  627%************************************************************************
  628
  629headed_lgg(Id1, Id2, IdG) :- headed_lgg(Id1, Id2, IdG, 'hlgg').
  630
  631headed_lgg(Id1, Id2, IdG, Label) :-
  632        ((var(Label) -> Label = hlgg);true),
  633        hlgg1(Id1, Id2, HG, BGlist),
  634%       reduce_irene([HG:p|BGlist],[HGr:p|BGlistred]), 
  635        reduce_complete([HG:p|BGlist],[HGr:p|BGlistred]),  % finally reduce lgg-body
  636%       reduce_approx([HG:p|BGlist],[HGr:p|BGlistred]),% alternatively (more efficient)
  637        store_clause(_, [HGr:p|BGlistred], Label, IdG).
  638
  639hlgg1(Id1, Id2, HG, BGlist) :-
  640        get_clause(Id1, H1, _, [_|B1list], _),      % if name + arity match for both heads
  641        get_clause(Id2, H2, _, [_|B2list], _),      % generalize heads first,
  642        functor(H1,F,N), functor(H2,F,N),           % then generalize bodies. 
  643        lgg_terms(H1,H2,HG,Subst1,Subst2),          
  644        lgg_body(B1list,B2list,BGlist,[],Subst1,Subst2,_,_).
  645
  646
  647
  648%************************************************************************
  649%*
  650%* predicate: hnr_lgg/3, hnr_lgg/4
  651%*
  652%* syntax: hnr_lgg(+ID1,+ID2,-IDG)
  653%*         hnr_lgg(+ID1,_ID2,-IDG,?Label)
  654%*
  655%* args: ID1,ID2,IDG: clauseIDs, Label: atom
  656%*
  657%* description: same as headed_lgg, except that the resulting generalised 
  658%*              clause is NOT reduced. Default label is hnrlgg
  659%*
  660%* example:
  661%*
  662%* peculiarities:
  663%*
  664%* see also:
  665%*
  666%************************************************************************
  667
  668hnr_lgg(Id1, Id2, IdG) :- hnr_lgg(Id1, Id2, IdG, 'hnrlgg').
  669
  670hnr_lgg(Id1, Id2, IdG, Label) :-
  671        ((var(Label) -> Label = hnrlgg);true),
  672        hlgg1(Id1, Id2, HG, BGlist),
  673        store_clause(_, [HG:p|BGlist], Label, IdG).
  674
  675
  676%************************************************************************
  677%*
  678%* predicate: lgg/3, lgg/4
  679%*
  680%* syntax: lgg(+ID1,+ID2,-IDG)
  681%*         lgg(+ID1,_ID2,-IDG,?Label)
  682%*
  683%* args: ID1,ID2,IDG: clauseIDs, Label: atom
  684%*
  685%* description: returns lgg of clauses ID1 ID2 in IDG. If both clauses
  686%*              have no compatible head literal, the head literal of IDG
  687%*              is set to 'true'.
  688%*              Default label is lgg
  689%*
  690%* example:
  691%*
  692%* peculiarities:
  693%*
  694%* see also:
  695%*
  696%************************************************************************
  697
  698lgg(Id1, Id2, IdG) :- lgg(Id1, Id2, IdG, 'lgg').
  699
  700lgg(Id1, Id2, IdG, Label) :-
  701        ((var(Label) -> Label = lgg);true),
  702        lgg1(Id1, Id2, HG, BGlist),
  703%       reduce_irene([HG:p|BGlist],[HGr:p|BGlistred]), 
  704        reduce_complete([HG:p|BGlist],[HGr:p|BGlistred]), % finally reduce lgg-body
  705%       reduce_approx([HG:p|BGlist],[HGr:p|BGlistred]),  % alternatively (more efficient)
  706        store_clause(_, [HGr:p|BGlistred], Label, IdG).
  707
  708
  709lgg1(Id1, Id2, HG, BGlist) :-
  710        get_clause(Id1, H1, _, [_|B1list], _),      % if name + arity match for both heads
  711        get_clause(Id2, H2, _, [_|B2list], _),      % then generalize heads,
  712        (functor(H1,F,N), functor(H2,F,N) ->        % else use 'true' as head;
  713        lgg_terms(H1,H2,HG,Subst1,Subst2);          % then generalize bodies.       
  714        HG = true, Subst1 = [], Subst2 = []),             
  715        lgg_body(B1list,B2list,BGlist,[],Subst1,Subst2,_,_).
  716
  717
  718
  719%************************************************************************
  720%*
  721%* predicate: nr_lgg/3, nr_lgg/4
  722%*
  723%* syntax: nr_lgg(+ID1,+ID2,-IDG)
  724%*         nr_lgg(+ID1,_ID2,-IDG,?Label)
  725%*
  726%* args: ID1,ID2,IDG: clauseIDs, Label: atom
  727%*
  728%* description: same as lgg, except that the resulting generalised 
  729%*              clause is NOT reduced. Default label is nrlgg
  730%*
  731%* example:
  732%*
  733%* peculiarities:
  734%*
  735%* see also:
  736%*
  737%************************************************************************
  738
  739nr_lgg(Id1, Id2, IdG) :- nr_lgg(Id1, Id2, IdG, 'nrlgg').
  740
  741nr_lgg(Id1, Id2, IdG, Label) :-
  742        ((var(Label) -> Label = nrlgg);true),
  743        lgg1(Id1, Id2, HG, BGlist),
  744        store_clause(_, [HG:p|BGlist], Label, IdG).
  745
  746
  747%***********************************************************************
  748%*									
  749%* predicate:	buildlgg/4							
  750%*									
  751%* syntax: build_lgg(+IDs,+IID,-GID,+Label)
  752%*									
  753%* args: IDs: list of clauseIDs,
  754%*       IID,GID: clauseIDs
  755%*       Label: atom								
  756%*									
  757%* description:	returns in GID the ID of the lgg of all clauses in IDs. IID is
  758%*              the ID of the intermediate result
  759%*									
  760%* example:								
  761%*									
  762%* peculiarities:	none				
  763%*									
  764%* see also:								
  765%*									
  766%***********************************************************************
  767
  768buildlgg([C1],C2,Clgg,L) :- lgg(C1,C2,Clgg,L), !.
  769
  770buildlgg([C1|CRest],Clgg_old,Clgg_new2,L) :-
  771        lgg(C1,Clgg_old,Clgg_new1,tmp), !,
  772        (buildlgg(CRest,Clgg_new1,Clgg_new2,L) ->
  773        delete_clause(Clgg_new1);
  774        delete_clause(Clgg_new1),fail).
  775
  776buildlgg([],O,N,L) :-
  777	get_clause(O,_,_,Cl,_),
  778	store_clause(_,Cl,L,N), !.
  779
  780
  781%************************************************************************
  782%*
  783%* predicate: lgg/5, nr_lgg/5
  784%*
  785%* syntax: (nr_)lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2)
  786%*
  787%* args: CL1,CL2,CLG: clauses in list notation
  788%*       Substi: Substitutions such that CLG Substi \subseteq CLi
  789%*
  790%* description: CLG is (non-reduced) lgg of clauses CL1 and CL2
  791%*
  792%* example:
  793%*
  794%* peculiarities:
  795%*
  796%* see also:
  797%*
  798%************************************************************************
  799
  800lgg(Clause1list, Clause2list, [HGr|BGlistred], S1,S2):-    %Theta1, Theta2) :-
  801	nr_lgg(Clause1list, Clause2list, [HG|BGlist], SS1, SS2),
  802%       reduce_irene([HG|BGlist],[HGr|BGlistred]).
  803       reduce_complete([HG|BGlist],[HGr|BGlistred]),
  804        clean_subst([HGr|BGlistred],SS1,S1),
  805        clean_subst([HGr|BGlistred],SS2,S2).
  806%       reduce_approx([HG|BGlist],[HGr|BGlistred]), %%alternatively (more efficient)
  807
  808	
  809
  810nr_lgg([H1:p|B1list], [H2:p|B2list], [HG:p|BGlist], Theta1, Theta2) :-
  811        (functor(H1,F,N), functor(H2,F,N) ->
  812        lgg_terms(H1,H2,HG,Subst1,Subst2);
  813        HG = true, Subst1 = [], Subst2 = []),             
  814        lgg_body(B1list,B2list,BGlist,[],Subst1,Subst2,Theta1,Theta2).
  815
  816
  817%************************************************************************
  818%*
  819%* predicate: headed_lgg/5, hnr_lgg/5
  820%*
  821%* syntax: headed_lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2)
  822%*         hnr_lgg(+CL1,+CL2,-CLG,-Subst1,-Subst2)
  823%*
  824%* args: CL1,CL2,CLG: clauses in list notation
  825%*       Substi: Substitutions such that CLG Substi \subseteq CLi
  826%*
  827%* description: CLG is (non-reduced) headed lgg of clauses CL1 and CL2
  828%*
  829%* example:
  830%*
  831%* peculiarities:
  832%*
  833%* see also:
  834%*
  835%************************************************************************
  836
  837headed_lgg(Clause1list, Clause2list, [HGr|BGlistred], S1,S2):- %%%Theta1, Theta2) :-
  838	hnr_lgg(Clause1list, Clause2list, [HG|BGlist], SS1, SS2),
  839%       reduce_irene([HG|BGlist],[HGr|BGlistred]).
  840        reduce_complete([HG|BGlist],[HGr|BGlistred]),
  841        clean_subst([HGr|BGlistred],SS1,S1),
  842        clean_subst([HGr|BGlistred],SS2,S2).
  843%       reduce_approx([HG|BGlist],[HGr|BGlistred]), %%alternatively (more efficient)
  844
  845hnr_lgg([H1:p|B1list], [H2:p|B2list], [HG:p|BGlist], Theta1, Theta2) :-
  846        functor(H1,F,N), functor(H2,F,N),
  847        lgg_terms(H1,H2,HG,Subst1,Subst2),
  848        lgg_body(B1list,B2list,BGlist,[],Subst1,Subst2,Theta1,Theta2).
  849
  850
  851%************************************************************************
  852%*
  853%* predicate: lgg_body/8
  854%*
  855%* syntax: lgg_body(+CL1,+CL2,+CLAccu,-CLAccu,+Subst1,+Subst2,-Subst1,-Subst2)
  856%*        
  857%* args: CL1,CL2,CLAccu: clauses bodiesin list representation 
  858%*       Subst..:Substitutions for the variables in CLAccu
  859%*
  860%* description: CLAccu is the non-reduced lgg of the clause bodies CL1 and
  861%*              CL2. The generalisation of two redundant literals L1:r, L2:r is
  862%*              marked as redundant LG:r.
  863%*
  864%* example:
  865%*
  866%* peculiarities:
  867%*
  868%* see also:
  869%*
  870%************************************************************************
  871
  872lgg_body([],_,Accu,Accu,S1,S2,S1,S2) :- !.
  873lgg_body(_,[],Accu,Accu,S1,S2,S1,S2) :- !.
  874        
  875lgg_body([Elem1|R1], List2, Glist, AcGL, S1old, S2old, Theta1, Theta2) :-
  876        generalize_elem(List2, Elem1, GLelem1, S1old, S2old, S1new, S2new),
  877        append(AcGL, GLelem1, AcGLnew),
  878        lgg_body(R1, List2, Glist, AcGLnew, S1new, S2new, Theta1, Theta2).
  879
  880
  881%***************************************************************
  882%*                                                              
  883%* predicate: lgg_gen_clause/8  
  884%*                                                              
  885%* syntax: lgg_gen_clause(+CL1,+CL2,+CLAccu,-CLAccu,+Subst1,
  886%*                           +Subst2,-Subst1,-Subst2)
  887%*        
  888%* args: CL1,CL2,CLAccu: general clauses in list representation 
  889%*       Subst..:Substitutions for the variables in CLAccu
  890%*                                                              
  891%* description: CLAccu is the lgg of CL1 and CL2 (non-reduced)
  892%*              CL1, CL2 might be non Horn
  893%*                                                              
  894%* example:                                                     
  895%*                                                              
  896%* peculiarities: 
  897%*                                                              
  898%* see also:                                                    
  899%*									
  900%***************************************************************
  901
  902lgg_gen_clause([],_,Accu,Accu,S1,S2,S1,S2) :- !.
  903lgg_gen_clause(_,[],Accu,Accu,S1,S2,S1,S2) :- !.
  904        
  905lgg_gen_clause([Elem1:Sign1|R1], List2, Glist, AcGL, S1old, S2old, Theta1, Theta2) :-
  906        generalize_elem(List2, Elem1:Sign1, GLelem1, S1old, S2old, S1new, S2new),
  907        append(AcGL, GLelem1, AcGLnew),
  908        lgg_gen_clause(R1, List2, Glist, AcGLnew, S1new, S2new, Theta1, Theta2).
  909
  910
  911%***************************************************************
  912%*                                                              
  913%* predicate: generalize_elem/7  
  914%*                                                              
  915%* syntax: generalize_elem(+CL,+Lit:Sign,-GCL,+Subst1,+Subst2,-Subst1,-Subst2)
  916%*                                                              
  917%* args: CL,GCL: clauses in list notation
  918%*       GCL: clause in list notation
  919%*       Lit:Sign: literal and sign (in {p,n,r})
  920%*       Subst..: Sustitutions for the variables in GCL 
  921%*                                                              
  922%* description: for each literal L in CL matching Lit:Sign (i.e. same functor, arity
  923%*       and compatible sign), the lgg of L and Lit is added to GCL, and the
  924%*       subtitutions are extended accordingly
  925%*                                                              
  926%* example:                                                     
  927%*                                                              
  928%* peculiarities: 
  929%*                                                              
  930%* see also:                                                    
  931%*									
  932%***************************************************************
  933
  934generalize_elem([],_,[],S1,S2,S1,S2) :- !.
  935
  936generalize_elem([Elem1:Sign1|R1],Literal:Sign2,[GTerm:Sign|RestGL],S10,S20,S12,S22) :-
  937        functor(Literal,F,N), functor(Elem1,F,N),
  938        lgg_terms(Literal,Elem1,GTerm,S11,S21,S10,S20),
  939        ( Sign1 == p, Sign2 == p   -> Sign = p
  940        ;
  941          Sign1 == r, Sign2 == r   -> Sign = r
  942        ;
  943          Sign1 == n, member(Sign2,[n,r]) -> Sign = n
  944        ;
  945          Sign1 == r, Sign2 == n   -> Sign = n
  946        ),
  947        generalize_elem(R1,Literal:Sign2,RestGL,S11,S21,S12,S22), !.
  948
  949generalize_elem([_|R1],Literal,RestGL,S1old,S2old,S1new,S2new) :-
  950        generalize_elem(R1,Literal,RestGL,S1old,S2old,S1new,S2new).
  951
  952
  953%************************************************************************
  954%*                                                                     
  955%* predicate: gti/3, gti/5                                             
  956%*                                                                     
  957%* syntax: gti(+C1,+C2,-C), gti(+C1,+C2,-C,-S1,-S2)                    
  958%*                                                                     
  959%* args: C1,C2,C: clauses in list notation                             
  960%*       S1,S2:   substitutions  [ V1/Term1 , .... ]                 
  961%*                                                                     
  962%* description: generalization thru intersection
  963%*              least general intersection                       
  964%*                                                                     
  965%* example:                                                            
  966%*                                                                     
  967%* peculiarities: the resulting clause might be unconnected            
  968%*                ( see connectedness.pl )                             
  969%*                                                                     
  970%* see also:                                                           
  971%*                                                                     
  972%************************************************************************
  973
  974
  975gti(C1,C2,C):- gti(C1,C2,C,_S1,_S2).
  976
  977
  978gti(Id1,Id2,ID,S1,S2):- 
  979     integer(Id1), integer(Id2), !,
  980     get_clause(Id1,_,_,C1,_),
  981     get_clause(Id2,_,_,C2,_),
  982     gti(C1,C2,C,S1,S2),
  983     store_clause(_,C,gti,ID).
  984
  985
  986gti([H1:p|C1],[H2:p|C2],[H:p|C],S1,S2):- 
  987     lgg_terms(H1,H2,H,Phi1,Phi2),
  988     gti(C1,C2,C,Phi1,Phi2,S1,S2).
  989
  990
  991
  992
  993gti([], _, [], S1, S2, S1, S2).
  994
  995gti( [L1:Sign1|Rest1], C2, [L:Sign|Rest], Phi1, Phi2, S1, S2):-
  996      nth1( _N, C2, L2:Sign2, Rest2),          % subtract L2 from C2
  997      lgg_terms( L1, L2, L,Theta1, Theta2, Phi1, Phi2),
  998      nonvar(L),
  999      ( Sign1 = r, Sign2 = r -> Sign = r
 1000        | otherwise          -> Sign = n),
 1001      gti( Rest1, Rest2, Rest, Theta1, Theta2, S1, S2).
 1002
 1003gti( [_|Rest1], C2, Rest, Phi1, Phi2, S1, S2):-
 1004      gti( Rest1, C2, Rest, Phi1, Phi2, S1, S2). 
 1005
 1006
 1007
 1008
 1009%************************************************************************
 1010%*                                                                     
 1011%* predicate:   lgti/3, lgti/5, lgti/6                                 
 1012%*                                                                     
 1013%* syntax: lgti(+C1,+C2,-C,-S1,-S2),lgti(+C1,+C2,-C,-S1,-S2,+Bound)    
 1014%*                                                                     
 1015%* args: C1,C2,C,S1,S2: see gti above                                  
 1016%*              Bound : pos. integer                                   
 1017%*                                                                     
 1018%* description: apply gti-operator Bound times ( default: Bound = 10 ).
 1019%*              Return the longest resulting clause & substitutions.   
 1020%*                                                                     
 1021%* example:                                                            
 1022%*                                                                     
 1023%* peculiarities:                                                      
 1024%*                                                                     
 1025%* see also:                                                           
 1026%*                                                                      
 1027%***********************************************************************
 1028
 1029lgti(ID1,ID2,ID):-
 1030     integer(ID1), integer(ID2),!,
 1031     lgti(ID1, ID2,C, _,_,10),
 1032     ( store_clause(_,C,lgti,ID); delete_clause(ID),fail ).
 1033
 1034lgti(C1,C2,C,S1,S2):- lgti(C1,C2,C,S1,S2,10).
 1035
 1036
 1037
 1038lgti(Id1,Id2,C,S1,S2,Bound):- 
 1039     integer(Id1), integer(Id2), !,
 1040     get_clause(Id1,_,_,C1,_),
 1041     get_clause(Id2,_,_,C2,_),
 1042     lgti(C1,C2,C,S1,S2,Bound).
 1043
 1044
 1045lgti(C1,C2,C,S1,S2,Bound):-
 1046        integer(Bound), Bound > 0,
 1047        init_chart(C1,C2,Bound),
 1048        !,
 1049        chart(_,_,_,_,_,_),
 1050        findall(Comp, chart(Comp,_,_,_,_,_), Bag),
 1051        once(maximum(Bag, MaxComp)),
 1052        once(retract( chart(MaxComp, C, C1,C2,S1, S2) )).
 1053
 1054:- dynamic(chart/6). 1055
 1056
 1057init_chart(C1,C2,Bound):-
 1058        retractall( chart_count(_) ),
 1059        assert(chart_count(1) ),
 1060        retractall( chart(_,_,_,_,_,_) ),
 1061        !,
 1062        init_chart1(C1,C2,Bound).
 1063
 1064
 1065init_chart1(C1,C2,Bound):-
 1066        gti( C1,C2,C,S1,S2 ),
 1067        once((complexity( C, Comp),              % no backtracking thru this
 1068              assertz( chart(Comp, C, C1,C2,S1, S2) ),
 1069              retract(chart_count(I) ),
 1070              J is I + 1,
 1071              assert( chart_count(J) )
 1072        )), 
 1073        J > Bound.
 1074
 1075init_chart1(_,_,_):-!.  % if there are less than Bound solutions.