1% MODULE bu_basics EXPORTS
    2:- module( bu_basics, 
    3	 [ addtolist/1,
    4           getlist/1,
    5           subs_build_clause/1,
    6           msg_build_long_clause/1,
    7           msg_build_heads/1,
    8           msg_build_body/1,
    9           annotate_redundancy/1,
   10           abs_process_proofs/2,
   11           abs_build_body/1,
   12           ident_process_proofs/2,
   13           ident_build_body/1,
   14           g1_build_clause/2,
   15           g1_process_proofs/2,
   16           idev_build_clause1/1,
   17           idev_build_clause/2,
   18	   process_new_literals/2,
   19           sat_build_clause/3,
   20           head/3,
   21	   body/3,
   22           assumption/3,
   23	   assert_absorptions/2,
   24           assert_clause/1,
   25	   assert_body/1,
   26	   assert_body_unique/1,
   27           assert_body_randomly/1,
   28           cover_assert_assumptions/1,
   29	   retract_body_literals/1,
   30           retract_literals/1,
   31           assert_literals/1,
   32	   clear_mngr/0,
   33	   reset_counts/0]).   34
   35% IMPORTS
   36:- use_module(home(div_utils),
   37              [contains_duplicates/1]).   38:- use_module_if_exists(library(basics),[member/2]).   39:- use_module_if_exists(library(random),[maybe/0]).   40
   41% METAPREDICATES
   42% none
   43
   44:- dynamic head/3.     % head( Literal, {old,new}, Counter)
   45:- dynamic body/3.     % body( Literal, {old,new}, Counter)
   46                       % the second argument is used to check whether
   47                       % saturation/idev resulted in a new literal at all.
   48                       % the third argument is 0 for new literals that 
   49                       % resulted from sat/idev, and \= 0 for literals that
   50                       % have been used for sat/idev
   51:- dynamic assumption/3.   52
   53%***********************************************************************
   54%*	
   55%* module: bu_utils.pl        					
   56%*									
   57%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend              date:12/92	
   58%*									
   59%* changed:								
   60%*									
   61%* description:	utilities for bottom-up operators
   62%*		
   63%* see also:								
   64%*									
   65%***********************************************************************
   66
   67%***********************************************************************
   68%*									
   69%* predicate:	process_new_literals/2							
   70%*									
   71%* syntax: process_new_literals(+[H:Proof|_],-Flag)
   72%*									
   73%* args: H = Lit/M where M is in {new_head,new_body}, or H = []
   74%*       Proof = [[Lit,N],..,[],...] where N in {head,body} 	
   75%*									
   76%* description:	asserts all new heads and bodies of matched clauses
   77%*              via head/3 and body/3
   78%*              Flag = 1 if at least one existed
   79%*									
   80%* example:								
   81%*									
   82%* peculiarities:	none				
   83%*									
   84%* see also:								
   85%*									
   86%***********************************************************************
   87
   88process_new_literals([],_).
   89
   90
   91process_new_literals([ []:_Proof| Rest] , Flag):-
   92	process_new_literals(Rest,Flag).
   93
   94process_new_literals([ L/new_body:_Proof| Rest] , Flag):-
   95	body(L,_,_) ,
   96	!,
   97	process_new_literals(Rest,Flag).
   98
   99process_new_literals([ L/new_head:_Proof| Rest] , Flag):-
  100	head(L,_,_),
  101	!,
  102	process_new_literals(Rest,Flag).
  103
  104process_new_literals([ (_L/_):Proof| Rest] , Flag):-
  105	contains_duplicates(Proof), %%eigentlich ein Filter: jedem Literal 
  106                                    %%im Parent entspricht eines in der Resolvente
  107	!,
  108	process_new_literals(Rest,Flag).
  109
  110process_new_literals([ (L/new_head):Proof| Rest] , 1):-
  111	!,
  112	assert( head(L,new,0) ),
  113	annotate(Proof),
  114	process_new_literals(Rest,_).
  115
  116process_new_literals([ (L/new_body):Proof| Rest] , 1):-
  117	assert( body(L,new,0) ),
  118	annotate(Proof),
  119	process_new_literals(Rest,_).
  120
  121% for backtracking
  122process_new_literals([ (L/new_body):_Proof| Rest] , Flag):-
  123	retract( body(L,new,0) ),
  124	process_new_literals(Rest,Flag).
  125
  126
  127%***********************************************************************
  128%*									
  129%* predicate:	annotate/1							
  130%*									
  131%* syntax: annotate(+Proofs)								
  132%*									
  133%* args: Proofs = [L1,..,Ln] where Li = [] or Li = [Lit,N] and N in {head,body}
  134%*									
  135%* description: increments counter for each head/body literal in Proofs
  136%*									
  137%* example:								
  138%*									
  139%* peculiarities:	none				
  140%*									
  141%* see also:								
  142%*									
  143%***********************************************************************
  144
  145annotate([]).
  146
  147annotate([ [L,body] | Rest ]):-
  148	retract( body( L,OldNew,I)),
  149	J is I + 1,
  150	assert( body(L,OldNew,J) ),
  151	annotate(Rest).
  152annotate([ [L,head] | Rest ]):-
  153	retract( head( L,OldNew,I)),
  154	J is I + 1,
  155	assert( head(L,OldNew,J)) ,
  156	annotate(Rest).
  157
  158annotate([ [] | Rest]):-
  159	annotate(Rest).
  160
  161
  162
  163%***********************************************************************
  164%*									
  165%* predicate:	abs_process_proofs/2							
  166%*									
  167%* syntax: abs_process_proofs(+Proofs,-Head)
  168%*									
  169%* args: Proofs = [CL1,..,CLn] where CLi is a clause in list notation
  170%*       Head: a head literal								
  171%*									
  172%* description:	returns a head literal from one of the CLi, and retracts
  173%*              the according body literals body(L,_,_) of CLi (destructive
  174%*              absorption)
  175%*									
  176%* example:								
  177%*									
  178%* peculiarities:	none				
  179%*									
  180%* see also:								
  181%*									
  182%***********************************************************************
  183
  184abs_process_proofs([ [Head:p|_] | MoreHeads ] , NewHead ):-
  185        body(Head,_,_),
  186	!,
  187        abs_process_proofs(MoreHeads, NewHead ).
  188
  189abs_process_proofs([ [_|Proof] | MoreHeads ] , NewHead ):-
  190        contains_duplicates(Proof), %%eigentlich ein Filter: jedem Literal 
  191                                    %%im Parent entspricht eines in der Resolvente
  192	!,
  193        abs_process_proofs(MoreHeads, NewHead ).
  194
  195abs_process_proofs([ [Head:p|Proof] | _MoreHeads ] , Head ):-
  196        retract_body_literals(Proof).
  197
  198% For Backtracking
  199abs_process_proofs([ [_Head:p|Proof] | MoreHeads ] , NewHead ):-
  200        assert_body(Proof),
  201        abs_process_proofs(MoreHeads, NewHead ).
  202
  203
  204
  205%***********************************************************************
  206%*									
  207%* predicate:	ident_process_proofs/2						
  208%*									
  209%* syntax: ident_process_proofs(+[[H:Proof]|_],-Head)
  210%*									
  211%* args: H =	 = Lit/M where M is in {new_head,new_body}, or H = []
  212%*       Proof = [[Lit,N],..,[],...] where N in {head,body}
  213%*       Head: a literal
  214%*									
  215%* description:	returns a head literal from one of the H:Proof, and retracts 
  216%*              the according literals from Proof from the kb
  217%*									
  218%* example:								
  219%*									
  220%* peculiarities:	none				
  221%*									
  222%* see also:								
  223%*									
  224%***********************************************************************
  225
  226ident_process_proofs([ [(Head/new_head):_] | MoreHeads ] , NewHead ):-
  227        head(Head,_,_),          %  
  228	!,
  229        ident_process_proofs(MoreHeads, NewHead ).
  230
  231ident_process_proofs([ [(_/_):Proof] | MoreHeads ] , NewHead ):-
  232        contains_duplicates(Proof), %%eigentlich ein Filter: jedem Literal 
  233                                    %%im Parent entspricht eines in der Resolvente
  234	!,
  235        ident_process_proofs(MoreHeads, NewHead ).
  236
  237ident_process_proofs([ [ (Head/new_head):Proof] | _MoreHeads ] , Head ):-
  238        retract_literals(Proof).
  239
  240% for backtracking
  241ident_process_proofs([ [ (_Head/new_head):Proof] | MoreHeads ] , NewHead ):-
  242        assert_literals(Proof),
  243        % write('new kb'),nl,subsume_mngr:show_heads,subsume_mngr:show_bodies,nl,
  244        ident_process_proofs( MoreHeads, NewHead).
  245
  246
  247
  248%***********************************************************************
  249%*									
  250%* predicate:	g1_process_proofs/2						
  251%*									
  252%* syntax: g1_process_proofs(+[[H:Proof]|_],-Lit)
  253%*									
  254%* args: H =	 = Lit/M where M is in {new_head,new_body}, or H = []
  255%*       Proof = [[Lit,N],..,[],...] where N in {head,body}
  256%*       Lit:  a literal and its sign
  257%*									
  258%* description:	returns the resolution literal from one of the H:Proof, and retracts 
  259%*              the according literals from Proof from the kb
  260%*									
  261%* example:								
  262%*									
  263%* peculiarities:	none				
  264%*									
  265%* see also:								
  266%*									
  267%***********************************************************************
  268
  269g1_process_proofs([[]:_|R],Lit):-
  270       g1_process_proofs(R,Lit).
  271
  272g1_process_proofs([ (Head/new_head):_ | MoreHeads ] , Lit ):-
  273        head(Head,_,_),           
  274	!,
  275        g1_process_proofs(MoreHeads, Lit ).
  276
  277
  278g1_process_proofs([ (Body/new_body):_ | MoreHeads ] , Lit ):-
  279        body(Body,_,_),            
  280	!,
  281        g1_process_proofs(MoreHeads, Lit ).
  282
  283g1_process_proofs([ (_/_):Proof | MoreHeads ] , Lit ):-
  284        contains_duplicates(Proof),%%eigentlich ein Filter: jedem Literal 
  285                                    %%im Parent entspricht eines in der Resolvente
  286	!,
  287        g1_process_proofs(MoreHeads, Lit ).
  288
  289g1_process_proofs([ (Lit/S0):Proof | _MoreHeads ] , Lit:S ):-
  290        (   S0 = new_head -> S = p ; S = n ),
  291        retract_literals(Proof).
  292
  293% for backtracking
  294g1_process_proofs([ (_/_):Proof | MoreHeads ] , Lit ):-
  295        assert_literals(Proof),
  296        % write('new kb'),nl,subsume_mngr:show_heads,subsume_mngr:show_bodies,nl,
  297        g1_process_proofs( MoreHeads, Lit).
  298
  299
  300%***********************************************************************
  301%*									
  302%* predicate:	assert_absorptions/2							
  303%*									
  304%* syntax: assert_assorptions(+[CL|_],-Flag)
  305%*									
  306%* args: CL: clause in list notation
  307%*									
  308%* description: asserts heads H of all absorbed clauses, if new, as 
  309%*              body(H,_,_). Flag=1 if at least one existed	
  310%*									
  311%* example:								
  312%*									
  313%* peculiarities:	none				
  314%*									
  315%* see also:								
  316%*									
  317%***********************************************************************
  318
  319
  320assert_absorptions([],_F).
  321assert_absorptions([ [Head:p|_] |MoreHeads] ,F):-
  322        body( Head,_OldNew,_Count) ,
  323        !,
  324        assert_absorptions(MoreHeads,F).
  325
  326assert_absorptions([ [Head:p|Proof]|MoreHeads],1 ):-
  327        assert( body(Head,new,0) ),
  328        annotate_redundancy(Proof),
  329        assert_absorptions(MoreHeads, 1).
  330
  331% For Backtracking
  332assert_absorptions([ [Head:p|_Proof]|_MoreHeads],_ ):-
  333        retract( body(Head,new,0) ).
  334
  335
  336%***********************************************************************
  337%*									
  338%* predicate:	annotate_redundancy/1							
  339%*									
  340%* syntax: annotate_redundancy(+Proof)
  341%*									
  342%* args: Proof: clause in list notation
  343%*									
  344%* description:	increments counter for each body literal in Proof
  345%*									
  346%* example:								
  347%*									
  348%* peculiarities:	none				
  349%*									
  350%* see also:								
  351%*									
  352%***********************************************************************
  353
  354annotate_redundancy([]).
  355annotate_redundancy([ L:_ | More ] ):-
  356        retract( body(L,OldNew,I) ),
  357        J is I + 1,
  358        assert( body(L,OldNew,J)),
  359        annotate_redundancy(More).
  360
  361
  362%***********************************************************************
  363%*									
  364%* predicate: assert_body_randomly/1
  365%*									
  366%* syntax: assert_body_randomly(+Clause_list)
  367%*									
  368%* args: +Clause_list ... Clause in list notation
  369%*									
  370%* description:	assert body literals in random order
  371%*									
  372%* example:								
  373%*									
  374%* peculiarities:	none				
  375%*									
  376%* see also:								
  377%*									
  378%***********************************************************************
  379
  380assert_body_randomly([]):-!.
  381
  382assert_body_randomly([H:p | More]):- 
  383       head(H,_,_),!,
  384       assert_body_randomly(More).
  385
  386assert_body_randomly([H:p | More]):- 
  387       assert(head(H,_,_)),
  388       assert_body_randomly(More).
  389
  390assert_body_randomly([L:_ | More]):-
  391       body(L,_,_),!,
  392       assert_body_randomly(More).
  393
  394assert_body_randomly([L:_ | More]):- 
  395       maybe,
  396       asserta( body(L,old,0) ),
  397       assert_body_randomly(More).
  398
  399assert_body_randomly([L:_ | More]):-
  400       assertz( body(L,old,0) ),  
  401       assert_body_randomly(More).
  402
  403%***********************************************************************
  404%*									
  405%* predicate:	addtolist/1							
  406%*									
  407%* syntax: addtolist(+ToAdd)								
  408%*									
  409%* args: ToAdd .. Id or list of Id's
  410%*									
  411%* description: asserts list of Id's	
  412%*									
  413%* example:								
  414%*									
  415%* peculiarities:	none				
  416%*									
  417%* see also: 							
  418%*									
  419%***********************************************************************
  420
  421addtolist([L|IST]) :- 
  422	retract(id_list(List1)), 
  423	append(List1,[L|IST],List2),
  424	assertz(id_list(List2)), !.
  425addtolist(Id) :- retract(id_list(List1)), assertz(id_list([Id|List1])), !.
  426addtolist([L|IST]) :- assertz(id_list([L|IST])), !.
  427addtolist(Id) :- assertz(id_list([Id])), !.
  428
  429
  430%***********************************************************************
  431%*									
  432%* predicate:	getlist/1
  433%*									
  434%* syntax: getlist(-ID_list)								
  435%*									
  436%* args:								
  437%*									
  438%* description:	retracts the list of id's that has been asserted by
  439%*		addtolist/1							
  440%* 									
  441%* example:								
  442%*									
  443%* peculiarities:	none				
  444%*									
  445%* see also:								
  446%*									
  447%***********************************************************************
  448
  449getlist(List) :- retract(id_list(List)).
  450
  451
  452%***********************************************************************
  453%*									
  454%* predicate: cover_assert_assumptions
  455%*									
  456%* syntax: cover_assert_assumptions(+Clause_list)
  457%*									
  458%* args: Clause_list .. clause in list representation
  459%*									
  460%* description:	asserts for each literal L in Clause_list assumption(L,_,_)
  461%*              in the kb							
  462%*
  463%* example:								
  464%*									
  465%* peculiarities:	none				
  466%*									
  467%* see also:								
  468%*									
  469%***********************************************************************
  470
  471cover_assert_assumptions([]).
  472cover_assert_assumptions([L:_|More]):-
  473      assertz( assumption(L,_,_) ),
  474      cover_assert_assumptions(More).
  475
  476
  477
  478%***********************************************************************
  479%*									
  480%* predicate: clear_mngr/0								
  481%*									
  482%* syntax:								
  483%*									
  484%* args:								
  485%*									
  486%* description:	retracts all head/3 and body/3 within the knowledge base
  487%*									
  488%* example:								
  489%*									
  490%* peculiarities:	none				
  491%*									
  492%* see also:								
  493%*									
  494%***********************************************************************
  495
  496clear_mngr:- retractall( head(_,_,_) ), retractall( body(_,_,_) ).
  497
  498
  499%***********************************************************************
  500%*									
  501%* predicate:  retract_body_literals/1
  502%*									
  503%* syntax: retract_body_literals(+CL)
  504%*									
  505%* args: CL: clause in list notation
  506%*									
  507%* description:	retracts body(L,_,_) for each L:_ in CL
  508%*									
  509%* example:								
  510%*									
  511%* peculiarities:	none				
  512%*									
  513%* see also:								
  514%*									
  515%***********************************************************************
  516
  517 retract_body_literals( [ L:_| More]):- 
  518	  retract( body(L,_,_) ),
  519	  retract_body_literals(More).
  520 retract_body_literals( []).
  521
  522
  523%***********************************************************************
  524%*									
  525%* predicate:  retract_literals/1
  526%*									
  527%* syntax: retract_literals(+[[Lit,N]|_])
  528%*									
  529%* args: N in {head,body}								
  530%*									
  531%* description:	retracts head(Lit,_,_)/body(Lit,_,_) for each [Lit,head]/
  532%*              [Lit,body] in the input							
  533%*									
  534%* example:								
  535%*									
  536%* peculiarities:	none				
  537%*									
  538%* see also:								
  539%*									
  540%***********************************************************************
  541
  542retract_literals([]).
  543retract_literals([ [L,head] | Rest ]):- 
  544          retract( head(L,_,_)),!,
  545          retract_literals(Rest).
  546retract_literals([ [L,body] | Rest ]):- 
  547          retract( body(L,_,_)),!,
  548          retract_literals(Rest).
  549retract_literals([ [_,_] | Rest ]):-
  550          retract_literals(Rest).
  551retract_literals([ [] | Rest ]):-
  552          retract_literals(Rest).
  553
  554
  555%***********************************************************************
  556%*									
  557%* predicate:  assert_literals/1
  558%*									
  559%* syntax: assert_literals(+[[Lit,N]|_])
  560%*									
  561%* args: N in {head,body}							
  562%*									
  563%* description:	asserts each Lit with [Lit,N] in the input as N(Lit,_,_)
  564%*									
  565%* example:								
  566%*									
  567%* peculiarities:	none				
  568%*									
  569%* see also:								
  570%*									
  571%***********************************************************************
  572
  573assert_literals([]).
  574assert_literals([ [L,head] | Rest ]):- 
  575          asserta( head(L,_,_)),!,
  576          assert_literals(Rest).
  577assert_literals([ [L,body] | Rest ]):- 
  578          assertz( body(L,_,_)),!,
  579          assert_literals(Rest).
  580assert_literals([ [_,_] | Rest ]):-
  581          assert_literals(Rest).
  582assert_literals([ [] | Rest ]):-
  583          assert_literals(Rest).
  584
  585
  586%***********************************************************************
  587%*									
  588%* predicate:  assert_clause/1								
  589%*									
  590%* syntax: assert_clause(+CL)								
  591%*									
  592%* args: CL .. clause in list representation
  593%*									
  594%* description:	asserts positive literals L in CL as head(L,old,0),
  595%*              negative and redundant literals as body(L,old,0).
  596%*									
  597%* example:								
  598%*									
  599%* peculiarities:	none				
  600%*									
  601%* see also:								
  602%*									
  603%***********************************************************************
  604
  605assert_clause(C):- assert_clause1(C).
  606assert_clause(_):- clear_mngr,!,fail. %on backtracking
  607
  608 assert_clause1( []).
  609 assert_clause1([H|T]):- assert_clause1(H), assert_clause1(T).
  610 assert_clause1(H:p):- head(H,_,_).
  611 assert_clause1(H:p):- assertz( head(H,old,0) ).
  612 assert_clause1(H:S):- member(S,[n,r]), body(H,_,_).
  613 assert_clause1(H:S):- member(S,[n,r]), assertz( body(H,old,0) ).
  614
  615
  616%***********************************************************************
  617%*									
  618%* predicate:  assert_body/1								
  619%*									
  620%* syntax: assert_body(+CL)								
  621%*									
  622%* args: CL ... clause body in list representation (only negative and
  623%*              redundant literals)
  624%*									
  625%* description:	asserts each literal L in CL as body(L,old,0)
  626%*									
  627%* example:								
  628%*									
  629%* peculiarities:	none				
  630%*									
  631%* see also:								
  632%*									
  633%***********************************************************************
  634
  635 assert_body( []).
  636 assert_body([H|T]):- assert_body(H), assert_body(T).
  637 assert_body(H:S):- member(S,[n,r]), assertz( body(H,old,0) ).
  638
  639
  640%***********************************************************************
  641%*									
  642%* predicate:  assert_body_unique/1
  643%*									
  644%* syntax: assert_body_unique(+CL)
  645%*									
  646%* args: CL ... clause body in list representation (only negative and
  647%*              redundant literals)
  648%*									
  649%* description:	as assert_body/1, but tests whether body(L,_,_) is already
  650%*              in the kb
  651%*									
  652%* example:								
  653%*									
  654%* peculiarities:	none				
  655%*									
  656%* see also:								
  657%*									
  658%***********************************************************************
  659
  660 assert_body_unique( []).
  661 assert_body_unique([H|T]):- assert_body_unique(H), assert_body_unique(T).
  662 assert_body_unique(H:S):- member(S,[n,r]), body(H,_,_).
  663 assert_body_unique(H:S):- member(S,[n,r]), assertz( body(H,old,0) ).
  664
  665
  666
  667%***********************************************************************
  668%*									
  669%* predicate:  reset_counts/0							
  670%*									
  671%* syntax:								
  672%*									
  673%* args:								
  674%*									
  675%* description:	for each kb-entry head(Lit,_,Count) and body(Lit,_,Count), 
  676%*              Count is set to 0
  677%*									
  678%* example:								
  679%*									
  680%* peculiarities:	none				
  681%*									
  682%* see also:								
  683%*									
  684%***********************************************************************
  685
  686 reset_counts:- retract( body(L,O,_) ), assertz( body(L,O,0) ),fail.
  687 reset_counts:- retract( head(L,O,_) ), assertz( head(L,O,0) ),fail.
  688 reset_counts.
  689
  690%**********************************************************************
  691%*									
  692%* predicate:	subs_build_clause/1							
  693%*									
  694%* syntax: subs_build_clause(-CL)
  695%*									
  696%* args: CL ... Horn clause in list representation
  697%*									
  698%* description:	retracts one entry head(H,_,_) and all entries 
  699%*              body(L,_,_) and builds clause [H:p,..,L:p,...]
  700%*
  701%* example:								
  702%*									
  703%* peculiarities:	none				
  704%*									
  705%* see also:								
  706%*									
  707%***********************************************************************
  708
  709subs_build_clause([H:p|Body]):-
  710	 retract( head(H,_,_) ),
  711	subs_build_clause( Body),!.
  712subs_build_clause([L:n|Body]):-
  713	 retract( body(L,_,_) ),
  714	 subs_build_clause( Body ).
  715subs_build_clause([]):- !.
  716
  717
  718%***********************************************************************
  719%*									
  720%* predicate:	sat_build_clause/3							
  721%*									
  722%* syntax: sat_build_clause(+H,+B,-CL)
  723%*									
  724%* args: H ... head
  725%*       B ... list of body literals
  726%*       CL ... Horn clause in list representation
  727%*									
  728%* description:	build clause CL = [H:p,...,L:M,....] for each L in B.
  729%*		M is n, if body(L,_,_) is true, else M is r
  730%* 									
  731%* example:								
  732%*									
  733%* peculiarities:	none				
  734%*									
  735%* see also:								
  736%*									
  737%***********************************************************************
  738
  739sat_build_clause(H,B,[H:p|B1]):-
  740        sat_build_body(B,B1).
  741sat_build_body([],[]).
  742sat_build_body( [L|B],[L:n|B1]):-          % nonredundant literal
  743        body( L,_,0),
  744        !,
  745        sat_build_body(B,B1).
  746sat_build_body( [L|B], [L:r|B1]):-         % (probably) superfluos literal
  747        sat_build_body( B,B1).
  748
  749
  750
  751%***********************************************************************
  752%*									
  753%* predicate:	msg_build_long_clause/1							
  754%*									
  755%* syntax: msg_build_long_clause(-CL)
  756%*									
  757%* args: CL ... a general clause in list representation
  758%*									
  759%* description:	
  760%*									
  761%* example:								
  762%*									
  763%* peculiarities:	none				
  764%*									
  765%* see also:								
  766%*									
  767%***********************************************************************
  768
  769
  770msg_build_long_clause( Clause):-
  771    msg_build_heads( Heads ),
  772    msg_build_body( Body),
  773    append( Heads, Body, Clause),!.
  774
  775
  776%***********************************************************************
  777%*									
  778%* predicate:	msg_build_heads/1							
  779%*									
  780%* syntax: msg_build_heads(-CL)								
  781%*									
  782%* args: CL ... clause in list representation, consisting only of 
  783%*              positive literals
  784%*									
  785%* description:	collects all Literals L such that head(L,_,_) is in kb,
  786%*              and returns CL = [...,L:p,....]
  787%*									
  788%* example:								
  789%*									
  790%* peculiarities:	none				
  791%*									
  792%* see also:								
  793%*									
  794%***********************************************************************
  795
  796msg_build_heads( [ H:p | More ]):-
  797    retract( head(H,F,I) ),
  798    msg_build_heads( More),
  799    asserta( head(H,F,I) ).
  800msg_build_heads([]):- !.
  801
  802
  803%***********************************************************************
  804%*									
  805%* predicate:	msg_build_body/1							
  806%*									
  807%* syntax: msg_build_body(-CL)								
  808%*									
  809%* args: CL ... clause in list representation, consisting only of 
  810%*              negative and redundant literals
  811%*									
  812%* description:	collects all Literals L such that body(L,_,_) is in kb,
  813%*              and returns CL = [...,L:M,....], M in {n,r}
  814%*									
  815%* example:								
  816%*									
  817%* peculiarities:	none				
  818%*									
  819%* see also:								
  820%*									
  821%***********************************************************************
  822
  823msg_build_body( [ H:Sign | More ]):-
  824	retract( body(H,F,I) ),
  825	( I = 0 -> Sign = n ; Sign = r),
  826	msg_build_body(More),!,
  827	asserta( body(H,F,I) ).
  828
  829msg_build_body([]):-!.
  830
  831
  832%***********************************************************************
  833%*									
  834%* predicate:	idev_build_clause1/1							
  835%*									
  836%* syntax: idev_build_clause1(-CL)
  837%*							
  838%* args: CL .. Horn clause in list representation
  839%*									
  840%* description:								
  841%*									
  842%* example:								
  843%*									
  844%* peculiarities:	none				
  845%*									
  846%* see also:								
  847%*									
  848%***********************************************************************
  849
  850idev_build_clause1( [H:p|More] ):-
  851	retract( head(H,F,0) ),!, % the head is unique !
  852	idev_build_body(More),
  853	asserta(head(H,F,0) ).
  854
  855%***********************************************************************
  856%*									
  857%* predicate:	idev_build_body/1							
  858%*									
  859%* syntax: idev_build_body(-CL)								
  860%*							
  861%* args: CL ... clause in list represenation, only negative and redundant literals
  862%*									
  863%* description:	collects all L such that body(L,_,_) is in kb
  864%*									
  865%* example:								
  866%*									
  867%* peculiarities:	none				
  868%*									
  869%* see also:								
  870%*									
  871%***********************************************************************
  872
  873idev_build_body( [ H:Sign | More ]):-
  874	retract( body(H,F,I) ),
  875	( I = 0 -> Sign = n ; Sign = r),
  876	idev_build_body(More),!,
  877	asserta( body(H,F,I) ).
  878
  879idev_build_body([]):-!.
  880
  881
  882
  883%***********************************************************************
  884%*									
  885%* predicate:	idev_build_clause/2							
  886%*									
  887%* syntax: idev_build_clause(+H,-CL)
  888%*							
  889%* args: CL .. clause in list representation
  890%*       H ... preferred head of CL
  891%*									
  892%* description:	as idev_build_clause1/1, but with preferred head in CL
  893%*									
  894%* example:								
  895%*									
  896%* peculiarities:	none				
  897%*									
  898%* see also:								
  899%*									
  900%***********************************************************************
  901
  902idev_build_clause(PrefHead, [H:p|More]):-
  903    idev_build_head( PrefHead, H),
  904    idev_build_body(More),!.
  905
  906%***********************************************************************
  907%*									
  908%* predicate:	idev_build_head/2							
  909%*									
  910%* syntax: idev_build_head(+PrefH,-H)
  911%*							
  912%* args: PrefH, H .. clause heads
  913%*									
  914%* description:	returns H such that head(H,_,_) in kb and PrefH and H
  915%*		unifiable. If none exists, the first H with head(H,_,_) in kb
  916%* 		is returned.							
  917%*									
  918%* example:								
  919%*									
  920%* peculiarities:	none				
  921%*									
  922%* see also:								
  923%*									
  924%***********************************************************************
  925
  926idev_build_head(PrefHead,PrefHead):-
  927    retract( head(PrefHead,F,N) ),!,
  928    asserta( head(PrefHead,F,N) ).
  929
  930idev_build_head( _, Head):-
  931    head( Head,_,_).
  932    % retract( head(Head,F,N) ),
  933    % !,
  934    % asserta( head(H,F,N) )
  935
  936 
  937
  938
  939%***********************************************************************
  940%*									
  941%* predicate:	ident_build_body/1							
  942%*									
  943%* syntax: ident_build_body(-CL)
  944%*									
  945%* args: CL ... clause in list notation, contains only negative literals
  946%*									
  947%* description:	CL = [...,L:n,...] for each L such that body(L,_,0) in kb
  948%*									
  949%* example:								
  950%*									
  951%* peculiarities:	none				
  952%*									
  953%* see also:								
  954%*									
  955%***********************************************************************
  956
  957ident_build_body( [ L:n | Rest ]):-
  958	retract( body( L, _, 0) ) ,
  959	!,
  960        ident_build_body( Rest),
  961        assertz( body( L,old,0) ).    % for backtracking
  962ident_build_body([]):-!.
  963
  964
  965
  966%***********************************************************************
  967%*									
  968%* predicate:	g1_build_clause/2							
  969%*									
  970%* syntax: g1_build_clause(+ResLit,-CL)
  971%*									
  972%* args: CL ... Horn clause in list notation
  973%*       ResLit ... the resolution literal
  974%*									
  975%* description:	CL is the second parent clause for the g1-operator
  976%*									
  977%* example:								
  978%*									
  979%* peculiarities:	none				
  980%*									
  981%* see also:								
  982%*									
  983%***********************************************************************
  984
  985g1_build_clause( L:p, [ L:p | Body ]):-
  986        ident_build_body(Body),!.
  987g1_build_clause( L:n, [ H:p, L:n | Body ]):- 
  988        ident_build_body(Body),
  989	retract( head( H, _, 0) ) ,
  990	!,
  991        assertz( head( L,old,0) ).   
  992
  993
  994%***********************************************************************
  995%*									
  996%* predicate:	abs_build_body/1							
  997%*									
  998%* syntax: abs_build_body(-CL)								
  999%*									
 1000%* args: CL .. clause in list representation, contains only negative literals
 1001%*									
 1002%* description:	CL = [...,L:n,....] for each L such that body(L,_,_) in kb
 1003%*									
 1004%* example:								
 1005%*									
 1006%* peculiarities:	none				
 1007%*									
 1008%* see also:								
 1009%*									
 1010%***********************************************************************
 1011
 1012
 1013abs_build_body( [ L:n | Rest ]):-
 1014	retract( body( L, F, I) ) ,
 1015	!,
 1016        abs_build_body( Rest),
 1017        assert( body(L,F,I) ).
 1018abs_build_body([]):-!