1% MODULE evaluation EXPORTS
    2
    3:- module( evaluation,
    4	[ covered_pos_examples/1,
    5          covered_neg_examples/1,
    6          all_covered_examples/1,
    7          
    8	  complexity/2,
    9          clear_evaluation/0,
   10          evaluated/1,
   11          change_evaluated/1,
   12
   13          eval_examples/0,             % Compute complete evaluation for all examples
   14                                       % AND clauses in kb
   15          eval_pos_examples/1,         % Compute evaluation for all pos examples in kb
   16	  complete_chk/0,              % check completeness, all pos examples covered?
   17	  correct_chk/0,               % check correctness, no neg examples covered?
   18 	  fp/1,
   19          fpo/1,
   20          fp_hyp/1, 
   21          ip/1,
   22          herbrand_base_ff/1,
   23          ivonTunterE/1,ivonBundE/1, 
   24          code_length/2,
   25          encoding_length_examples/1,
   26          encoding_length_clause/2]).   27
   28%IMPORTS
   29:- use_module(home(div_utils),
   30              [make_unique/2,insert_unique/4,sort_by_length/3,mysetof/3,
   31               remove/3,append_all/2,sum/2,identical_make_unique/2,best/2,
   32               remove_variant/3,make_unique/2,
   33               fak/2,fak1/3,nueberk/3,log2/2,log2nueberk/3,sum_of_logs/3]).   34:- use_module(home(environment),
   35              [ask_for/1]).   36:- use_module(home(var_utils),
   37              [term_size/2,vars/2,skolemize/3]).   38:- use_module(home(kb),
   39              [get_example/3,ex/3,known/6,assertallz/1,get_predlist/1,
   40               get_evaluation/2,delete_example/1,delete_clause/1,get_clause/5]).   41:- use_module(home(interpreter),
   42              [prooftrees/3,solve_once/3,proof_close/2,
   43               solve/3,ip_part1/2,ip_part2/3]).   44:- use_module_if_exists(library(basics),
   45              [member/2]).   46:- use_module_if_exists(library(subsumes),
   47              [subsumes_chk/2,variant/2]).   48:- use_module_if_exists(library(occurs),
   49              [sub_term/2]).   50:- use_module_if_exists(library(math),
   51              [pow/3]).   52
   53
   54% METAPREDICATES
   55% none
   56
   57
   58
   59:- dynamic evaluated/1.   60
   61
   62%***********************************************************************
   63%*	
   64%* module: evaluation.pl        					
   65%*									
   66%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend              date:12/92
   67%*									
   68%* changed:								
   69%*									
   70%* description:	evaluation of (parts of) the knowledge base
   71%*                                                                      
   72%* see also:	
   73%*									
   74%***********************************************************************
   75
   76
   77
   78%***********************************************************************
   79%*									
   80%* predicate:	ip/1							
   81%*									
   82%* syntax:	ip(-UA_List)							
   83%*									
   84%* args: -UA_List ... list of ground atoms
   85%*									
   86%* description:	Shapiro's algorithm for diagnosing finite failure       
   87%*              ip in our framework. Returns a set of ground atoms that        
   88%*              has to be covered to make all uncovered positive        
   89%*              examples succeed.
   90%*  	        Allows backtracking on alternative sets of ground atoms
   91%*              that make all examples succeed. 
   92%*									
   93%* example:								
   94%*									
   95%* peculiarities:	none						
   96%*									
   97%* see also:								
   98%*									
   99%***********************************************************************
  100
  101ip(UA_List):-
  102   (   evaluated(no) ->
  103       eval_examples
  104   ;   true
  105   ),
  106   mysetof(E,I^Trees^(get_example(I,E,'+'),prooftrees(I,fail,Trees)),Elist),!,
  107   ip_list(Elist,[],UA_List1),
  108   make_unique(UA_List1,UA_List).
  109
  110ip_list([],L,L).
  111ip_list([E|R],L,L2):-
  112   ip0(E,UAs),
  113   append(L,UAs,L1),
  114   ip_list(R,L1,L2).
  115
  116
  117
  118%***********************************************************************
  119%*									
  120%* predicate:								
  121%*									
  122%* syntax:	ip(+UA,-UAs)							
  123%*									
  124%* args:								
  125%*									
  126%* description: UA is an uncovered atom, i.e. both prooftrees(I,fail,Trees) 
  127%*   	and ex(I,UA,+) are in the knowledge base.
  128%*   	UAs is a list [A1,...,An] such that a proof of UA would 
  129%*   	succeed if A1 through An were covered by the knowledge base.
  130%*   	Cave!: Extensive oracle interaction
  131%*
  132%* example:								
  133%*									
  134%* peculiarities:	none						
  135%*									
  136%* see also:								
  137%*									
  138%***********************************************************************
  139
  140ip0(Goal,UAs):-
  141   setof(Proof,Goal^ip_part1(Goal,Proof),Proofs0),
  142   append_all(Proofs0,Proofs1),
  143   proof_close(Proofs1,Proofs),!,
  144   ip_part2(Proofs,Goal,UAs0),
  145   make_unique(UAs0,UAs).
  146
  147
  148%***********************************************************************
  149%*									
  150%* predicate:	fp/1							
  151%*									
  152%* syntax:	fp(-OR)						
  153%*									
  154%* args:	OR:							
  155%*									
  156%* description: a kind of shapiro's contradiction backtracing that      
  157%*              aims to detect possibly overgeneral clauses.
  158%*              As it does not use an oracle, all possibly overgeneral
  159%*              clauses are considered and a minimal combination 
  160%*              such that all negative examples become uncovered is
  161%*              returned.
  162%*              Allows backtracking to an alternative set of possibly
  163%*              overgeneral clauses
  164%* 	        OR is a list [I:E,...], where I is the index of a possibly
  165%*   	        overgeneral clause and E is the set of wrong (head-)instantiations of
  166%*   	        clause I that should be excluded by specializing I.
  167%*   	        OR is a minimal selection of possibly overgeneral clauses such
  168%*   	        that by specialising them all negative examples become uncovered.
  169%*   	        On backtracking, the second selection is returned, and so on.
  170%*									
  171%* example:								
  172%*									
  173%* peculiarities:	none						
  174%*									
  175%* see also:								
  176%*									
  177%***********************************************************************
  178
  179fp(OR):-
  180   (   evaluated(no) ->
  181       eval_examples
  182   ;   true
  183   ),
  184   bagof(TL,I^E^Trees^P^(get_example(I,E,'-'),prooftrees(I,success,Trees),
  185                         member(P,Trees),fp(P,[],TL)), TList),
  186   collect_indices(TList,[],Indices),
  187   or_subsets(Indices,TList,OR_List),!,
  188   best(OR_List,OR).
  189fp([]).
  190
  191
  192%***********************************************************************
  193%*									
  194%* predicate:	fp/3							
  195%*									
  196%* syntax: fp(+Prooftree,+L,-L)								
  197%*									
  198%* args: Prooftree is a prooftree for a succeeding negative example
  199%*       L = [...,ID:[G1,..,Gn],...] where ID is a clause index and
  200%*       G1,..,Gn are the head instantiations  the clause has been applied with
  201%*       during the proof Prooftree.
  202%*									
  203%* description:	collects clauses and goals that have been used during 
  204%*              a successfull proof of a negative example
  205%*									
  206%* example:								
  207%*									
  208%* peculiarities:	none						
  209%*									
  210%* see also:								
  211%*									
  212%***********************************************************************
  213
  214fp([sys,_,_],L,L):- !.
  215fp([I,A,SG],L,L2):-
  216   fp_list(SG,L,L1),
  217   insert_unique(I,A,L1,L2).
  218
  219fp_list([],L,L).
  220fp_list([G|R],L,L2):-
  221   fp_list(R,L,L1),
  222   fp(G,L1,L2).
  223
  224
  225
  226%***********************************************************************
  227%*									
  228%* predicate:	fp_hyp/1							
  229%*									
  230%* syntax:	fp_hyp(-OR)						
  231%*									
  232%* args:	OR:							
  233%*									
  234%* description: as fp/1, but considers only clauses with label 'hypo' as 
  235%*              possibly overgeneral
  236%*              Allows backtracking to an alternative set of possibly
  237%*              overgeneral clauses
  238%* 	        OR is a list [I:E,...], where I is the index of a possibly
  239%*   	        overgeneral clause and E is the set of wrong (head-)instantiations of
  240%*   	        clause I that should be excluded by specializing I.
  241%*   	        OR is a minimal selection of possibly overgeneral clauses such
  242%*   	        that by specialising them all negative examples become uncovered.
  243%*   	        On backtracking, the second selection is returned, and so on.
  244%*									
  245%* example:								
  246%*									
  247%* peculiarities:	none						
  248%*									
  249%* see also:								
  250%*									
  251%***********************************************************************
  252
  253fp_hyp(OR):-
  254   (   evaluated(no) ->
  255       eval_examples
  256   ;   true
  257   ),
  258   bagof(TL,I^E^Trees^P^(get_example(I,E,'-'),prooftrees(I,success,Trees),
  259                         member(P,Trees),fp_hyp(P,[],TL)), TList),
  260   collect_indices(TList,[],Indices),
  261   or_subsets(Indices,TList,OR_List),!,
  262   best(OR_List,OR).
  263fp_hyp([]).
  264
  265
  266%***********************************************************************
  267%*									
  268%* predicate:	fp_hyp/3							
  269%*									
  270%* syntax: fp_hyp(+Prooftree,+L,-L)	
  271%*									
  272%* args: Prooftree is a prooftree for a succeeding negative example
  273%*       L = [...,ID:[G1,..,Gn],...] where ID is a clause index of a clause with
  274%*       label 'hypo', and
  275%*       G1,..,Gn are the head instantiations  the clause has been applied with
  276%*       during the proof Prooftree.
  277%*									
  278%* description:	collects clauses and goals that have been used during 
  279%*              a successfull proof of a negative example
  280%*									
  281%* example:								
  282%*									
  283%* peculiarities:	none						
  284%*									
  285%* see also:								
  286%*									
  287%***********************************************************************
  288
  289fp_hyp([sys,_,_],L,L):- !.
  290fp_hyp([I,A,SG],L,L2):-
  291   fp_hyp_list(SG,L,L1),
  292   (   get_clause(I,_,_,_,hypo) ->
  293       insert_unique(I,A,L1,L2)
  294   ;   L2 = L1
  295   ).
  296
  297fp_hyp_list([],L,L).
  298fp_hyp_list([G|R],L,L2):-
  299   fp_hyp_list(R,L,L1),
  300   fp_hyp(G,L1,L2).
  301
  302
  303
  304%***********************************************************************
  305%*									
  306%* predicate:	fpo/1							
  307%*									
  308%* syntax:	fpo(-OR)						
  309%*									
  310%* args:	OR:							
  311%*									
  312%* description: as fp/1, but uses oracle
  313%*              Allows backtracking to an alternative set of possibly
  314%*              overgeneral clauses
  315%* 	        OR is a list [I:E,...], where I is the index of a possibly
  316%*   	        overgeneral clause and E is the set of wrong (head-)instantiations of
  317%*   	        clause I that should be excluded by specializing I.
  318%*   	        OR is a minimal selection of possibly overgeneral clauses such
  319%*   	        that by specialising them all negative examples become uncovered.
  320%*   	        On backtracking, the second selection is returned, and so on.
  321%*									
  322%* example:								
  323%*									
  324%* peculiarities:	none						
  325%*									
  326%* see also:								
  327%*									
  328%***********************************************************************
  329
  330fpo(OR):-
  331   (   evaluated(no) ->
  332       eval_examples
  333   ;   true
  334   ),
  335   bagof(TL,I^E^Trees^P^(get_example(I,E,'-'),prooftrees(I,success,Trees),
  336                         member(P,Trees),fpo(P,[],TL,_)), TList),
  337   collect_indices(TList,[],Indices),
  338   or_subsets(Indices,TList,OR_List),!,
  339   best(OR_List,OR).
  340fpo([]).
  341
  342
  343%***********************************************************************
  344%*									
  345%* predicate:	fpo/4							
  346%*									
  347%* syntax: fpo(+Prooftree,+L,-L,-M)
  348%*									
  349%* args: Prooftree is a prooftree for a succeeding negative example
  350%*       L = [...,ID:[G1,..,Gn],...] where ID is a clause index and
  351%*       G1,..,Gn are the head instantiations  the clause has been applied with
  352%*       during the proof Prooftree.
  353%*       M indicates whether Prooftree is successful in the oracle-simulation (ok)
  354%*       or not (not_ok)
  355%*									
  356%* description:	collects wrong clauses and goals that have been used during 
  357%*              a successfull proof of a negative example (uses oracle)
  358%*									
  359%* example:								
  360%*									
  361%* peculiarities:	none						
  362%*									
  363%* see also:								
  364%*									
  365%***********************************************************************
  366
  367fpo([sys,_,_],L,L,ok):- !.
  368fpo([I,A,SG],L,L1,X):-
  369   (   ask_for(A) ->
  370       fpo_list(SG,L,L1,X)
  371   ;   insert_unique(I,A,L,L1),
  372       X = not_ok
  373   ).
  374
  375fpo_list([],L,L,ok).
  376fpo_list([G|R],L,L2,X):-
  377   fpo(G,L,L1,Xg),
  378   (   Xg = ok ->
  379       fpo_list(R,L1,L2,X)
  380   ;   X = Xg
  381   ).
  382
  383
  384%***********************************************************************
  385%*									
  386%* predicate:	collect_indices/3							
  387%*									
  388%* syntax: collect_indices(+L,+Accu,-Accu)
  389%*									
  390%* args: L = [[I1:[G11,..,G1n],...,Im:[Gm1,...,Gmn]],...]
  391%*	 Accu = [I1,...,Ik]
  392%*								
  393%* description:	given the list of lists produced by fp/3, all indices of
  394%*     clauses that participated in successful proofs of negative examples
  395%*     are collected									
  396%*									
  397%* example:								
  398%*									
  399%* peculiarities:	none						
  400%*									
  401%* see also:								
  402%*									
  403%***********************************************************************
  404
  405collect_indices([],L,L).
  406collect_indices([X|R],L,L2):-
  407   c_indices(X,L,L1),
  408   collect_indices(R,L1,L2).
  409
  410c_indices([],L,L).
  411c_indices([I:_|R],L,L2):-
  412   c_indices(R,L,L1),
  413   (   member(I,L1) ->
  414       L2 = L1
  415   ;   L2 = [I|L1]
  416   ).
  417
  418
  419
  420%***********************************************************************
  421%*									
  422%* predicate:	or_subsets/3							
  423%*									
  424%* syntax: or_subsets(+Indices,+Tlist,-OR_List)
  425%*									
  426%* args: Indices ... list of indices of clauses that participated in successful
  427%*                   proofs of negative examples
  428%*       Tlist = [[I:[G1,..,Gn],..],..] list of lists produced by fp/3
  429%*       OR_List = list of lists [I:E,..] where I is the index of a possibly
  430%*       overgeneral clause and E is the set of wrong (head-)instantiations of
  431%*       clause I that should be excluded by specializing I. OR_List is sorted 
  432%*       ascendingly according to the length of the sublists
  433%*									
  434%* description: selects all possible combinations of possibly overgeneral clauses
  435%*     	such that by specialising them all negative examples become uncovered.
  436%*									
  437%* example:								
  438%*									
  439%* peculiarities:	none						
  440%*									
  441%* see also:								
  442%*									
  443%***********************************************************************
  444
  445or_subsets(IX,TL,ORL):-
  446   initialize_or_subsets(IX,IX,TL,TL1),
  447   or_all_subsets(TL1,[],TL2),
  448   sort_by_length(TL2,[],ORL).
  449
  450
  451%***********************************************************************
  452%*									
  453%* predicate:	initialize_or_subsets/4
  454%*									
  455%* syntax: initialize_or_subsets(+IX,+IX,+TL,-TL1)
  456%*									
  457%* args: IX list of clauseIDs 
  458%*       TL = [[I:CoveredI,J:CoveredJ,...],...] resulting from fp/3.
  459%*       each sublist in TL corresponds to a successful proof of a negative
  460%*       example
  461%* 									
  462%* description:	TL1 contains for each I in IX and entry [I:A]:IX1:TLI,
  463%*      where IX1 = IX - {I} and TLI results from TL by deleting every
  464%*      sublist [J:CJ,..,I:CI,...] that contains I:CI, and accumulating
  465%*      the head instances of I in A. 
  466%*      The set TLI contains all proofs of negative examples that are 
  467%*      still possible if clause I is excluded (e.g. specialised).
  468%*									
  469%* example:								
  470%*									
  471%* peculiarities:	none						
  472%*									
  473%* see also:								
  474%*									
  475%***********************************************************************
  476
  477initialize_or_subsets([],_,_,[]).
  478initialize_or_subsets([I|R],IX,TL,[[I:A]:IX1:TL1|R1]):-
  479   initialize_or_subsets(R,IX,TL,R1),
  480   remove(I,IX,IX1),
  481   remove_conjuncts(I,TL,TL1,[],A).
  482
  483
  484%***********************************************************************
  485%*									
  486%* predicate:	remove_conjuncts/5							
  487%*									
  488%* syntax: remove_conjuncts(+I,+TL,-TLI,+A,-A)
  489%*									
  490%* args: I .. clause Index, TL = [[I:CI,J:CJ,...],...],
  491%*       A = [G1,..,Gn] head instances of I
  492%*									
  493%* description:	removes from TL every sublist containing I:CI, and accumulates
  494%*		CI in A. Each sublist in TL corresponds to a successful proof of 
  495%*              a negative example. If clause I is assumed to be overgeneral and 
  496%*              therefore excluded, the proof fails and the remaining clauses that
  497%*              have been used need not be specialised. Therefore, the sublist is
  498%*              removed from TL.
  499%*									
  500%* example:								
  501%*									
  502%* peculiarities:	none						
  503%*									
  504%* see also:								
  505%*									
  506%***********************************************************************
  507
  508remove_conjuncts(_,[],[],A,A).
  509remove_conjuncts(I,[X|R],R1,A,A2):-
  510   member(I:E,X),!,
  511   append(E,A,A0),
  512   identical_make_unique(A0,A1),
  513   remove_conjuncts(I,R,R1,A1,A2).
  514remove_conjuncts(I,[X|R],[X|R1],A,A1):-
  515   remove_conjuncts(I,R,R1,A,A1).
  516
  517
  518%***********************************************************************
  519%*									
  520%* predicate:	or_all_subsets/3							
  521%*									
  522%* syntax: or_all_subsets(+TL1,+Accu,-Accu)
  523%*									
  524%* args: TL1 = [IXS:IXR:TLI,...] where IXS = [I:CI,...], IXR the indices not
  525%*       occurring in IXS, and TLI the remaining proofs of negative examples
  526%*       Accu = [IXS,...]
  527%*									
  528%* description:	tests every combination of clause indices whether all proofs
  529%*    of negative examples are excluded when the clauses are assumed to be 
  530%*    overgeneral. A combination IXS is successful, if all proofs are excluded,
  531%*    i.e. TLI = [].							
  532%*
  533%* example:								
  534%*									
  535%* peculiarities:	none						
  536%*									
  537%* see also:								
  538%*									
  539%***********************************************************************
  540
  541or_all_subsets([IXS:_:[]|R],L,[IXS|L1]):-
  542   or_all_subsets(R,L,L1).
  543or_all_subsets([IXS:RI:TL|R],L,L1):-
  544   or_asubsets(RI,RI,IXS,TL,R1),
  545   append(R,R1,R2),
  546   or_all_subsets(R2,L,L1).
  547or_all_subsets([],L,L).
  548
  549or_asubsets([],_,_,_,[]).
  550or_asubsets([I|R],RI,IXS,TL,[[I:A|IXS]:RI1:TL1|R1]):-
  551   remove(I,RI,RI1),
  552   remove_conjuncts(I,TL,TL1,[],A),
  553   or_asubsets(R,RI,IXS,TL,R1).
  554
  555
  556%***********************************************************************
  557%*									
  558%* predicate:	eval_pos_examples/1							
  559%*									
  560%* syntax:	 eval_pos_examples ( - List_of_Exs )	
  561%*									
  562%* args:								
  563%*									
  564%* description:	Evaluate (= try to prove) all positive examples, return a list of the
  565%*	ones which *cannot* be proved (empty list if successful).	
  566%*									
  567%* example:								
  568%*									
  569%* peculiarities: Output-argument looks like [exID1:Fact1, exID2:Fact2, ...].		
  570%*	!!! Procedure does not compute evaluation for clauses!!
  571%*									
  572%* see also:								
  573%*									
  574%***********************************************************************
  575
  576eval_pos_examples(Exlist) :-
  577	retractall(prooftrees(_,_,_)),
  578        findall(I:Fact, ( ex(I,Fact,'+'), solve_once(Fact,fail,_) ), Exlist).        
  579
  580
  581
  582%******************************************************************************
  583%* 
  584%* predicate: eval_examples/0 
  585%*
  586%* syntax:
  587%*
  588%* args:
  589%*
  590%* description: One should use this to compute the evaluation for kb clauses!
  591%*              - asserts for each example ID prooftrees(ID,Mark,Proofs), where
  592%*                Mark in {success,fail} and Proofs are the successful/failing
  593%*                proofs accordingly
  594%*              - determines the evaluation of each rule in the kb according to
  595%*                the current examples
  596%*
  597%* example:
  598%*
  599%* peculiarities:
  600%*
  601%* see also:
  602%*
  603%******************************************************************************
  604
  605eval_examples:- evaluated(yes),!.
  606
  607eval_examples :-
  608	retractall(prooftrees(_,_,_)),
  609	eval_examples1,!,
  610        change_evaluated(yes).
  611eval_examples1 :-
  612        ex(I,Fact,_),
  613        solve(Fact,M,Proofs),
  614        assert(prooftrees(I,M,Proofs)),
  615        fail.
  616eval_examples1 :-
  617        bagof(I:Proofs,prooftrees(I,success,Proofs),Plist),
  618        findall(known(J,H,B,Clist,L,_),(get_clause(J,H,B,Clist,L),delete_clause(J)),Klist),
  619        % don't use bagof here!
  620        compute_evaluation(Klist,Plist,Klist1),
  621        assertallz(Klist1),!.
  622eval_examples1.               % in case there are no examples
  623
  624clear_evaluation:- 
  625        retractall(prooftrees(_,_,_)),
  626        change_evaluated(no).
  627
  628change_evaluated(X):-
  629    retractall(evaluated(_)),
  630    assert(evaluated(X)). 
  631
  632
  633%***********************************************************************
  634%*									
  635%* predicate:correct_chk/0 								
  636%*									
  637%* syntax:								
  638%*									
  639%* args:								
  640%*									
  641%* description: fails when first *negative* example covered	
  642%*									
  643%* example:								
  644%*									
  645%* peculiarities: Does not compute evaluation for clauses!!
  646%*									
  647%* see also:								
  648%*									
  649%***********************************************************************
  650
  651correct_chk :-
  652   (   evaluated(no) ->
  653       (   (ex(_ID,Fact,'-'),solve_once(Fact,success,_)) ->
  654           fail
  655       ;   true
  656       )
  657   ;   (   (ex(ID,_Fact,'-'),prooftrees(ID,success,_)) ->
  658	   fail
  659       ;   true
  660       )
  661    ).
  662
  663%***********************************************************************
  664%*									
  665%* predicate: complete_chk/0 								
  666%*									
  667%* syntax:								
  668%*									
  669%* args:								
  670%*									
  671%* description:  fails if not all *positive* examples covered
  672%*									
  673%* example:								
  674%*									
  675%* peculiarities: Does not compute evaluation for clauses!!
  676%*									
  677%* see also:								
  678%*									
  679%* origin:  kb.pl (Irene/Markus)
  680%*									
  681%***********************************************************************
  682
  683complete_chk :-
  684   (   evaluated(no) ->
  685       (   (ex(_ID,Fact,'+'), solve_once(Fact,fail,_)) ->
  686           fail
  687       ;   true
  688       )
  689   ;   (   (ex(ID,_Fact,'+'),prooftrees(ID,fail,_)) ->
  690	   fail
  691       ;   true
  692       )
  693   ).
  694
  695
  696
  697%***********************************************************************
  698%*									
  699%* predicate:compute_evaluation/3
  700%*									
  701%* syntax: compute_evaluation(+Klist,+Plist,-Klist)
  702%*									
  703%* args: Klist ... list of kb-entries [known(I,H,B,Clist,Label,E),...]
  704%*		   where E is the evaluation of clause I
  705%*       Plist ... list of all successfule Proofs using Klist
  706%*                 = [I:Proofs,...] where prooftrees(I,success,Proofs) in kb
  707%*
  708%* description:	computes for each kb-entry in Klist the evaluation 
  709%*   E = evaluation(RA,NPos,Pos,NNeg,Neg,UNPos,UPos,UNNeg,UNeg), where
  710%*       RA ... #applications of the clause
  711%*       NPos ... #definitively positive examples covered by the clause
  712%*       Pos ... list of definitively positive examples covered by the clause
  713%*       NNeg ... #definitively negative  examples covered by the clause
  714%*       Neg ... list of definitively negative  examples covered by the clause
  715%*       UNPos ... #probably positive examples covered by the clause
  716%*       i.e. instantiations of the clause used in successful proofs of positive 
  717%*       examples
  718%*       UPos ... list of probably positive examples covered by the clause
  719%*       UNNeg ... #probably negative  examples covered by the clause
  720%*       i.e. instantiations of the clause used in successful proofs of negative 
  721%*       examples
  722%*       UNeg ... list of probably negative examples covered by the clause
  723%*									
  724%* example:								
  725%*									
  726%* peculiarities:	none				
  727%*									
  728%* see also:								
  729%*									
  730%***********************************************************************
  731
  732compute_evaluation([],_,[]).
  733compute_evaluation(
  734   [known(I,H,B,Clist,O,_)|R],Plist,
  735   [known(I,H,B,Clist,O,evaluation(RA,NPos,Pos,NNeg,Neg,UNPos,UPos,UNNeg,UNeg))|R1]
  736   ):-
  737   compute_evaluation(R,Plist,R1),
  738   compute_eval(Plist,I,RA,NPos,Pos,NNeg,Neg,UNPos,UPos,UNNeg,UNeg).
  739
  740
  741compute_eval([],_,0,0,[],0,[],0,[],0,[]).
  742compute_eval([I:Proofs|R],J,RA,NPos,Pos,NNeg,Neg,UNPos,UPos,UNNeg,UNeg):-
  743   compute_eval(R,J,RA0,NPos0,Pos0,NNeg0,Neg0,UNPos0,UPos0,UNNeg0,UNeg0),
  744   (   ex(I,_,'-') ->
  745       compute_eval(Proofs,t,I,J,RA0,RA,NNeg0,NNeg,Neg0,Neg,UNNeg0,UNNeg,UNeg0,UNeg),
  746       NPos = NPos0, Pos = Pos0, UNPos = UNPos0, UPos = UPos0
  747   ;   compute_eval(Proofs,t,I,J,RA0,RA,NPos0,NPos,Pos0,Pos,UNPos0,UNPos,UPos0,UPos),
  748       NNeg = NNeg0, Neg = Neg0, UNNeg = UNNeg0, UNeg = UNeg0
  749   ).
  750
  751compute_eval([],_,_,_,RA,RA,N,N,L,L,UN,UN,UL,UL).
  752compute_eval([[I,H,B]|R],T,K,J,RA,RA3,N,N3,L,L3,UN,UN3,UL,UL3):-
  753   compute_eval(R,T,K,J,RA,RA1,N,N1,L,L1,UN,UN1,UL,UL1),
  754   compute_eval(B,b,K,J,RA1,RA2,N1,N2,L1,L2,UN1,UN2,UL1,UL2),
  755   (   I == J ->
  756       RA3 is RA2 + 1,
  757       (   T == t ->
  758           (   member(_:H,L2) ->
  759               L3 = L2, N3 = N2, UN3 = UN2, UL3 = UL2
  760           ;   N3 is N2 + 1,
  761               L3 = [K:H|L2], 
  762               UN3 = UN2, UL3 = UL2
  763           )
  764       ;   (   member(_:H,UL2) ->
  765               L3 = L2, N3 = N2, UN3 = UN2, UL3 = UL2
  766           ;   UN3 is UN2 + 1,
  767               UL3 = [K:H|UL2],
  768               N3 = N2, L3 = L2
  769           )
  770       )
  771   ;   RA3 = RA2, L3 = L2, N3 = N2, UN3 = UN2, UL3 = UL2
  772   ).
  773
  774
  775%***********************************************************************
  776%*									
  777%* predicate:	covered_pos_examples/1
  778%*									
  779%* syntax: covered_examples(-CE)
  780%*									
  781%* args: CE ... list of IDs of covered positive examples
  782%*									
  783%* description:	returns IDs of all covered positive examples
  784%*									
  785%* example:								
  786%*									
  787%* peculiarities:	none				
  788%*									
  789%* see also:								
  790%*									
  791%***********************************************************************
  792
  793covered_pos_examples(Bag):- 
  794        (   evaluated(no) ->
  795            eval_examples
  796        ;   true
  797        ),
  798        findall( ID, (  get_example(ID,_,'+'), prooftrees(ID,success,_) ),
  799                 Bag),!.
  800
  801
  802%***********************************************************************
  803%*									
  804%* predicate:	covered_neg_examples/1
  805%*									
  806%* syntax: covered_neg_examples(-CE)
  807%*									
  808%* args: CE ... list of IDs of covered negative examples
  809%*									
  810%* description:	returns IDs of all covered negative examples
  811%*									
  812%* example:								
  813%*									
  814%* peculiarities:	none				
  815%*									
  816%* see also:								
  817%*									
  818%***********************************************************************
  819
  820covered_neg_examples(Bag):- 
  821        (   evaluated(no) ->
  822            eval_examples
  823        ;   true
  824        ),
  825        findall( ID, (  get_example(ID,_,'-'), prooftrees(ID,success,_) ),
  826                 Bag),!.
  827
  828
  829
  830%***********************************************************************
  831%*									
  832%* predicate:	all_covered_examples/1
  833%*									
  834%* syntax: all_covered_examples(-CE)
  835%*									
  836%* args: CE ... list of IDs of covered negative examples
  837%*									
  838%* description:	returns IDs of all covered  examples
  839%*									
  840%* example:								
  841%*									
  842%* peculiarities:	none				
  843%*									
  844%* see also:								
  845%*									
  846%***********************************************************************
  847
  848all_covered_examples(Bag):- 
  849        (   evaluated(no) ->
  850            eval_examples
  851        ;   true
  852        ),
  853        findall( ID, (  get_example(ID,_,_), prooftrees(ID,success,_) ),
  854                 Bag),!.
  855
  856
  857
  858%***********************************************************************
  859%*									
  860%* predicate:	complexity/2								
  861%*									
  862%* syntax: complexity(+ClauseID,-Size)
  863%*									
  864%* args: 								
  865%*									
  866%* description:	for kb references							
  867%*		complexity/2 calculates the size of a clause,		
  868%*		defined to be the number of constant and function       
  869%*		symbol occurences in the literals of the clause.	
  870%*									
  871%* example:								
  872%*									
  873%* peculiarities:	none				
  874%*									
  875%* see also:								
  876%*									
  877%***********************************************************************
  878
  879complexity( I, C):-
  880        integer(I),
  881        get_clause(I,_,_,Clause,_),
  882        compute_complexity(Clause,C),!.
  883
  884
  885
  886%***********************************************************************
  887%*									
  888%* predicate:	complexity/2								
  889%*									
  890%* syntax: complexity(+CL,-Size)
  891%*									
  892%* args:								
  893%*									
  894%* description: for clauses in list representation
  895%*
  896%* example:
  897%*
  898%* peculiarities:
  899%*
  900%* see also:
  901%*									
  902%***********************************************************************
  903
  904complexity( Clause, C):-
  905        Clause = [ _H:p | _ ],
  906        compute_complexity(Clause,C),!.
  907
  908
  909%***********************************************************************
  910%*									
  911%* predicate: complexity/2
  912%*									
  913%* syntax: complexity(List_of_ClauseIDs,-Size)
  914%*									
  915%* args:								
  916%*									
  917%* description:	for a list of kb references
  918%*
  919%* example:
  920%*
  921%* peculiarities:
  922%*
  923%* see also:
  924%*									
  925%***********************************************************************
  926 
  927complexity( [ID|List], C) :-
  928	integer(ID),
  929        findall(Com, ( member(I, [ID|List]),
  930	               get_clause(I,_,_,Clause,_),
  931		       compute_complexity(Clause,Com) ), Bag),
  932        sum( Bag,C),!.
  933	
  934
  935%***********************************************************************
  936%*									
  937%* predicate:	complexity/2								
  938%*									
  939%* syntax: complexity(+Term,-Size)
  940%*									
  941%* args:								
  942%*									
  943%* description:	for arbitrary prolog terms ( but not integers)
  944%*									
  945%* example:								
  946%*									
  947%* peculiarities:	none				
  948%*									
  949%* see also:								
  950%*									
  951%***********************************************************************
  952
  953complexity(Term,Complexity):-
  954        term_size(Term,Complexity),!.
  955
  956
  957
  958%***********************************************************************
  959%*									
  960%* predicate:	complexity/2							
  961%*									
  962%* syntax: complexity(+usr,-Size)
  963%*									
  964%* args:								
  965%*									
  966%* description:	for all clauses with label usr
  967%*									
  968%* example:								
  969%*									
  970%* peculiarities:	none				
  971%*									
  972%* see also:								
  973%*									
  974%***********************************************************************
  975
  976complexity( usr, C):- 
  977        findall( I, ( get_clause(_,_,_,Clause,usr), compute_complexity(Clause,I) ), Bag),
  978        sum( Bag,C),!.
  979
  980
  981%***********************************************************************
  982%*									
  983%* predicate: complexity/2								
  984%*									
  985%* syntax: complexity(+examples,-Size)
  986%*									
  987%* args:								
  988%*									
  989%* description: for all examples
  990%*									
  991%* example:								
  992%*									
  993%* peculiarities:	none				
  994%*									
  995%* see also:								
  996%*									
  997%***********************************************************************
  998
  999complexity( examples, C):- 
 1000        findall( I, ( get_example(_,Clause,_), compute_complexity(Clause,I) ), Bag),
 1001        sum( Bag,C),!.
 1002
 1003
 1004
 1005%***********************************************************************
 1006%*									
 1007%* predicate:	compute_complexity/2							
 1008%*									
 1009%* syntax: compute_complexity(+CL,-Size)
 1010%*									
 1011%* args: CL ... clause in list represenation
 1012%*									
 1013%* description:	complexity for a clause in list representation
 1014%*									
 1015%* example:								
 1016%*									
 1017%* peculiarities:	none				
 1018%*									
 1019%* see also:								
 1020%*									
 1021%***********************************************************************
 1022
 1023compute_complexity( [], 0).
 1024compute_complexity( [L:_|More],C):-
 1025        term_size( L, C1),
 1026        compute_complexity(More,C2),
 1027        C is C1 + C2.
 1028
 1029
 1030%***********************************************************************
 1031%*									
 1032%* predicate:	ivonTunterE/1						
 1033%*									
 1034%* syntax: ivonTunterE(-ITE)						
 1035%*									
 1036%* args: ITE... information content of T, given E
 1037%*       (only for funtion-free T and E!!)
 1038%*									
 1039%* description:	Given evidence E for T. Then if T|=E, then
 1040%*     I(T|E) = I(T) + I(E|T). If T = B & H, then T compresses
 1041%*     the examples E if I(T|E) =< I(B & E)
 1042%*     Precondition: B, T, E function-free!
 1043%*     
 1044%*     How to compute I(T) and I(E|T) (for function-free T,E):
 1045%*     -  I(E|T) = log2( (|M+(T)|  |E+|) ) + log2( (|M-(T)|  |E-(T)|) )
 1046%*     -  P(T) .. #Pred. Symbols in T
 1047%*        C(T) .. #Constants in T
 1048%*        V(T) .. max number of vars of any clause in T
 1049%*        a .. max arity of any pred. symbol in T
 1050%*        l .. max cardinality of the body of any clause in T
 1051%*        |T| .. #clauses in T
 1052%*        
 1053%*        |A(T)| =< P(T)*(C(T) + V(T))^a
 1054%*        |CL(T)| =< |A(T)| * (|A(T)|  l)
 1055%*        I(T) = log2( (|CL(T)|  |T|) )
 1056%*        where (a  b) == (a) = n!/(k!*(n-k)!)
 1057%*                        (b)
 1058%*									
 1059%* example:								
 1060%*									
 1061%* peculiarities:	none				
 1062%*									
 1063%* see also: L. DeRaedth, S. Muggleton: ILP: Theory and Methods
 1064%*	     submitted to Journal of LP
 1065%*
 1066%***********************************************************************
 1067
 1068ivonTunterE(ITE):-
 1069   findall(P/A, (get_clause(_,_,_,CL,_),
 1070                 member(F:_,CL),functor(F,P,A)),Predlist0),
 1071   make_unique(Predlist0,Predlist),
 1072   max_arity(Predlist,A),
 1073   length(Predlist,PT),
 1074   findall(C,(get_clause(_,H,B,_,_),
 1075              sub_term(C,(H,B)),
 1076              atomic(C),C \== true),Clist0),
 1077   make_unique(Clist0,Clist),
 1078   length(Clist,CT),
 1079   findall(V/L2,(get_clause(_,_,_,CL,_),
 1080                 length(CL,L1), L2 is L1 - 1,
 1081                 vars(CL,VL),length(VL,V)),LList),
 1082   maxvars(LList,VT),
 1083   max_arity(LList,L),
 1084   findall(ID,get_clause(ID,_,_,_,_),IDL),
 1085   length(IDL,BT),
 1086   ivonT(PT,CT,VT,A,L,BT,IT),
 1087   ivonEunterT(Predlist,CT,IET),
 1088   ITE is IT + IET.
 1089
 1090
 1091
 1092ivonT(PT0,CT0,VT0,A0,L0,BT0,IT):-
 1093   PT is float(PT0), 
 1094   CT is float(CT0), 
 1095   VT is float(VT0), 
 1096   A is float(A0),
 1097   L is float(L0),
 1098   BT is float(BT0),
 1099   X1 is CT + VT,
 1100   pow(X1,A,X2),
 1101   AT is PT * X2,
 1102   nueberk(AT,L,X3),
 1103   CLT is AT * X3,
 1104   log2nueberk(CLT,BT,IT).
 1105
 1106ivonEunterT(Predlist,CT,IET):-
 1107   all_atoms(Predlist,CT,HT0),
 1108   mTplus(CT,MTP0),
 1109   HT is float(HT0),
 1110   MTP is float(MTP0),
 1111   MTM is HT - MTP,
 1112   findall(P,get_example(_,P,+),PL),
 1113   length(PL,PLN0),
 1114   findall(N,get_example(_,N,-),NL),
 1115   length(NL,NLN0),
 1116   PLN is float(PLN0),
 1117   NLN is float(NLN0),
 1118   log2nueberk(MTP,PLN,LX),
 1119   log2nueberk(MTM,NLN,LY),
 1120   IET is LX + LY.
 1121
 1122%***********************************************************************
 1123%*									
 1124%* predicate:	ivonBundE/1						
 1125%*									
 1126%* syntax: ivonBundE(-IBE)						
 1127%*									
 1128%* args: ITE... information content of B & E
 1129%*       (only for funtion-free B and E!!)
 1130%*									
 1131%* description:	computes information content of B & E.
 1132%*     If T = B & H, then T compresses
 1133%*     the examples E if I(T|E) =< I(B & E)
 1134%*     Precondition: B, T, E function-free!
 1135%*									
 1136%* example:								
 1137%*									
 1138%* peculiarities:	none				
 1139%*									
 1140%* see also: L. DeRaedth, S. Muggleton: ILP: Theory and Methods
 1141%*	     submitted to Journal of LP
 1142%*
 1143%***********************************************************************
 1144
 1145ivonBundE(IBE):-
 1146   findall(P/A, (get_clause(_,_,_,CL,_),
 1147                 member(F:_,CL),functor(F,P,A)),Predlist00),
 1148   findall(P1/A1, (get_example(_,F,_),
 1149                 functor(F,P1,A1)),Predlist01),
 1150   append(Predlist00,Predlist01,Predlist0),
 1151   make_unique(Predlist0,Predlist),
 1152   max_arity(Predlist,A),
 1153   length(Predlist,PT),
 1154   findall(C,(get_clause(_,H,B,_,_),
 1155              sub_term(C,(H,B)),
 1156              atomic(C),C \== true),Clist00),
 1157   findall(C1,(get_example(_,H1,_),
 1158               sub_term(C1,H1),
 1159               atomic(C1),C1 \== true),Clist01),
 1160   append(Clist00,Clist01,Clist0),
 1161   make_unique(Clist0,Clist),
 1162   length(Clist,CT),
 1163   findall(V/L2,(get_clause(_,_,_,CL,_),
 1164                 length(CL,L1), L2 is L1 - 1,
 1165                 vars(CL,VL),length(VL,V)),LList),
 1166   maxvars(LList,VT),
 1167   max_arity(LList,L),
 1168   findall(ID,get_clause(ID,_,_,_,_),IDL00),
 1169   findall(ID1,get_example(ID1,_,_),IDL01),
 1170   append(IDL00,IDL01,IDL),
 1171   length(IDL,BT),
 1172   ivonT(PT,CT,VT,A,L,BT,IBE).
 1173
 1174
 1175%***********************************************************************
 1176%*									
 1177%* predicate:	all_atoms/3							
 1178%*									
 1179%* syntax: all_atoms(+Predlist,+No_constants,-No_atoms)
 1180%*									
 1181%* args: Predlist = [p1/arity1,...,pn/arityn] list of pred. symbols and 
 1182%*                   their arities
 1183%*       No_constants.... number c of constants in the current theory
 1184%*       No_atoms = number of atoms that can be built from the preds
 1185%*                  in predlist and the c constants
 1186%*                = c^arity1 + .... + c^arityn
 1187%*									
 1188%* description:	
 1189%*									
 1190%* example:								
 1191%*									
 1192%* peculiarities:	none				
 1193%*									
 1194%* see also:								
 1195%*									
 1196%***********************************************************************
 1197
 1198all_atoms([],_,0).
 1199all_atoms([_/A0|R],CT0,HT):-
 1200   all_atoms(R,CT0,HT0),
 1201   CT is float(CT0),
 1202   A is float(A0),
 1203   pow(CT,A,X),
 1204   HT is HT0 + X.
 1205
 1206
 1207%***********************************************************************
 1208%*									
 1209%* predicate:	max_arity/2, maxvars/2, maxi/3
 1210%*									
 1211%* syntax: max_arity(+Plist,-A), maxvars(+Vlist,-V), maxi(+X,+Y,-Z)
 1212%*									
 1213%* args: Plist = [_/n1,...,_/nn] for numbers ni, A is the max of the ni
 1214%*	 Vlist = [_/n1,...,_/nn] for numbers ni, V is the max of the ni
 1215%*       Z is the max of X and Y
 1216%*							
 1217%* description:	
 1218%*									
 1219%* example:								
 1220%*									
 1221%* peculiarities:	none				
 1222%*									
 1223%* see also:								
 1224%*									
 1225%***********************************************************************
 1226
 1227max_arity([_/A],A):- !.   
 1228max_arity([_/A|R],C):-
 1229   max_arity(R,B),
 1230   maxi(A,B,C).
 1231
 1232maxvars([A/_],A):- !.
 1233maxvars([A/_|R],C):-
 1234   maxvars(R,B),
 1235   maxi(A,B,C).
 1236
 1237maxi(A,B,C):-
 1238   (   A >= B ->
 1239       C = A
 1240   ;   C = B
 1241   ).
 1242
 1243%***********************************************************************
 1244%*									
 1245%* predicate:	herbrand_base_ff/1							
 1246%*									
 1247%* syntax: herbrand_base_ff(-M)
 1248%*									
 1249%* args: M .. reduced list of atoms entailed by the current 
 1250%*       function-free theory
 1251%*									
 1252%* description:	
 1253%*									
 1254%* example:								
 1255%*									
 1256%* peculiarities:	none				
 1257%*									
 1258%* see also:								
 1259%*									
 1260%***********************************************************************
 1261
 1262herbrand_base_ff(M):-
 1263   findall(H, get_clause(_,H,true,_,_),M00),
 1264   reduce_hb(M00,M0),
 1265   findall(ID,(get_clause(ID,_,B,_,_),B \== true),IDlist),
 1266   herbrand_base_ff(IDlist,M0,M).
 1267
 1268herbrand_base_ff(IDlist,M,M2):-
 1269   herbrand_base_ff(IDlist,M,M,M1,Mark),
 1270   (   Mark == changed ->
 1271       herbrand_base_ff(IDlist,M1,M2)
 1272   ;   M2 = M1
 1273   ).
 1274
 1275herbrand_base_ff([],_,M,M,not_changed).
 1276herbrand_base_ff([ID|R],M,M1,M4,Mark):-
 1277   herbrand_base_ff(R,M,M1,M2,Mark0),
 1278   get_clause(ID,H,B,_,_),
 1279   findall(H1,match_body(H,B,M,H1),HL),
 1280   append(HL,M2,M3),
 1281   make_unique(M3,M31),
 1282   reduce_hb(M31,M4),
 1283   (   remove_variant(M2,M4,[]) ->
 1284       Mark = Mark0
 1285   ;   Mark = changed
 1286   ).
 1287
 1288match_body(H,B,M,H1):-
 1289   copy_term((H,B),(H1,B1)),
 1290   copy_term(M,M1),
 1291   match_body(B1,M1).
 1292
 1293match_body((A,B),M):- !,
 1294   member(A,M),
 1295   match_body(B,M).
 1296match_body(A,M):-
 1297   member(A,M).
 1298
 1299reduce_hb(L,L1):-
 1300   reduce_hb(L,L,L1).
 1301reduce_hb([],_,[]).
 1302reduce_hb([H|R],L,R2):-
 1303   reduce_hb(R,L,R1),
 1304   (   \+(sub_contained_in(H,L)) ->
 1305       R2 = [H|R1]
 1306   ;   R2 = R1
 1307   ).
 1308
 1309sub_contained_in(H,[H1|R]):-
 1310   (   (H1 \== H, subsumes_chk(H1,H)) ->
 1311       true
 1312   ;   sub_contained_in(H,R)
 1313   ).
 1314
 1315
 1316%***********************************************************************
 1317%*									
 1318%* predicate:	mTplus/2							
 1319%*									
 1320%* syntax: mTplus(+No_constants,-MT)
 1321%*									
 1322%* args: No_constants... number c of constants in T
 1323%*       MT ... size of M+(T) for theory T
 1324%*									
 1325%* description:	determines first the reduced Herbrand base of T, i.e.
 1326%*       a list [A1,...,An] where Ai are atoms that might contain variables.
 1327%*       The size of M+(T) is then
 1328%*        |vars(A1)|^c + .... + |vars(An)|^c
 1329%*									
 1330%* example:								
 1331%*									
 1332%* peculiarities:	none				
 1333%*									
 1334%* see also:								
 1335%*									
 1336%***********************************************************************
 1337
 1338mTplus(CT,MT):-
 1339   herbrand_base_ff(M),
 1340   hb_plus(M,CT,MT).
 1341
 1342hb_plus([],_,0).
 1343hb_plus([T|R],CT0,MT):-
 1344   hb_plus(R,CT0,MT1),
 1345   vars(T,V),
 1346   length(V,VN0),
 1347   CT is float(CT0),
 1348   VN is float(VN0),
 1349   pow(CT,VN,X),
 1350   MT is MT1 + X.
 1351
 1352
 1353%***********************************************************************
 1354%*									
 1355%* predicate:	code_length/2							
 1356%*									
 1357%* syntax: code_length(+Term,-CL)
 1358%*									
 1359%* args: CL .. code length of Term
 1360%*									
 1361%* description:	code length of a term a la R. Wirth/S. Muggleton: 
 1362%*              let sym(Term) be all symbols in Term, and N the number of
 1363%*              all symbol occurrences in Term. Let ps be the relative 
 1364%*              frequency of symbol s in Term. Then
 1365%*              code_length(Term)= N * sum_{s in sym(Term)} -ps log2ps
 1366%*									
 1367%* example:								
 1368%*									
 1369%* peculiarities:	none				
 1370%*									
 1371%* see also:								
 1372%*									
 1373%***********************************************************************
 1374
 1375code_length(S,L):-
 1376   skolemize(S,_,S0),
 1377   symbol_frequencies(S0,[],SymS),
 1378   relative_frequencies(SymS,0,N,SymS1),
 1379   code_length1(SymS1,L0),
 1380   L is N * L0.
 1381
 1382code_length1([],0).
 1383code_length1([F|R],L):-
 1384   code_length1(R,L0),
 1385   log2(F,LF),
 1386   L1 is F * (-LF),
 1387   L is L0 + L1.
 1388
 1389relative_frequencies([],N,N,[]).
 1390relative_frequencies([_/_/M|R],N0,N,[RM|R1]):-
 1391   N1 is N0 + M,
 1392   relative_frequencies(R,N1,N,R1),
 1393   RM is M/N.
 1394
 1395symbol_frequencies(X,L,L1):-
 1396   atomic(X),!,
 1397   update_frequency_list(L,X,0,L1).
 1398symbol_frequencies(X,L,L1):-
 1399   functor(X,F,N),
 1400   update_frequency_list(L,F,N,L0),
 1401   symbol_frequencies(N,X,L0,L1).
 1402
 1403symbol_frequencies(0,_,L,L):- !.
 1404symbol_frequencies(N,X,L,L2):-
 1405   N1 is N - 1,
 1406   symbol_frequencies(N1,X,L,L1),
 1407   arg(N,X,Xn),
 1408   symbol_frequencies(Xn,L1,L2).
 1409
 1410update_frequency_list([],F,N,[F/N/1]).
 1411update_frequency_list([F/N/M|R],F,N,[F/N/M1|R]):-
 1412   !, M1 is M + 1.
 1413update_frequency_list([X|R],F,N,[X|R1]):-
 1414   update_frequency_list(R,F,N,R1).
 1415
 1416
 1417
 1418%***********************************************************************
 1419%*									
 1420%* predicate:	encoding_length_examples/1, encoding_length_clause/2
 1421%*									
 1422%* syntax: encoding_length_examples(-EE)
 1423%*         encoding_length_clause(+CL,-EC)
 1424%*									
 1425%* args: EE, EC.. floats
 1426%*       CL... clause in list representation
 1427%*									
 1428%* description:	encoding length a la Quinlan:
 1429%*    for examples: PN.. no of pos ex., NN.. no. of neg ex, U = PN + NN
 1430%*             EE = log2(U) + log2((U  PN))
 1431%*    for clauses: N.. length of Clause, Preds.. no of preds,
 1432%*                 A .. no of poss. args
 1433%*             EC = (sum_{i=1}^{N} bits for literal i)/log2(N!)
 1434%*             bits for literali = 1 + log2(Preds) + log2(A)
 1435%*									
 1436%* example:								
 1437%*									
 1438%* peculiarities:	none				
 1439%*									
 1440%* see also:								
 1441%*									
 1442%***********************************************************************
 1443
 1444encoding_length_examples(X):-
 1445   mysetof(ID,F^(get_example(ID,F,+)),PL),
 1446   length(PL,PN),
 1447   mysetof(ID1,F1^(get_example(ID1,F1,-)),NL),
 1448   length(NL,NN),
 1449   U is PN + NN,
 1450   log2(U,LU),
 1451   U1 is float(U),
 1452   PN1 is float(PN),
 1453   log2nueberk(U1,PN1,Y),
 1454   X is LU + Y.
 1455
 1456encoding_length_clause(CL,EL):-
 1457   length(CL,N),
 1458   N1 is float(N),
 1459   sum_of_logs(1.0,N1,LNF),
 1460   encoding_length_lits(CL,Lits0),
 1461   get_predlist(PList),
 1462   length(PList,Preds),
 1463   log2(Preds,LPreds),
 1464   Lits is Lits0 + N + (N * LPreds),
 1465   EL is Lits/LNF.
 1466
 1467encoding_length_lits([H:p|R],M):-
 1468   functor(H,_,N),
 1469   H =.. [_|Args],
 1470   log2(N,LN),
 1471   encoding_length_lits(R,Args,M1),
 1472   M is M1 + LN.
 1473
 1474encoding_length_lits([L:_|R],Args,M):-
 1475   length(Args,LA),
 1476   log2(LA,M0),
 1477   L =.. [_|Args1],
 1478   append(Args1,Args,Args2),
 1479   identical_make_unique(Args2,Args3),
 1480   encoding_length_lits(R,Args3,M1),
 1481   M is M0 + M1.
 1482encoding_length_lits([],_,0)