1% MODULE interpreter EXPORTS 2:- module( interpreter, 3 [ solve/3, 4 solve_once/3, 5 failed_proof/1, 6 prooftrees/3, 7 proof_close/2, 8 prove1/2, 9 prove3/2, 10 prove4/3, 11 12 prove5/2, 13 14 proof_path/4, 15 set_proof_depth/0, 16 17 t_interpreter/2, 18 ip_part1/2, 19 ip_part2/3 ]). 20 21% IMPORTS 22:- use_module(home(kb), 23 [get_clause/5,interpretable_predicate/1]). 24:- use_module(home(div_utils), 25 [insert_unique/3,identical_member/2,append_all/2,mysetof/3]). 26:- use_module(home(bu_basics), 27 [head/3,body/3,assumption/3]). 28:- use_module(home(environment), 29 [satisfiable/1]). 30:- use_module_if_exists(library(basics), 31 [member/2]). 32:- use_module_if_exists(library(unify), 33 [unify/2]). 34 35 36% METAPREDICATES 37% none 38 39 40:- dynamic failed_proof/1, tag/1, prooftrees/3, depth_bound/1,depth_exceeded/0, 41 depth_exceeded/3. 42 43 44 45%*********************************************************************** 46%* 47%* module: interpreter.pl 48%* 49%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend date:12/92 50%* 51%* changed: 52%* 53%* description: different interpreters working on the knowledge base 54%* 55%* see also: 56%* 57%*********************************************************************** 58 59 60%*********************************************************************** 61%* 62%* predicate: ip_part1/2 63%* 64%* syntax: ip_part1(+Goal,-Proof) 65%* 66%* args: Goal: an uncovered positive example 67%* Proof: a failing proof for the positive example 68%* 69%* description: works exactly as the general interpreter solve0/2. The only 70%* difference is that instead of failing when a system goal is failing 71%* or a proof is looping or rules are missing, the interpreter 72%* continues, assuming that the failing goals should be correct 73%* 74%* example: 75%* 76%* peculiarities: none 77%* 78%* see also: 79%* 80%*********************************************************************** 81 82ip_part1(Goal,Proof) :- 83 retractall(tag(_)), 84 assert(tag(Goal)), 85 gen_depth(D, Delta), 86 ipp1(Goal,D,Delta,Proof,Proof,[]). 87 88ipp1(true,_D,_Delta,_Proof,Poi,_) :- 89 !, 90 Poi = []. 91 92ipp1(no_rule,_,_,_,_,_):- !. 93 94ipp1((A,B),D, Delta,Proof,Poi,Ancestors) :- 95 !, Poi = [PoiA|PoiB], 96 ipp1(A,D, Delta,Proof,[PoiA],Ancestors), 97 ipp1(B,D, Delta,Proof,PoiB,Ancestors). 98 99ipp1(A,D, Delta,Proof,Poi,Ancestors) :- 100 interpretable_predicate(A),!, 101 ( D > 0 -> 102 true 103 ; assert(tag(A)),fail 104 ), 105 ( identical_member(A,Ancestors) -> 106 Poi = [[-1,A,looping]] 107 ; D1 is D - 1, 108 ipp1_rule(D,Delta,Proof,Poi,I,A, B), 109 Poi = [[I,A,PoiB]], 110 ipp1(B,D1, Delta,Proof,PoiB,[A|Ancestors]) 111 ). 112 113ipp1(A,_D, _Delta,_Proof,Poi,_):- 114 ( call(A) -> 115 Poi = [[sys,A,[]]] 116 ; Poi = [[sys,A,fail]] 117 ). 118 119 120 121ipp1_rule(_,_,_,_,I,A,B):- get_clause(I,A,B,_,_). 122ipp1_rule(_D,_Delta,_Proof,Poi,_,A,no_rule):- 123 ( get_clause(_,A,_,_,_) -> 124 fail 125 ; Poi = [[-1,A,no_rules]] 126 ). 127 128 129%*********************************************************************** 130%* 131%* predicate: ip_part2/3 132%* 133%* syntax: ip_part2(+Proofs,+Goal,-Uncovered_Atoms) 134%* 135%* args: Proofs: failing proofs determined by ip_part1, 136%* Goal: uncovered positive example Uncovered_Atoms: Atoms that make 137%* Goal succeed, if they were covered by the kb 138%* 139%* description: the satisfiability of each subgoal within failing proof is 140%* determined. For that, the oracle might be necessary. 141%* 142%* example: 143%* 144%* peculiarities: none 145%* 146%* see also: 147%* 148%*********************************************************************** 149 150ip_part2([P|_],_Goal,UA):- 151 ipp2(P,[],[],UA). 152ip_part2([_|R],Goal,UA):- 153 ip_part2(R,Goal,UA). 154 155ipp2([I,H,looping],_,L,[I:H|L]):- !. 156ipp2([sys,_,fail],[I:A|_],L,[I:A|L]):- !. 157ipp2([_,_,[]],_,L,L):- !. 158ipp2([_,H,no_rules],_,L,[-1:H|L]):- !. 159ipp2([I,H,SG],Ancestors,L,L1):- 160 ( satisfiable(SG) -> 161 ipp2_list(SG,[I:H|Ancestors],L,L1) 162 ; L1 = [I:H|L] 163 ). 164 165 166ipp2_list([],_,L,L). 167ipp2_list([G|R],A,L,L2):- 168 ipp2(G,A,L,L1), 169 ipp2_list(R,A,L1,L2). 170 171 172%*********************************************************************** 173%* 174%* predicate: proof_path/4 175%* 176%* syntax: proof_path(+Ex,+Pred,+Type,-ClauseIDs) 177%* 178%* args: Ex: example for p/n 179%* Pred = p(X1,..,Xn): most general term of p/n 180%* Type = typei(Xi) for an argument of p/n 181%* ClauseIDs: list of clauseIDs that have beed used for proving 182%* typei(ei) for the ith argument of Ex 183%* 184%* description: simulates the proof of typei(ei) for the ith argument of Ex 185%* and collects the indices of all used clauses 186%* 187%* example: 188%* 189%* peculiarities: none 190%* 191%* see also: 192%* 193%*********************************************************************** 194 195proof_path(Ex,P,T,Ts):- 196 copy_term((P,T),(Ex,T0)), 197 proof_path(T0,[],Ts). 198 199proof_path(true,T,T):- !. 200proof_path((A,B),T,T2):- !, 201 proof_path(A,T,T1), 202 proof_path(B,T1,T2). 203 204proof_path(A,T,T):- 205 A =.. [all|_],!. 206proof_path(A,T,T):- 207 A =.. [T1|_], 208 ( T1 = atom; T1 = atomic; T1 = number ),!, 209 call(A). 210 211proof_path(A,T,T1):- 212 get_clause(I,A,B,_,type), 213 proof_path(B,T,T0), 214 insert_unique(I,T0,T1). 215 216 217%*********************************************************************** 218%* 219%* predicate: t_interpreter/2 220%* 221%* syntax: t_interpreter(+Goal,+ClauseList) 222%* 223%* args: Goal: goal type(Arg), Arg ground 224%* ClauseList: List of clauses defining different types 225%* 226%* description: proves type(Arg) from ClauseList as kb 227%* 228%* example: 229%* 230%* peculiarities: none 231%* 232%* see also: 233%* 234%*********************************************************************** 235 236t_interpreter(true,_):- !. 237t_interpreter((A,B),CL):- !, 238 t_interpreter(A,CL), 239 t_interpreter(B,CL). 240t_interpreter(C,_):- 241 C =.. [P|_], 242 ( P = atom ; P = number ; P = atomic ),!, 243 call(C). 244t_interpreter(C,CL):- 245 copy_term(CL,CL1), 246 member((C:-B),CL1), 247 t_interpreter(B,CL). 248 249 250 251%************************************************************************ 252%* 253%* predicate: solve/3 254%* 255%* syntax: solve(+Goal,-Mark,-Proofs) 256%* 257%* args: Goal: ground atom or rule with ground head 258%* Mark: success or fail 259%* Proofs: all succeeding/failing proofs according to Mark 260%* 261%* description: format for Proofs: [P1,..,Pn] 262%* where Pi = [ID,Head,PBody] where ID is the ID of the 263%* applied rule (sys for system predicates, -1 if no rule 264%* is applicable), Head is the instantiation of the rule head, 265%* and PBody is the proof of the rule body. PBody is of the form 266%* - [], if Head is true 267%* - fail, if Head is a failing syspred 268%* - looping if the proof is looping on Head 269%* - no_rules if no rules match Head 270%* - depth_exceeded if the proof fails because of depth bound 271%* Maximum depth for proofs: 50 272%* 273%* example: 274%* 275%* peculiarities: 276%* 277%* see also: 278%* 279%************************************************************************ 280 281solve( (H :- B), Mark, Proofs) :- 282 ground(H) -> 283 solve( B, Mark, Proofs) 284 ; !, fail. 285 286solve(Goal,Mark,Proofs):- 287 ( setof(Proof,Goal^solve0(Goal,Proof),Proofs0) -> 288 Mark = success 289 ; bagof(FProof,failed_proof(FProof),Proofs00), 290 Mark = fail, 291 ( depth_exceeded -> 292 setof(EProof,A^depth_exceeded(A,EProof,[[-1,A,depth_exceeded]]),EProofs0), 293 append(EProofs0,Proofs00,Proofs0) 294 ; Proofs0 = Proofs00 295 ) 296 297 ), 298 append_all(Proofs0,Proofs1), 299 proof_close(Proofs1,Proofs). 300 301 302%*********************************************************************** 303%* 304%* predicate: solve_once/3 305%* 306%* syntax: solve_once(+Goal,-Mark,-Proof) 307%* 308%* args: as solve/3 309%* 310%* description: proves Goal only once 311%* 312%* example: 313%* 314%* peculiarities: none 315%* 316%* see also: 317%* 318%*********************************************************************** 319 320solve_once( (H :- B), Mark, Proofs) :- 321 ground(H) -> 322 solve_once( B, Mark, Proofs) 323 ; !, fail. 324 325solve_once(Goal,Mark,Proofs):- 326 ( solve0(Goal,Proof) -> Proofs0 = [ Proof ], 327 Mark = success 328 ; bagof(FProof,failed_proof(FProof),Proofs0), 329 Mark = fail 330 ), 331 append_all(Proofs0,Proofs1), 332 proof_close(Proofs1,Proofs). 333 334 335 336%*********************************************************************** 337%* 338%* predicate: proof_close/2 339%* 340%* syntax: proof_close(+Proofs,-Proofs) 341%* 342%* args: Proofs as for solve/3 343%* 344%* description: closes the open lists in Proofs 345%* 346%* example: 347%* 348%* peculiarities: none 349%* 350%* see also: 351%* 352%*********************************************************************** 353 354proof_close(X,[]):- 355 var(X),!. 356proof_close([[J,H,B1]|R1],[[J,H,B2]|R2]):- 357 proof_close(B1,B2), 358 proof_close(R1,R2). 359proof_close(X,X):- 360 atomic(X),!. 361 362 363%*********************************************************************** 364%* 365%* predicate: solve0/2 366%* 367%* syntax: solve0(+Goal,-Proof) 368%* 369%* args: Goal: ground atom, Proof: one possible proof for Goal 370%* 371%* description: 372%* 373%* example: 374%* 375%* peculiarities: none 376%* 377%* see also: 378%* 379%*********************************************************************** 380 381solve0(Goal,Proof) :- 382 retractall(tag(_)),retractall(failed_proof(_)),retractall(depth_exceeded(_,_,_)), 383 retractall(depth_exceeded), 384 gen_depth(D, Delta), 385 solve2(Goal,D,Delta,Proof,Proof,[]). 386 387 388solve2(true,_,_,_,[],_) :- !. 389 390 391solve2((A,B),D,Delta,Proof,Poi,Ancestors) :- 392 !, 393 Poi = [PoiA|PoiB], 394 solve2(A,D,Delta,Proof,[PoiA],Ancestors), 395 solve2(B,D,Delta,Proof,PoiB,Ancestors). 396 397 398solve2(A,D,Delta,Proof,Poi,Ancestors) :- % A is in KB 399 interpretable_predicate(A),!, 400 ( D = 0 -> assert(tag(A)), assert(depth_exceeded(A,Proof,Poi)), fail 401 ; ( identical_member(A,Ancestors) -> 402 Poi = [[-1,A,looping]], 403 ( D < Delta -> 404 assert(failed_proof(Proof)) 405 ; true 406 ), 407 fail 408 ; D1 is D - 1, 409 solve_rule(D1,Delta,Proof,Poi,I,A, B), 410 Poi = [[I,A,PoiB]], 411 solve2(B,D1,Delta,Proof,PoiB,[A|Ancestors]) 412 ) 413 ). 414 415solve2(A,D,Delta,Proof,Poi,_):- % A is built-in 416 ( 417 predicate_property(A,built_in), 418 on_exception(_,call(A),fail) -> % exception handling 419 Poi = [[sys,A,[]]] 420 ; Poi = [[sys,A,fail]], 421 ( D < Delta -> 422 assert(failed_proof(Proof)) 423 ; true 424 ), 425 fail 426 ). 427 428 429solve2(A,D,D,Proof,Poi,_) :- % no rules at all for initial goal 430 \+(depth_exceeded), 431 Poi = [[-1,A,no_rules]], 432 assert(failed_proof(Proof)), 433 fail. 434 435 436%*********************************************************************** 437%* 438%* predicate: solve_rule/7 439%* 440%* syntax: solve_rule(+D,+Delta,+Proof,+Proof_Poi,-ID,+Goal,-Body) 441%* 442%* args: D,Delta: depth bounds for iterative deepening 443%* Proof,Proof_Poi: intermediate Proof of the toplevel goal (open list) 444%* Goal: current goal 445%* ID,Body: id and body of a kb-rule matchin Goal (if any) 446%* 447%* description: 448%* 449%* example: 450%* 451%* peculiarities: none 452%* 453%* see also: 454%* 455%*********************************************************************** 456 457solve_rule(_,_,_,_,I,A,B):- 458 functor(A,F,N), 459 functor(A1,F,N), 460 get_clause(I,A1,B,_,_), 461 unify(A,A1). 462solve_rule(D,Delta,Proof,Poi,_,A,_):- 463 Poi = [[-1,A,no_more_rules]], 464 ( D < Delta -> 465 assert(failed_proof(Proof)) 466 ; true 467 ), 468 fail. 469 470 471%*********************************************************************** 472%* 473%* predicate: gen_depth/2 474%* 475%* syntax: gen_depth(D, Delta) 476%* 477%* args: D,Delta: integers 478%* 479%* description: generates depth bound for the interative deepening 480%* theorem prover. Delta is the difference between D and 481%* the former depth (not to create duplicate proofs) 482%* 483%* example: 484%* 485%* peculiarities: none 486%* 487%* see also: 488%* 489%*********************************************************************** 490 491/***** gen_depth without maximum depth***** 492gen_depth(D, Delta) :- 493 gen_depth(3, 100, D, Delta). 494 495 496gen_depth(D, Delta, D, Delta). 497 498gen_depth(D0, _, D, Delta) :- 499 Delta1 is D0 div 2 + 1, 500 D1 is D0 + Delta1, 501 ( tag(_) -> 502 retractall(tag(_)), 503 gen_depth(D1, Delta1, D, Delta) 504 ; fail 505 ). 506*******/ 507 508 509gen_depth(D, Delta) :- % D = new depth for proofs 510 % Delta = new D - former D 511 depth_bound(N), 512 ( number(N) -> 513 ( N >= 3 -> 514 gen_depth(3, D, 3, Delta) 515 ; gen_depth(N,D,N,Delta) 516 ) 517 ; gen_depth(3, D, 3, Delta) 518 ). 519 520 521 522gen_depth(D, D, Delta, Delta). 523 524gen_depth(D0, D, _, Delta) :- 525 ( tag(_) -> 526 retractall(tag(_)), 527 Delta1 is ( D0 div 2 ) + 1, 528 D1 is D0 + Delta1, 529 depth_bound(Max), 530 ( number(Max) -> 531 ( D1 =< Max -> 532 retractall(depth_exceeded(_,_,_)) 533 ; assert(depth_exceeded),fail 534 ) 535 ; true 536 ), 537 gen_depth(D1, D, Delta1, Delta) 538 ; fail 539 ). 540 541set_proof_depth:- 542 nl,nl, 543 write('Speficy maximum depth for theorem prover (number or n for unbound proofs): '), 544 read(N), 545 retractall(depth_bound(_)), 546 assert(depth_bound(N)). 547 548 549%*********************************************************************** 550%* 551%* predicate: prove1/2 552%* 553%* syntax: prove1(+Clause, -Proof) 554%* 555%* args: Clause: clause in list form ( [H:p,L1:n,L2:n,..]) 556%* Proof: list of all literals used to prove clause 557%* 558%* description: 559%* prove1 tries to match Clause against literals in this kb, 560%* use for clause reduction wrt theta-subsumption (Plotkin). 561%* 562%* example: 563%* 564%* peculiarities: 565%* 566%* see also: Buntine,1988. Plotkin,1970. 567%* 568%*********************************************************************** 569/* 570prove1([H|T],Proof):- 571 prove1(H,HProof), 572 prove1(T,TProof), 573 append(HProof,TProof,Proof). 574prove1([],[]). 575prove1(L:S,[L:S]):- 576 member(S,[n,r]), 577 body(L,_O,_I). 578prove1(L:p,[L:p]):- 579 head(L,_O,_I). 580*/ 581 582%*********************************************************************** 583%* 584%* predicate: prove1/2 585%* 586%* syntax: prove1(+Clause, -Proof) 587%* 588%* args: Clause: clause in list form ( [H:p,L1:n,L2:n,..]) 589%* Proof: list of all literals used to prove clause 590%* 591%* description: 592%* prove1 tries to match Clause against literals in this kb, 593%* use for clause reduction wrt theta-subsumption (Plotkin). 594%* This is a more efficient version for embedding Clause in the kb: 595%* (IRENE) 596%* a list CL1 = [Lit:Sign:Litlist|_] is constructed from Clause 597%* where Litlist is the list of literals in the kb (if Sign = p, literals 598%* head(L,_,_), else body(L,_,_)) unifiable with Lit. CL1 is sorted 599%* ascendingly according to the length of Litlist. If there is an 600%* empty Litlist in CL1, prove1a fails and backtracking occurs. 601%* Else Lit is unified with a literal in Litlist (backtracking point), 602%* and the remaining list CL1 is updated. 603%* 604%* example: 605%* 606%* peculiarities: 607%* 608%* see also: Buntine,1988. Plotkin,1970. 609%* 610%*********************************************************************** 611 612prove1(CL,SProof):- 613 ini_prove1(CL,CL1), 614 prove1a(CL1,[],SProof). 615 616prove1a([],SP,SP). 617prove1a(L,_,_):- member(_:_:[],L),!,fail. 618prove1a([Lit:S:LitL|R],SProof,SP):- 619 ( ground(Lit) -> 620 prove1a(R,[Lit:S|SProof],SP) 621 ; member(Lit,LitL), 622 adapt_prove1(R,Lit,S,R1), 623 prove1a(R1,[Lit:S|SProof],SP) 624 ). 625 626ini_prove1([],[]). 627ini_prove1([Lit:S|R],R2):- 628 ini_prove1(R,R1), 629 ( S = p -> 630 mysetof(H,M^O^(head(H,M,O),\+(\+(Lit = H))),LitL) 631 ; mysetof(H,M^O^(body(H,M,O),\+(\+(Lit = H))),LitL) 632 ), 633 insert_prove1(Lit:S:LitL,R1,R2). 634 635insert_prove1(L:S:LL,[L1:S1:LL1|R],[L1:S1:LL1|R1]):- 636 length(LL,LLN),length(LL1,LL1N), 637 LLN > LL1N,!, 638 insert_prove1(L:S:LL,R,R1). 639insert_prove1(X,L,[X|L]). 640 641adapt_prove1([],_,_,[]). 642adapt_prove1([Lit:S:_|R],Lit1,S1,R1):- 643 Lit == Lit1, S == S1,!, 644 adapt_prove1(R,Lit1,S1,R1). 645adapt_prove1([Lit:S:LL|R],Lit1,S1,R2):- 646 mysetof(X,(member(X,LL),\+(\+(Lit = X))),LL1), 647 adapt_prove1(R,Lit1,S1,R1), 648 insert_prove1(Lit:S:LL1,R1,R2). 649 650 651%*********************************************************************** 652%* 653%* predicate: prove3/2 654%* 655%* syntax: prove3(+CL,-CL) 656%* 657%* args: CL: clause body in list notation 658%* 659%* description: embedd CL in skolemized body of an example clause 660%* (body/3 entries in the kb) 661%* used for absorption, saturation 662%* 663%* example: 664%* 665%* peculiarities: none 666%* 667%* see also: 668%* 669%*********************************************************************** 670 671prove3( [A|B],[ProofA|ProofB] ):- 672 prove3(A,ProofA), 673 prove3(B,ProofB). 674prove3([],[]). 675 676prove3(A:n,A:n):- 677 body(A,_,_). 678prove3(A:r,A:r):- 679 body(A,_,_). 680 681 682%*********************************************************************** 683%* 684%* predicate: prove4/3 685%* 686%* syntax: prove4(+CL,-Uncovered,-Proof) 687%* 688%* args: CL: clause in list notation 689%* Uncovered = H/M, where M in {new_head,new_body} 690%* or Uncovered = [] if all literals are covered 691%* Proof = [[Lit,N],...] where N in {head,body} 692%* 693%* description: embeds CL in skolemized example clause (head/3,body/3 entries) 694%* allows 1 uncovered literal (= the resolution literal) & returns it 695%* 696%* example: 697%* 698%* peculiarities: none 699%* 700%* see also: 701%* 702%*********************************************************************** 703 704prove4( [H|More], Uncovered, [ProofH|ProofRest]):- 705 prove4(H,Uncovered,ProofH), 706 prove4(More,Uncovered,ProofRest). 707 708 709prove4([],[],[]):-!. 710prove4([],_,[]):-!. 711prove4(H:n,_,[H,body]):- body(H,_,_). 712prove4(H:r,_,[H,body]):- body(H,_,_). 713prove4(H:p,_,[H,head]):- head(H,_,_). 714prove4(H:n,Uncovered,[]):- var(Uncovered), Uncovered = H/new_head. 715prove4(H:r,Uncovered,[]):- var(Uncovered), Uncovered = H/new_head. 716prove4(H:p,Uncovered,[]):- var(Uncovered), Uncovered = H/new_body. 717 718 719%*********************************************************************** 720%* 721%* predicate: prove5/2 722%* 723%* syntax: prove5(+HS,+RuleIDs) 724%* 725%* args: HS: skolemized clause head, RuleIDs: list of ruleIDs 726%* 727%* description: tries to infer HS from assumptions and the rules in 728%* RuleIDs 729%* 730%* example: 731%* 732%* peculiarities: none 733%* 734%* see also: 735%* 736%*********************************************************************** 737 738prove5( H, _):- assumption( H,_,_). 739prove5( true, _). 740prove5( H, RULES):- 741 get_clause(ID,H,true,_,_), 742 member(ID,RULES). 743prove5( (L1,L2), RULES):- 744 prove5(L1,RULES), 745 prove5(L2,RULES). 746prove5( H, RULES):- 747 get_clause(ID, H, B, _,_), 748 member( ID, RULES), 749 prove5(B, RULES)