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)