1% MODULE filter EXPORTS 2:- module( filter, 3 [ is_flat/1, 4 is_unflat/1, 5 connected_vars/4, 6 truncate_unconnected/2, 7 truncate_unconnected/1, 8 is_weakly_generative/1, 9 is_strongly_generative/1, 10 is_connected/1, 11 truncate/3, 12 truncate_r/2, 13 truncate_r/1, 14 truncate_flat_r/1, 15 truncate_unconnecting/1, 16 truncate_unconnecting/2, 17 truncate_strongly_generative/1, 18 truncate_strongly_generative/2, 19 truncate_neg_based/1, 20 truncate_flat_neg_based/1, 21 truncate_facts/1, 22 truncate_j/2, 23 noduplicate_atoms/1, 24 noduplicate_atom/2, 25 select_var_sharing_lits/2, 26 already_in/3 27 ]). 28 29 30%IMPORTS 31:- use_module_if_exists(library(not), 32 [ (once)/1 ]). 33:- use_module_if_exists(library(sets), 34 [union/2,union/3,intersection/3,list_to_set/2,subtract/3, 35 subset/2,select/3]). 36:- use_module_if_exists(library(strings), 37 [string_append/3,substring/4,midstring/6]). 38:- use_module_if_exists(library(basics),[member/2]). 39:- use_module_if_exists(library(lists),[subseq/3,rev/2,last/2,nth1/4]). 40:- use_module_if_exists(library(occurs),[sub_term/2]). 41:- use_module_if_exists(library(arg),[genarg/3]). 42:- use_module_if_exists(library(subsumes), 43 [subsumes_chk/2]). 44:- use_module(home(div_utils), 45 [shares_var/2]). 46:- use_module(home(var_utils), 47 [vars/2,contains_vars/2,skolemize/3,deskolemize/3,skolems/2, 48 flagged_contains_vars/3]). 49:- use_module(home(kb), 50 [get_clause/5,store_clause/4,delete_clause/1,get_fact/4, 51 unflatten_kb/0]). 52:- use_module(home(flatten), 53 [flatten_clause/2,unflatten_clause/2]). 54:- use_module(home(evaluation), 55 [correct_chk/0]). 56 57 58% METAPREDICATES 59% none 60 61:- dynamic functional_mode/1. 62 63%*********************************************************************** 64%* 65%* module: filter.pl 66%* 67%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend date:12/92 68%* 69%* changed: 70%* 71%* description: various filters useful for td- and bu-induction 72%* 73%* see also: 74%* 75%*********************************************************************** 76 77 78%*********************************************************************** 79%* predicate: already_in/3 (optional) 80%* 81%* syntax: already_in(+N,+P,+Y) 82%* 83%* args: N: arity of a literal P 84%* P: literal 85%* Y: term 86%* 87%* description: succeeds if Y is(==) already an argument of P 88%* 89%* example: 90%* 91%* peculiarities: none 92%* 93%* see also: 94%* 95%*********************************************************************** 96 97already_in(0,_,_):- !,fail. 98already_in(N,P,Y):- 99 arg(N,P,Pn), 100 ( Pn == Y -> 101 true 102 ; N1 is N - 1, 103 already_in(N1,P,Y) 104 ). 105 106 107%*********************************************************************** 108%* 109%* predicate: select_var_sharing_lits/2 110%* 111%* syntax: select_var_sharing_lits(+List_of_Clauses,-List_of_Clauses) 112%* 113%* args: 114%* 115%* description: removes all clauses from List_of_Clauses the last 116%* literal of which does not share a variable with 117%* the rest of the clause -> to be used during td-refinement 118%* (not to add unconnected body literals) 119%* 120%* example: 121%* 122%* peculiarities: none 123%* 124%* see also: 125%* 126%*********************************************************************** 127 128select_var_sharing_lits([],[]). 129select_var_sharing_lits([C|R],R2):- 130 select_var_sharing_lits(R,R1), 131 ( var_sharing_lit(C,[]) -> 132 R2 = [C|R1] 133 ; R2 = R1 134 ). 135 136 137%*********************************************************************** 138%* 139%* predicate: var_sharing_lit/2 140%* 141%* syntax: var_sharing_lit(+Clause,+CAccu) 142%* 143%* args: CAccu contains all literals of clause except the last one 144%* 145%* description: succeeds if the last literal of clause shares (at least) 146%* a variable with the rest of the clause. 147%* 148%* example: 149%* 150%* peculiarities: none 151%* 152%* see also: 153%* 154%*********************************************************************** 155 156var_sharing_lit((H:-B),[]):- 157 !,var_sharing_lit(B,[H]). 158var_sharing_lit((A,B),C):- 159 !, var_sharing_lit(B,[A|C]). 160var_sharing_lit(A,C):- 161 shares_var(A,C),!. 162 163 164%*********************************************************************** 165%* predicate: noduplicate_atom/2 166%* 167%* syntax: noduplicate_atom(+P,+B) 168%* 169%* args: P: literal 170%* B: clause body 171%* 172%* description: tests if P already occurs(==) in B 173%* 174%* example: 175%* 176%* peculiarities: none 177%* 178%* see also: 179%* 180%*********************************************************************** 181 182noduplicate_atom(P,(A,B)):- 183 !, P \== A, 184 noduplicate_atom(P,B). 185noduplicate_atom(P,A):- 186 P \== A. 187 188 189%*********************************************************************** 190%* predicate: noduplicate_atoms/1 191%* 192%* syntax: noduplicate_atoms(+Clause) 193%* 194%* args: 195%* 196%* description: tests whether Clause contains duplicate literals 197%* 198%* example: 199%* 200%* peculiarities: none 201%* 202%* see also: 203%* 204%*********************************************************************** 205 206noduplicate_atoms((A:-B)):- 207 !, noduplicate_atom(A,B), 208 noduplicate_atoms(B). 209noduplicate_atoms((A,B)):- 210 !,noduplicate_atom(A,B), 211 noduplicate_atoms(B). 212noduplicate_atoms(_). 213 214 215%*********************************************************************** 216%* 217%* predicate: connected_vars/4 218%* 219%* syntax: connected_vars(+ClauseIn,-ClauseOut,-Connected,-Unconnected) 220%* 221%* args: ClauseIn,ClauseOut: clauses in list notation 222%* Connected,Unconnected: list of variables 223%* 224%* description: returns connected & unconnected vars 225%* A variable is connected ( to the head literal ) iff 226%* - it appears in the head, or 227%* - it appears in a literal with a connected variable 228%* A literal is connected iff it's vars are. 229%* 230%* example: 231%* 232%* peculiarities: we make a copy of the input clause 233%* 234%* see also: 235%* 236%*********************************************************************** 237 238connected_vars(ClauseIn,ClauseOut,Connected,Unconnected):- 239 copy_term(ClauseIn,ClauseIn1), 240 skolemize( ClauseIn1, S, Clause1), 241 connected_skolems( Clause1, C, U), 242 deskolemize( (Clause1:C:U) , S, (ClauseOut:Connected:Unconnected) ). 243 244connected_skolems([Head:p|Body],Connected,Unconnected):- 245 skolems(Head, Con), 246 Uncon = [], 247 find_connected_skolems_in_body(Body, Con, Connected, Uncon, Unconnected_tupels), 248 union(Unconnected_tupels,Unconnected). 249 250 251%*********************************************************************** 252%* 253%* predicate: find_connected_skolems_in_body/5 254%* 255%* syntax: find_connected_skolems_in_body(+Body_list,+Connected,-Connected, 256%* +Unconnected_tuples,-Unconnected_tuples) 257%* 258%* args: Body_list .. clause body in list notation, 259%* Connected .. connected skolem atoms 260%* Unconnected_tuples .. lists of lists of unconnected skolem atoms 261%* 262%* description: separates connected and unconnected skolem atoms 263%* (each corresponds to a variable) within the body 264%* 265%* example: 266%* 267%* peculiarities: 268%* 269%* see also: 270%* 271%*********************************************************************** 272 273find_connected_skolems_in_body( [L:_|Rest], C1,C2,U1,U2):- 274 skolems(L,V1), 275 ( intersection(C1,V1,I), I \== [] 276 -> union(C1,V1,C4) , connect(V1,C4,C3,U1,U3) 277 ; 278 C3 = C1, U3 = [ V1 | U1 ] 279 ), 280 find_connected_skolems_in_body(Rest, C3,C2,U3,U2). 281find_connected_skolems_in_body( [],C,C,U,U). 282 283connect(_V,C,C,[],[]). 284connect(Vars,C1,C2,[Tupel|More],U2):- 285 member(Var,Vars), 286 member(Var,Tupel),!, 287 union(C1,Tupel,C3), 288 connect(Vars,C3,C2,More,U2). 289connect(Vars,C1,C2,[Tupel|More],[Tupel|U2]):- 290 connect(Vars,C1,C2,More,U2). 291 292 293%*********************************************************************** 294%* 295%* predicate: is_weakly_generative/1 296%* 297%* syntax: is_weakly_generative(+Clause) 298%* 299%* args: Clause: clause in list notation 300%* 301%* description: a clause is weakly generative if all vars of its head 302%* appear also in another literal 303%* 304%* example: 305%* 306%* peculiarities: 307%* 308%* see also: Muggleton,90 309%* 310%*********************************************************************** 311 312is_weakly_generative([H:p|B]):- 313 vars(H,Vars), 314 contains_vars(Vars,B). 315 316 317%*********************************************************************** 318%* 319%* predicate: is_stronly_generative/1 320%* 321%* syntax: is_strongly_generative(+Clause) 322%* 323%* args: Clause: clausew in list notation 324%* 325%* description: a clause is strongly generative if every variable 326%* appears in at least 2 literals 327%* 328%* example: 329%* 330%* peculiarities: 331%* 332%* see also: Muggleton,90 333%* 334%*********************************************************************** 335 336is_strongly_generative(Clause):- 337 findall(Flag, 338 ( subseq( Clause, [L], Rest), 339 vars(L,Vars), 340 flagged_contains_vars(Vars,Rest,Flag) ), 341 Flags), 342 \+ member( false, Flags), !. 343 344 345%*********************************************************************** 346%* 347%* predicate: is_connected/1 348%* 349%* syntax: is_connected(+Clause) 350%* 351%* args: Clause: clause in list notation 352%* 353%* description: a clause is connected if every variable is connected 354%* to the head. 355%* 356%* example: 357%* 358%* peculiarities: 359%* 360%* see also: Rouveirol,91 361%* 362%*********************************************************************** 363 364is_connected(Clause):- connected_vars(Clause,_,_,[]). 365 366 367%*********************************************************************** 368%* 369%* predicate: is_flat/1, is_unflat/1 370%* 371%* syntax: is_flat(+Clause), is_unflat(Clause) 372%* 373%* args: clause in list notation [ head:p, b1:n, .. ] 374%* 375%* description: succeeds/fails if Clause contains no function symbols 376%* 377%* example: 378%* 379%* peculiarities: if input is not a clause in list form, is_flat/1 380%* always succeeds. 381%* 382%* see also: 383%* 384%*********************************************************************** 385 386is_flat(Clause):- nonvar(Clause), \+ is_unflat(Clause). 387 388is_unflat([L:_|_Rest]):-is_unflat_literal(L). 389is_unflat([_|Rest]):- is_unflat(Rest). 390 391is_unflat_literal(L):- 392 sub_term(Subterm,L), 393 Subterm \== L, 394 nonvar(Subterm),!. 395 396 397%*********************************************************************** 398%* 399%* predicate: truncate/3 400%* 401%* syntax: truncate(+Strategy,+ClauseIn,-ClauseOut) 402%* 403%* args: Strategy: one of { r, unconnected, unconnecting, 404%* strongly_generative} 405%* ClauseIn,ClauseOut: integers (kb references) 406%* 407%* description: performs truncation operator on ClauseIn 408%* using Strategy. 409%* 410%* The list of possible strategies is to be completed. 411%* 412%* example: 413%* 414%* peculiarities: 415%* 416%* see also: 417%* 418%*********************************************************************** 419 420truncate( Strategy, In, Out):- 421 get_clause( In,_,_,C1,_), 422 do_truncate( Strategy, C1, C2), 423 store_clause( _,C2,trunc,Out). 424 425do_truncate( r, C1, C2):- truncate_r(C1,C2). 426do_truncate( unconnected,C1,C2):- truncate_unconnected(C1,C2). 427do_truncate( strongly_generative, C1,C2):- truncate_strongly_generative(C1,C2). 428do_truncate( unconnecting,C1,C2):- truncate_unconnecting(C1,C2). 429 430 431%*********************************************************************** 432%* 433%* predicate: truncate_r/2/1 434%* 435%* syntax: truncate_r(ClauseIn,ClauseOut) 436%* truncate_r(ID) 437%* 438%* args: clauses in list notation 439%* 440%* description: drop all literals with label ':r', 441%* i.e. drop all literals that were used in saturation. 442%* 443%* example: 444%* 445%* peculiarities: 446%* 447%* see also: 448%* 449%*********************************************************************** 450 451truncate_r(ID):- 452 get_clause(ID,_,_,ClauseIn,_), 453 truncate_r(ClauseIn,ClauseOut), 454 delete_clause(ID), 455 store_clause( _,ClauseOut, trc, ID). 456 457truncate_r(ClauseIn,ClauseOut):- 458 copy_term(ClauseIn,C), 459 do_truncate_r(C,ClauseOut). 460 461do_truncate_r([],[]). 462do_truncate_r([_L:r|Rest],Rest1):-!, do_truncate_r(Rest,Rest1). 463do_truncate_r([L:S|Rest],[L:S|Rest1]):-!, do_truncate_r(Rest,Rest1). 464 465 466%*********************************************************************** 467%* 468%* predicate: truncate_flat_r/2/1 469%* 470%* syntax: truncate_flat_r(ClauseIn,ClauseOut) 471%* truncate_flat_r(ID) 472%* 473%* args: clauses in list notation 474%* 475%* description: drop all true literals with label ':r', 476%* i.e. drop all literals that were used in saturation, 477%* but no literals with type information ( suffix '_p'). 478%* 479%* example: 480%* 481%* peculiarities: 482%* 483%* see also: 484%* 485%*********************************************************************** 486 487truncate_flat_r(ID):- 488 get_clause(ID,_,_,ClauseIn,_), 489 truncate_flat_r(ClauseIn,ClauseOut), 490 delete_clause(ID), 491 store_clause( _,ClauseOut, trc, ID). 492 493truncate_flat_r(ClauseIn,ClauseOut):- 494 copy_term(ClauseIn,C), 495 do_truncate_flat_r(C,ClauseOut). 496 497do_truncate_flat_r([],[]). 498do_truncate_flat_r([L:r|Rest],Rest1):- 499 functor(L,F,N), 500 functor(LC,F,N), % L is bg predicate 501 get_clause(_,LC,_,_,usr), 502 !, do_truncate_flat_r(Rest,Rest1). 503do_truncate_flat_r([L:S|Rest],[L:S|Rest1]):-!, do_truncate_flat_r(Rest,Rest1). 504 505 506%*********************************************************************** 507%* 508%* predicate: truncate_unconnected/2 509%* 510%* syntax: truncate_unconnected(+ClauseIn, -ClauseOut) 511%* 512%* args: ClauseIn,ClauseOut: clauses in list notation 513%* 514%* description: truncate unconnected body literals (see above) 515%* 516%* example: let ClauseIn = [ min(A,[A|B]):p, min(C,B):n, ge(E,F):n ] 517%* then ClauseOut = [ min(A,[A|B]):p, min(C,B):n ] 518%* let ClauseIn = [p(X):n,q(X,V1):n,r(V1,V2):n,q(V3):n,s(V3,V1):n], 519%* then ClauseOut = [p(X):n,q(X,V1):n,r(V1,V2):n,q(V3):n,s(V3,V1):n] 520%* (in contrast to truncate_unconnecting) 521%* 522%* peculiarities: 523%* 524%* see also: 525%* 526%*********************************************************************** 527 528truncate_unconnected(ID):- 529 get_clause(ID, _,_,C,_), 530 truncate_unconnected(C,D), 531 delete_clause(ID), 532 store_clause(_,D,trc_unconn,ID),!. 533 534 535 536truncate_unconnected( ClauseIn, ClauseOut):- 537 skolemize(ClauseIn,S,ClauseInS ), 538 connected_skolems( ClauseInS, _Con, Uncon), 539 ClauseInS = [ Head:p | Body ], 540 truncate_unconnected1(Body, Uncon, BodyOut), 541 ClauseOutS = [ Head:p | BodyOut ], 542 deskolemize( ClauseOutS,S, ClauseOut). 543 544truncate_unconnected1([],_,[]). % no literals to drop 545truncate_unconnected1(B,[],B):-!. % all vars connected 546truncate_unconnected1([L:_ | More], Uncon, BodyOut):- 547 ( skolems( L, SKs), 548 member(A,SKs) % either all or no vars in L are connected 549 -> member(A,Uncon), % local cut 550 truncate_unconnected1(More,Uncon,BodyOut) 551 ; fail 552 ),!. 553truncate_unconnected1([L:S | More], Uncon, [L:S|BodyOut]):- 554 truncate_unconnected1(More,Uncon,BodyOut),!. 555 556 557%*********************************************************************** 558%* 559%* predicate: truncate_unconnecting/1/2 560%* 561%* syntax: truncate_unconnecting(ClauseIn,ClauseOut) 562%* 563%* args: clauses in list notation 564%* 565%* description: connectivity heuristics for truncation: 566%* Rouveirol: Drop a body literal if all other literals remain 567%* connected. 568%* We added another constraint: the resulting clause must be 569%* weakly generative. 570%* Do not confuse the connectivity with the connectedness 571%* heuristics !! 572%* 573%* example: truncate_unconnecting([p(X):n,q(X,V1):n,r(V1,V2):n,q(V3):n,s(V3,V1):n], 574%* [p(X):n,q(X,V1):n,r(V1,V2):n, s(V3,V1):n], 575%* 576%* peculiarities: 577%* 578%* see also: Rouveirol '90; module connectedness.pl 579%* 580%*********************************************************************** 581 582truncate_unconnecting(ID):- 583 get_clause(ID, _,_,C,_), 584 truncate_unconnecting(C,D), 585 delete_clause(ID), 586 store_clause(_,D,trc_unconn,ID),!. 587 588truncate_unconnecting( ClauseIn, ClauseOut):- 589 copy_term( ClauseIn, [H:p|Body]), 590 subseq(Body,[_L],BodyOut), 591 ClauseOut1 = [ H:p | BodyOut ], 592 connected_vars( ClauseOut1, ClauseOut, _Con, []), % no unconnected vars 593 is_weakly_generative(ClauseOut). 594 595 596%*********************************************************************** 597%* 598%* predicate: truncate_strongly_generative/2 599%* 600%* syntax: truncate_strongly_generative(+ClauseIn,-ClauseOut) 601%* 602%* args: clauses in list notation 603%* 604%* description: drop one body literal from a strongly generative 605%* clause s.t. the resulting clause is also strongly 606%* generative. 607%* 608%* example: 609%* 610%* peculiarities: 611%* 612%* see also: 613%* 614%*********************************************************************** 615 616truncate_strongly_generative(ID):- 617 get_clause(ID, _,_,C,_), 618 truncate_strongly_generative(C,D), 619 delete_clause(ID), 620 store_clause(_,D,trc_unconn,ID),!. 621 622truncate_strongly_generative(ClauseIn, ClauseOut):- 623 copy_term(ClauseIn,[H:p|Body]), 624 subseq(Body,[_L],BodyOut), 625 ClauseOut = [ H:p | BodyOut ], 626 is_strongly_generative(ClauseOut). 627 628 629%*********************************************************************** 630%* 631%* predicate: truncate_neg_based/1 632%* 633%* syntax: truncate_neg_based(+ID) 634%* 635%* args: integer, kb reference 636%* 637%* description: truncate as many literals as possible, s.t. the 638%* resulting clause covers no negative examples. 639%* 640%* This only works on unflat clauses; 641%* i.e. it only accounts for dropping condition. 642%* 643%* example: 644%* 645%* peculiarities: 646%* 647%* see also : Muggleton's negative based reduction 648%* 649%*********************************************************************** 650 651truncate_neg_based(ID):- 652 ( get_clause( ID, _,_,C, _Label) 653 ; 654 store_clause(_,C, _Label,ID), fail 655 ), 656 delete_clause(ID), 657 once(truncate_unconnected(C,D)), 658 store_clause(_,D,trc,ID), 659 correct_chk, 660 D = [ H | Body ], 661 length(Body,N), 662 truncate_neg_based1(N,ID, H, Body). 663 664truncate_neg_based1(0,_,_,_):-!. 665 666truncate_neg_based1(N, ID, H, Body):- 667 nth1(N,Body,_L,NewBody), 668 delete_clause(ID), 669 store_clause( _,[H|NewBody],trc,ID), 670 M is N - 1, 671 ( is_weakly_generative([H|NewBody]), 672 correct_chk 673 -> truncate_neg_based1(M,ID,H,NewBody) 674 ; 675 delete_clause(ID), 676 store_clause( _,[H|Body],trc,ID), 677 truncate_neg_based1( M, ID, H, Body) 678 ). 679 680 681%*********************************************************************** 682%* 683%* predicate: truncate_flat_neg_based/1 684%* 685%* syntax: truncate_flat_neg_based(+ID) 686%* 687%* args: integer, kb reference 688%* 689%* description: truncate as many literals as possible, s.t. the 690%* resulting clause covers no negative examples. 691%* 692%* As initial condition, the kb must be unflat. 693%* The truncation is done on the flattened clause, so that 694%* this accounts for the dropping rule & inverse subst. 695%* On exiting, the kb is unflat. 696%* 697%* example: 698%* 699%* peculiarities: 700%* 701%* see also : Muggleton's negative based reduction 702%* 703%*********************************************************************** 704 705truncate_flat_neg_based(ID):- 706 get_clause(ID,_,_,C,Label), 707 flatten_clause(C,D), 708 truncate_unconnected(D,E), 709 delete_clause(ID), 710 store_clause(_,E,_Trc,ID),!, 711 ( once(correct_chk), 712 D = [ H|Body], 713 truncate_flat_neg_based(ID,H,[],Body) 714 ; 715 delete_clause(ID), 716 store_clause(_,C,Label,ID) 717 ). 718 719truncate_flat_neg_based(ID,H,Nec,[]):- 720 delete_clause(ID), 721 truncate_unconnected([H|Nec],D), 722 unflatten_clause(D,E), 723 store_clause(_,E,trc,ID), 724 !, 725 correct_chk. 726 727 728truncate_flat_neg_based(ID,H,Nec,[L|Maybe]):- 729 append(Nec,Maybe,C), 730 truncate_unconnected([H|C],D), 731 unflatten_clause(D,E), 732 delete_clause(ID), 733 store_clause(_,E,trc,ID), 734 ( correct_chk -> Nec1 = Nec 735 ; 736 append(Nec,[L],Nec1) 737 ), 738 truncate_flat_neg_based(ID,H,Nec1,Maybe). 739 740 741%*********************************************************************** 742%* 743%* predicate: truncate_facts/1 744%* 745%* syntax: truncate_facts(+ID) 746%* 747%* args: integer, kb reference 748%* 749%* description: truncate all body literals unifying with a kb fact 750%* labeled 'usr'. 751%* 752%* example: 753%* 754%* peculiarities: 755%* 756%* see also: 757%* 758%*********************************************************************** 759 760truncate_facts(ID):- 761 get_clause(ID,_,_,[H|B],_), 762 truncate_facts1(B,BodyOut), 763 delete_clause(ID), 764 store_clause(_,[H|BodyOut],trc,ID). 765 766truncate_facts1([],[]). 767truncate_facts1([L:S|Rest], BodyOut):- 768 truncate_facts1(Rest,Rest1), 769 ( get_fact( _,L1,_,usr), 770 subsumes_chk(L1,L) -> BodyOut = Rest1 771 ; BodyOut = [ L:S|Rest1] 772 ). 773 774 775%*********************************************************************** 776%* 777%* predicate: truncate_j/2 778%* 779%* syntax: truncate_j(+ID,J) 780%* 781%* args: ID: kb reference 782%* J : integer = number of allowed new variables per literal 783%* 784%* description: truncate all literals containing more than J variables 785%* not appearing in the head of kb clause ID. 786%* 787%* example: 788%* 789%* peculiarities: 790%* 791%* see also: truncate_j is remotely related to Muggleton's 792%* ij-determination. We take i = 1. 793%* More importantly, we cannot tell in our system, if a 794%* literal is determinate or not, since we have no model. 795%* 796%*********************************************************************** 797 798truncate_j(ID,J):- 799 get_clause(ID,_,_,C,_), 800 skolemize( C, S, [Head:p|BodyIn] ) , 801 skolems(Head,Vars), 802 do_truncate_j( J, Vars, BodyIn, BodyOutS), 803 deskolemize( [Head:p|BodyOutS], S, D), 804 truncate_unconnected( D,E), 805 delete_clause(ID), 806 store_clause( _,E,trc_j,ID). 807 808do_truncate_j(J,Vars,BodyIn,BodyOut):- 809 findall( L, ( member(L,BodyIn), 810 once( ( skolems(L,VarsL), 811 subtract(VarsL,Vars,NewVars), 812 length(NewVars, J1), 813 J1 =< J 814 )) 815 ), 816 BodyOut)