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)