1% MODULE g1_ops EXPORTS 2:- module( g1_ops, 3 [ saturate/2 , % saturate with default depth 4 saturate/3, % saturate with given maximum depth 5 elem_saturate/3, 6 inv_derivate/2, 7 inv_derivate/3, 8 inv_derivate1/2, 9 most_spec_v/3, 10 absorb/3, 11 identify/3, 12 g1_op/3, 13 g1_op/4, 14 apply_g1/2 15 ]). 16 17%IMPORTS 18:- use_module(home(lgg), 19 [headed_lgg/3,headed_lgg/4]). 20:- use_module(home(kb), 21 [get_clause/5,store_clause/4,delete_clause/1, 22 get_example/3]). 23:- use_module(home(var_utils), 24 [skolemize/3,skolemize/4,deskolemize/3]). 25:- use_module(home(div_utils), 26 [neg/2, buildpar2/3,efface/3]). 27:- use_module(home(bu_basics), 28 [addtolist/1,getlist/1,clear_mngr/0,assert_body/1, 29 abs_process_proofs/2,abs_build_body/1,assert_clause/1, 30 ident_process_proofs/2,g1_process_proofs/2,g1_build_clause/2, 31 idev_build_clause/2,process_new_literals/2,sat_build_clause/3, 32 assert_absorptions/2,body/3,ident_build_body/1]). 33:- use_module(home(show_utils), 34 [show_bodies/0]). 35:- use_module(home(interpreter), 36 [prove3/2,prove4/3]). 37:- use_module_if_exists(library(basics), 38 [member/2]). 39 40% METAPREDICATES 41% none 42 43 44%*********************************************************************** 45%* 46%* module: g1_ops.pl 47%* 48%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend date:12/92 49%* 50%* changed: 51%* 52%* 53%* description: - g1-Operator 54%* Implementation of Ruediger Wirth's G1-operator for inverse 55%* resolution corresponding to his 1989 PhD thesis. 56%* - Absorption 57%* All clauses induced by absorption are labelled "abs" in kb 58%* - Rouveirol's saturation, with functions allowed as terms. 59%* *Saturation: Maximum depth: given as input 60%* default: 100 inverse resolution steps 61%* *elementary saturation 62%* - inverse derivate 63%* Muggleton's inverse linear derivation, i.e. the 64%* repeated application of the most specific v 65%* (most specific absorption &most specific identification) 66%* Induced clauses are marked invd 67%* - identification 68%* clauses induced by identification are labelled "idn" in kb 69%* 70%* see also: 71%* 72%*********************************************************************** 73 74 75%********************************************************************************% 76%* 77%* predicate: g1_op/3, g1_op/4 78%* 79%* syntax: g1_op ( +ResolventID, +Parent1ID, -Parent2ID ) 80%* g1_op ( +ResolventID, +Parent1ID, -Parent2ID, + Label ) 81%* 82%* args: ResolventID, Parent1ID, Parent2ID .. clauseIDs 83%* Label for Parent2ID (default: g11) 84%* 85%* description: given a resolvent and one parent clause, the second parent clause 86%* is constructed 87%* 88%* example: 89%* 90%* peculiarities: 91%* 92%* see also: 93%* 94%******************************************************************************** 95 96g1_op( Res, Par1, Par2) :- 97 g1_op( Res, Par1, Par2, g11). 98g1_op( Res, Par1, Par2, Label) :- 99 (var(Label) -> Label = g11;true), 100 get_clause(Res,_,_,Lres,_), 101 get_clause(Par1,_,_,Lpar1,_), % clauses in list representation 102 Res \== Par1, % not a clause with itself 103 clear_mngr, 104 skolemize(Lres,SS,LresSko), % skolemize resolvent 105 assert_clause(LresSko), 106 findall(Uncovered:Proof,prove4(Lpar1,Uncovered,Proof),Proofs), 107 g1_process_proofs(Proofs,Reslit), 108 g1_build_clause(Reslit,Lpar2Sko), % build parent2 109 deskolemize(Lpar2Sko,SS,Lpar2), % deskolemize 110 store_clause(_,Lpar2,Label,Par2). % and store 111 112 113%********************************************************************************% 114%* 115%* predicate: extend_g1/2 116%* 117%* syntax: extend_g1(+Ai_ID,-A_Id) 118%* 119%* args: clauseIDs 120%* 121%* description: locates suitable V's that are already available in the kb 122%* 123%* example: 124%* 125%* peculiarities: 126%* 127%* see also: 128%* 129%********************************************************************************% 130 131extend_g1(Ai_id, A_id) :- 132 get_clause(Ai_id,_,_,Ai,_), 133 length(Ai,Li), 134 get_clause(Aj_id,_,_,Aj,g11), 135 Ai_id \== Aj_id, 136 length(Aj,Li), 137 headed_lgg(Ai_id,Aj_id,A_id,g1), 138 get_clause(A_id,_,_,A,_), 139 length(A,L), 140 (L >= Li -> % heuristic 141 delete_clause(Aj_id); 142 delete_clause(A_id), 143 fail). 144 145 146%*********************************************************************** 147%* 148%* predicate: apply_g1/2 149%* 150%* syntax: apply_g1( + NewClauseId, - List_of_ResultIds ) 151%* 152%* args: 153%* 154%* description: One might want to use apply_g1/2 if a new clause of background 155%* knowledge is added to the kb and the G1-operator is to be applied. 156%* If there already is a suitable "V", it will be extended and the 157%* lgg of two A's will be built. 158%* 159%* A 160%* Bi / \ Bj 161%* \ Ai Aj / 162%* \ / \ / 163%* Ci Cj 164%* 165%* If a clause A can be built as lgg of Ai and Aj (extend_g1/2), 166%* Ai and Aj will be deleted. 167%* 168%* example: 169%* 170%* peculiarities: none 171%* 172%* see also: 173%* 174%*********************************************************************** 175 176apply_g1(Clause,_) :- % use new clause as parent1 177 g1_op(_,Clause,Par2), 178 findall(GenPar2, (extend_g1(Par2,GenPar2)), Bag), 179 (Bag == [] -> addtolist(Par2); 180 delete_clause(Par2), addtolist(Bag)), 181 fail, !. 182apply_g1(Clause,_) :- % use new clause as resolvent 183 g1_op(Clause,_,Par2), 184 findall(GenPar2, (extend_g1(Par2,GenPar2)), Bag), 185 (Bag == [] -> addtolist(Par2); 186 delete_clause(Par2), addtolist(Bag)), 187 fail. 188apply_g1(_,List) :- getlist(List). 189 190 191%*********************************************************************** 192%* 193%* predicate: absorb/3 194%* 195%* syntax: absorb(+ExID, ?Parent1ID, -NewID) 196%* 197%* args: ExID: ID of example clause 198%* Parent1ID: id of known parent clause 199%* NewID: ID of absorption of example clause 200%* 201%* description: apply one absorption step on input clause ExID; 202%* if Parent1ID is given, it is tried to perform the 203%* absorption step with it as known parent. 204%* Otherwise absorption will be performed with the first 205%* applicable background clause. 206%* It is made sure that no 2 literals of a parent 207%* clause abs_match the same literal in the resolvent. 208%* 209%* example: 210%* 211%* peculiarities: no inverse subsitution yet 212%* 213%* see also: 214%* 215%*********************************************************************** 216 217 218% parent given 219absorb(ExID,PID,NewID):- 220 nonvar(PID), 221 clear_mngr, 222 get_clause(ExID,_,_,Ex,_), 223 skolemize(Ex,S,[SHead:p|SBody]), 224 assert_body(SBody), 225 !, 226 abs_match1(PID,success,Proofs), 227 abs_process_proofs(Proofs,PHead), 228 abs_build_body(Body1), 229 append(Body1,[PHead:n],Body), 230 NewClauseS = [ SHead:p | Body ], 231 deskolemize(NewClauseS,S, NewClause), 232 store_clause(_,NewClause,abs,NewID). 233 234 235 236% parent not given 237absorb(ExID,PID,NewID):- 238 var(PID), 239 clear_mngr, 240 get_clause(ExID,_,_,Ex,_), 241 skolemize(Ex,S,[SHead:p|SBody]), 242 assert_body(SBody), 243 !, 244 abs_match(ExID,success,Proofs), 245 abs_process_proofs(Proofs,PHead), 246 abs_build_body(Body1), 247 append(Body1,[PHead:n],Body), 248 NewClauseS = [ SHead:p | Body ], 249 deskolemize(NewClauseS,S, NewClause), 250 store_clause(_,NewClause,abs,NewID). 251 252 253%*********************************************************************** 254%* 255%* predicate: abs_match/3 256%* 257%* syntax: abs_match(+ExID,-Mark,-Proofs) 258%* 259%* args: ExID: Id of the resolvent 260%* Mark in {success,fail} 261%* Proofs = [CL,...] where CL is a clause in list notation 262%* 263%* description: returns all (instantiated) clauses that can be embedded in the 264%* skolemized example clause (stored in kb with head/3,body/3) 265%* 266%* example: 267%* 268%* peculiarities: none 269%* 270%* see also: 271%* 272%*********************************************************************** 273 274abs_match( ExID, Mark,Proofs):- 275 ( findall(Proof, abs_match0(ExID,Proof), Proofs) 276 -> Mark = success 277 ; 278 Proofs = [], Mark = fail 279 ). 280 281abs_match0( ExId, [Goal:p|Proof]):- 282 get_clause(I,_,_,[Goal:p|Body],usr), 283 I \== ExId, 284 prove3(Body,Proof). 285 286 287%*********************************************************************** 288%* 289%* predicate: abs_match1/3 290%* 291%* syntax: abs_match1(+PID,-Mark,-Proofs) 292%* 293%* args: PID: ID of a parent clause 294%* 295%* description: as abs_match, except for the fixed parent clause that 296%* is embedded in the resolvent 297%* 298%* example: 299%* 300%* peculiarities: none 301%* 302%* see also: 303%* 304%*********************************************************************** 305 306abs_match1(PID, Mark, Proofs):- 307 ( findall(Proof, abs_match1a(PID,Proof), Proofs) 308 -> Mark = success 309 ; 310 Proofs = [], Mark = fail 311 ). 312 313abs_match1a( PID, [Goal:p|Proof]):- 314 get_clause(PID,_,_,[Goal:p|Body],_), 315 prove3(Body,Proof). 316 317 318%*********************************************************************** 319%* 320%* predicate: identify/3 321%* 322%* syntax: identify(+ExID, ?Parent1ID, -NewID) 323%* 324%* args: ExID: ID of example clause 325%* Parent1ID: id of known parent clause 326%* NewID: ID of identification of example clause 327%* 328%* description: apply one identification step on input clause ExID; 329%* if Parent1ID is given, it is tried to perform the 330%* identification step with it as known parent. 331%* Otherwise identification will be performed with the 332%* first applicable background clause. 333%* It is made sure that no 2 literals of a parent 334%* clause ident_match the same literal in the resolvent. 335%* 336%* example: 337%* 338%* peculiarities: no inverse subsitution yet 339%* no backtraking 340%* 341%* see also: 342%* 343%*********************************************************************** 344 345% parent given 346identify(ExID,PID,NewID):- 347 nonvar(PID), 348 clear_mngr, 349 get_clause(ExID,_,_,Ex,_), 350 skolemize(Ex,S,SClause), 351 assert_clause(SClause), 352 !, 353 ident_match1(PID,success,Proofs), 354 ident_process_proofs(Proofs,PHead), 355 ident_build_body(Body1), 356 NewClauseS = [ PHead:p | Body1 ], 357 deskolemize(NewClauseS,S, NewClause), 358 store_clause(_,NewClause,idn,NewID). 359 360 361 362% parent not given 363identify(ExID,PID,NewID):- 364 var(PID), 365 get_clause(ExID,_,_,Ex,_), 366 clear_mngr, 367 skolemize(Ex,S,SClause), 368 assert_clause(SClause), 369% show_bodies, 370 ident_match(ExID,success,Proofs), 371 ident_process_proofs(Proofs,PHead), 372 ident_build_body(Body1), 373 NewClauseS = [ PHead:p | Body1 ], 374 deskolemize(NewClauseS,S, NewClause), 375 store_clause(_,NewClause,idn,NewID). 376 377 378 379%*********************************************************************** 380%* 381%* predicate: ident_match/3 382%* 383%* syntax: ident_match(+ExID,-Mark,-Proofs) 384%* 385%* args: ExID: ID of the resolvent 386%* Mark in {success,fail} 387%* Proofs = [P1,..,Pm], where Pi=[Uncovered:Proof] and 388%* Uncovered = Lit/M (M in {new_head,new_body}), Proof = [[Lit,N],...] 389%* (N in {head,body} 390%* 391%* description: matches clauses in kb against skolemized resolvent (stored 392%* in kb with head/3,body/3), Uncovered is the resolution 393%* literal that might be positive (new_head) or negative 394%* (new_body) 395%* 396%* example: 397%* 398%* peculiarities: none 399%* 400%* see also: 401%* 402%*********************************************************************** 403 404ident_match( ExID, Mark,Proofs):- 405 ( findall(Proof, ident_match0(ExID,Proof), Proofs) 406 -> Mark = success 407 ; 408 Proofs = [], Mark = fail 409 ). 410 411 412ident_match0( ExId, [Uncovered:Proof]):- 413 get_clause(I,_,_,Clause,usr), 414 I \== ExId, 415 prove4(Clause,Uncovered,Proof). 416 417 418%*********************************************************************** 419%* 420%* predicate: ident_match1/3 421%* 422%* syntax: ident_match1(+PID,-Mark,-Proofs) 423%* 424%* args: PID ...parentID, Mark,Proofs as for ident_match 425%* 426%* description: as ident_match, except for the parent clause to be matched 427%* against the resolvent is given 428%* 429%* example: 430%* 431%* peculiarities: none 432%* 433%* see also: 434%* 435%*********************************************************************** 436 437ident_match1(PID, Mark, Proofs):- 438 ( findall(Proof, ident_match1a(PID,Proof), Proofs) 439 -> Mark = success 440 ; 441 Proofs = [], Mark = fail 442 ). 443 444 445ident_match1a( PID, [Uncovered:Proof]):- 446 get_clause(PID,_,_,Clause,_), 447 prove4(Clause,Uncovered,Proof). 448 449 450%*********************************************************************** 451%* 452%* predicates: inv_derivate/2/3 453%* 454%* syntax: inv_derivate(+ExID,-NewID) 455%* inv_derivate(+ExID,+PrefHead,-NewID) 456%* 457%* args: ExID : id of example 458%* NewID: id of expanded example 459%* PrefHead: a prolog literal 460%* 461%* description: Muggleton's inverse linear derivation 462%* But: 463%* while in intermediate stages several head literals 464%* might appear simultanously, the result will always 465%* be a Horn clause. As head literal we choose the 466%* latest one derived in inv_derivate/2. 467%* inv_derivate/3 takes as additional argument 468%* a literal, which is interpreted as a preferred 469%* head. If it is possible, inv_derivate/3 results 470%* in a Horn clause where the head matches this 471%* literal. 472%* The operator is restricted to finding clauses at most 473%* 100 inverse resolution steps away. 474%* 475%* example: inv_derivate(1, member(A,B), ID) 476%* 477%* peculiarities: 478%* 479%* see also: 480%* 481%*********************************************************************** 482 483inv_derivate(ExID,NewID):- 484 clear_mngr, 485 ( get_clause(ExID,_,_,CList,_) 486 ; 487 get_example(ExID,Ex,'+'), CList = [Ex:p] 488 ), 489 skolemize(CList,S,CListS), 490 assert_clause(CListS), 491 inv_derivate1(ExID,1), 492 idev_build_clause(_,Clause1), 493 deskolemize(Clause1,S,Clause), 494 store_clause(_,Clause,invd,NewID),!. 495 496 497inv_derivate(ExID,PrefHead,NewID):- 498 clear_mngr, 499 get_clause(ExID,_,_,CList,_), 500 skolemize(CList,S,CListS), 501 assert_clause(CListS), 502 inv_derivate1(ExID,1), 503 idev_build_clause(PrefHead,Clause1), 504 deskolemize(Clause1,S,Clause), 505 store_clause(_,Clause,invd,NewID),!. 506 507inv_derivate1(ExID,I):- 508 setof(U:P,ExID^Clause^idev_match0(ExID,Clause,U,P),Proofs), 509 process_new_literals(Proofs,Flag), 510 ( nonvar(Flag), I<100 511 -> J is I + 1,inv_derivate1(ExID,J) 512 ; true 513 ). 514 515 516%*********************************************************************** 517%* 518%* predicate: idev_match0/4 519%* 520%* syntax: idev_match0(+ExID,-Clause,-Uncovered,-Proof) 521%* 522%* args: ExID: ID of the resolvent 523%* Clause: clause in list notation 524%* Uncovered: Lit/M, where M in {new_head,new_body} 525%* Proof: [[Lit,N],...] where N in {head,body} 526%* 527%* description: matches clause on skolemized resolvent (stored in kb 528%* with head/3, body/3), and returns the instantiation 529%* of clause and the resolution literal (Uncovered) 530%* 531%* example: 532%* 533%* peculiarities: none 534%* 535%* see also: 536%* 537%*********************************************************************** 538 539idev_match0( ExID,Clause, Uncovered, Proof):- 540 get_clause(ID,_,_,Clause,_), 541 ExID \== ID, 542 prove4(Clause,Uncovered,Proof). 543 544 545%*********************************************************************** 546%* 547%* predicate: most_spec_v/3 548%* 549%* syntax: most_spec_v(+ExID, ?PID, -NewID) 550%* 551%* args: ExID: id of example (resolvent) 552%* PID: id of known parent 553%* NewID: id of new clause 554%* 555%* description: 556%* Apply one most-spec-v operation to example with parent PID; 557%* If PID is not given, take the first applicable clause 558%* of bg as parent. 559%* The most specific v comprises the most specific absorption 560%* and the most specific identification. 561%* Since we always want Horn clauses as a result, this operator 562%* does not implement the most specific identification as 563%* described by Muggleton: Instead of adding a second head 564%* literal to the old clause, we replace the original head. 565%* I.e. our most specific identification operator is destructive. 566%* The most specific absorption remains nondestructive 567%* 568%* example: 569%* 570%* peculiarites: 571%* 572%* see also: inv_derivate/2 where multiple head literals are 573%* allowed om intermediate stages. 574%* 575%*********************************************************************** 576 577most_spec_v(ExID,PID,NewID):- 578 ( get_clause(ExID,_,_,CList,_) 579 ; 580 get_example(ExID,Ex,'+'), CList = [Ex:p] 581 ) , 582 clear_mngr, 583 skolemize(CList,S,CListS), 584 assert_clause(CListS), 585 idev_match1(ExID,_,Uncovered,Proof,PID), 586 % Uncovered \== [], 587 process_new_literals([Uncovered:Proof],Flag), 588 nonvar(Flag), 589 idev_build_clause(_,Clause1), 590 deskolemize(Clause1,S,Clause), 591 store_clause(_,Clause,msv,NewID). 592 593 594 595%*********************************************************************** 596%* 597%* predicate: idev_match1/5 598%* 599%* syntax: idev_match1(+ExID,-Clause,-Uncovered,-Proof,-ID) 600%* 601%* args: ExID: ID of the resolvent, ID: ID of matched clause 602%* Clause: clause in list notation 603%* Uncovered: Lit/M, where M in {new_head,new_body} 604%* Proof: [[Lit,N],...] where N in {head,body} 605%* 606%* description: is like idev_match0/4, but returns id of absorbed clause 607%* 608%* example: 609%* 610%* peculiarities: none 611%* 612%* see also: 613%* 614%*********************************************************************** 615 616idev_match1( ExID,Clause, Uncovered, Proof,ID):- 617 get_clause(ID,_,_,Clause,_), 618 ExID \== ID, 619 prove4(Clause,Uncovered,Proof). 620 621 622%*********************************************************************** 623%* 624%* predicate: saturate/2,saturate/3 625%* 626%* syntax: saturate(+ExID, -NewID), saturate(+ExID,-NewID,+Bound) 627%* 628%* args: ExID: ID of example clause 629%* NewID: ID of saturation of example clause 630%* 631%* description: apply elementary saturation w.r.t. background 632%* clauses. 633%* It is bounded by at most 100 iterations, if bound is not given 634%* When checking the preconditions for firing one 635%* absorption step, 636%* it is made sure that no 2 literals of a parent 637%* clause subsume the same literal in the resolvent. 638%* 639%* example: 640%* 641%* peculiarities: 642%* 643%* see also: 644%* 645%*********************************************************************** 646 647saturate(ExID,GenID):- 648 saturate(ExID,GenID,100). 649 650saturate(ExID,GenID,Bound):- 651 saturate1(ExID,NewClause,Bound), % Rouveirol's theorem proving alg. 652 653 % write(NewClause),nl, 654 store_clause(_,NewClause,sat,GenID), 655 !. % no backtracking 656 657 658 659%*********************************************************************** 660%* 661%* predicate: saturate1/3 662%* 663%* syntax: saturate1(+ExID,-NewClause,+Bound) 664%* 665%* args: ExID .. ID of example clause, NewClause .. Prolog clause in list notation, 666%* Bound .. bound for interations 667%* 668%* description: saturates example clause w.r.t. background knowledge. 669%* It is bounded by at most Bound interations. 670%* 671%* example: 672%* 673%* peculiarities: none 674%* 675%* see also: 676%* 677%*********************************************************************** 678 679saturate1(ExID,NewClause,Bound):- 680 clear_mngr, 681 get_clause(ExID,H,_B,T,_), 682 skolemize( T,S,[HS:p|U]), 683 assert_body(U), 684 saturate1a(HS,1,Bound,S,S1), 685 bagof(A, M^I^body(A,I,M), NewBody1), 686 sat_build_clause( H, NewBody1, Clause1), % Clause in list notation 687 deskolemize( Clause1,S1,NewClause). 688 689 690%*********************************************************************** 691%* 692%* predicate: saturate1a/5 693%* 694%* syntax: saturate1a(+HS,+Count,+Bound,+Subst,-Subst) 695%* 696%* args: HS: skolemized head of the example clause, 697%* Count,Bound: integers 698%* Subst: skolem subtitutions 699%* 700%* description: while Count < Bound, all heads following from the saturated 701%* clause so far (stored as body(Lit,_,_)) are asserted as 702%* additional body-literals (via body/3) 703%* 704%* example: 705%* 706%* peculiarities: none 707%* 708%* see also: 709%* 710%*********************************************************************** 711 712saturate1a(HS,I,Bound,S1,S2):- 713 sat_match(HS,success,Proofs), 714 !, 715 skolemize(Proofs,S1,S3,Proofs1), 716 assert_absorptions(Proofs1,Flag), 717 ( nonvar(Flag), I < Bound 718 -> J is I +1, saturate1a(HS,J,Bound,S3,S2) 719 ; 720 S2 = S3 721 ). 722 723 724saturate1a(_,_,_,S,S):- !. 725 726 727%*********************************************************************** 728%* 729%* predicate: sat_match/3 730%* 731%* syntax: sat_match(+HS,-M,-Proofs) 732%* 733%* args: HS: skolemized head of the example clause 734%* Proofs = [CL,...] where each CL is a clause in list notation 735%* 736%* description: finds all possible proofs for all possible absorptions 737%* 738%* example: 739%* 740%* peculiarities: none 741%* 742%* see also: 743%* 744%*********************************************************************** 745 746sat_match(HS,Mark,Proofs):- 747 ( setof(Proof,HS^sat_match0(HS,Proof), Proofs ) 748 -> Mark = success 749 ; 750 Proofs = [], 751 Mark = fail 752 ). 753 754sat_match0(HS,[Goal:p|ProofBody]):- 755 get_clause(_I,_,_,[Goal:p|Body],_), 756 prove3(Body,ProofBody), 757 Goal \== HS. 758 759 760%*********************************************************************** 761%* 762%* predicate: elem_saturate/3 763%* 764%* syntax: elem_saturate( +ExID, ?PID, -NewID) 765%* 766%* args: ExID: id of resolvent 767%* PID : id of parent in bg 768%* NewID: id of new parent 769%* 770%* description: 771%* Add head of parent from bg to body of resolvent. 772%* The Operator is identical to Muggleton's 773%* most-specific-absorption. 774%* When checking the preconditions for firing one 775%* absorption step, 776%* it is made sure that no 2 literals of a parent 777%* clause subsume the same literal in the resolvent. 778%* 779%* example: 780%* 781%* peculiarities: 782%* 783%* see also: 784%* 785%*********************************************************************** 786 787% parent given 788elem_saturate(ExID,PID,NewID):- 789 nonvar(PID), 790 clear_mngr, 791 get_clause(ExID,_,_,[H:p|B],_), 792 skolemize(B,S,BS), 793 assert_body(BS), 794 get_clause(PID,_,_,[Goal:p|Body],_), 795 prove3(Body,ProofBody), 796 assert_absorptions([ [Goal:p|ProofBody]],Flag), 797 nonvar(Flag), 798 findall( L, body(L,_I,_M) ,NewBody), 799 sat_build_clause(H,NewBody,Clause1), 800 deskolemize(Clause1,S,NewClause), 801 store_clause(_,NewClause,esat,NewID). 802 803 804% parent not given 805elem_saturate(ExID,PID,NewID):- 806 var(PID), 807 clear_mngr, 808 get_clause(ExID,_,_,[H:p|B],_), 809 skolemize(B,S,BS), 810 assert_body(BS), 811 sat_match1(ExID, [Goal:p|ProofBody],PID), 812 assert_absorptions([ [Goal:p|ProofBody]],Flag), 813 nonvar(Flag), 814 findall( L, body(L,_I,_M) ,NewBody), 815 sat_build_clause(H,NewBody,Clause1), 816 deskolemize(Clause1,S,NewClause), 817 store_clause(_,NewClause,esat,NewID). 818 819 820%*********************************************************************** 821%* 822%* predicate: sat_match1/3 823%* 824%* syntax: sat_match1(+ExID,-Proof,-ID) 825%* 826%* args: ExID,ID: clauseIDs, Proofs: clause in list notation 827%* 828%* description: is like sat_match0/2, but returns id of absorbed clause 829%* 830%* example: 831%* 832%* peculiarities: none 833%* 834%* see also: 835%* 836%*********************************************************************** 837 838sat_match1(Ex,[Goal:p|ProofBody],I):- 839 get_clause(I,_,_,[Goal:p|Body],_), 840 I \== Ex, 841 prove3(Body,ProofBody)