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