/******************************************************************/
/* EBG.PRO                                                        */
/* Different meta-interpreters for Mitchell's explanation-based   */
/* generalisation and partial evaluation                          */
/******************************************************************/
/*
    Copyright (c) 1988 Thomas Hoppe
    This program is free software; you can redistribute it and/or
    modify it under the terms of the GNU General Public License
    Version 1 as published by the Free Software Foundation.
*/
/******************************************************************/
/*  reference   : Explanation-Based Generalisation as Resolution  */
/*                Theorem Proving, Smadar T. Kedar-Cabelli, L.    */
/*                Thorne McCharty, Proceedings of the Fourth      */
/*                International Workshop on Machine Learning,     */
/*                Irvine, Morgan Kaufmann Publishers, California, */
/*                1987                                            */
/*                                                                */
/*                Explanation-Based Generalisation = Partial      */
/*                Evaluation, van Harmelen, F., Bundy, A.,        */
/*                Research Note, AI 36, 1988.                     */
/******************************************************************/

/******************************************************************/
/*                                                                */
/*  call        : prove_1 (+GOAL)                                 */
/*                                                                */
/*  arguments   : GOAL  = instantiated goal for a proof           */
/*                                                                */
/*  properties  : backtrackable                                   */
/*                                                                */
/******************************************************************/
/* prove_1 implements a PROLOG meta-interpreter, which succeds if */
/* GOAL is deducible from a PROLOG program.                       */
/* In opposite to the literature the last clause is necessary to  */
/* handle PROLOG built-in predicates corret.                      */
/******************************************************************/
prove_1((HEAD,REST)) :-
     !, prove_1(HEAD), prove_1(REST) .
prove_1(FACT) :-
     clause1(FACT,true) .
prove_1(GOAL) :-
     clause1(GOAL,PREMISSES), prove_1(PREMISSES) .
prove_1(GOAL) :-
     call(GOAL) .

/******************************************************************/
/*                                                                */
/*  call        : prove_2 (+GOAL,-PROOF)                          */
/*                                                                */
/*  arguments   : GOAL  = instantiated goal for a proof           */
/*                PROOF = proof tree for GOAL                     */
/*                                                                */
/*  properties  : backtrackable                                   */
/*                                                                */
/******************************************************************/
/* prove_2 is the extention of prove_1 to deliver the PROOF for   */
/* the GOAL, if GOAL is deducible from a PROLOG program.          */
/* In opposite to the literature the last clause is necessary to  */
/* handle PROLOG built-in predicates corret.                      */
/* On backtracking it gives the next possible prove.              */
/******************************************************************/
prove_2((HEAD,REST),PROOF) :-
     !, prove_2(HEAD,HEAD_PROOF), prove_2(REST,REST_PROOF),
       append(HEAD_PROOF,REST_PROOF,PROOF) .
prove_2(FACT,[FACT]) :-
     clause1(FACT,true) .
prove_2(GOAL,PROOF) :-
     clause1(GOAL,PREMISSES), not(PREMISSES == true),
       prove_2(PREMISSES,PREM_PROOF),
       append([GOAL],[PREM_PROOF],PROOF) .
/*
prove_2(GOAL,[GOAL]) :-
     call(GOAL) .
*/
/******************************************************************/
/*                                                                */
/*  call        : prove_3 (+GOAL,-PROOF)                          */
/*                                                                */
/*  arguments   : GOAL  = instantiated goal for a proof           */
/*                PROOF = proof tree for GOAL                     */
/*                                                                */
/*  properties  : backtrackable                                   */
/*                                                                */
/******************************************************************/
/* prove_3 is an extention of prove_2 to deliver generalized      */
/* PROOFS for the GOAL, if GOAL is deducible from a pure PROLOG   */
/* program.                                                       */
/* The call 'not (not clause(FACT,true))' is a special PROLOG     */
/* trick, which succeds if 'clause(FACT,true)' holds, without     */
/* instanciating GOAL.                                            */
/* A sublist of length 1 in the PROOF denotes a fact, which has   */
/* to be instanciated to fulfill the proof.                       */
/* The first element of a list is the subtree goal.               */
/* On backtracking it gives the next possible prove path.         */
/******************************************************************/
prove_3((HEAD,REST),PROOF) :-
     !, prove_3(HEAD,HEAD_PROOF), prove_3(REST,REST_PROOF),
       append(HEAD_PROOF,REST_PROOF,PROOF) .
prove_3(FACT,[FACT]) :-
     not (not clause1(FACT,true)) .
prove_3(GOAL,PROOF) :-
     clause1(GOAL,PREMISSES), not(PREMISSES == true),
       prove_3(PREMISSES,PREM_PROOF),
       append([GOAL],[PREM_PROOF],PROOF) .
/*
prove_3(GOAL,[GOAL]) .
*/
/******************************************************************/
/*                                                                */
/*  call        : prove_4 (+GOAL,-FACTS)                          */
/*                                                                */
/*  arguments   : GOAL  = uninstantiated goal for a proof         */
/*                FACTS = List of FACTS which must hold for a     */
/*                        proof of GOAL                           */
/*                                                                */
/*  properties  : backtrackable                                   */
/*                                                                */
/******************************************************************/
/* prove_4 is an extention of prove_3 to delivers the generalized */
/* FACTS that must be true for a proof of GOAL, if GOAL is        */
/* deducible from a pure PROLOG program.                          */
/* With this predicat a partial evaluation of the theory according*/
/* to the GOAL is possible                                        */
/* On backtracking it gives the next partial evaluation.          */
/******************************************************************/
prove_4((HEAD;REST),PROOF) :- 
     !, (prove_4(HEAD,PROOF); prove_4(REST,PROOF)) . 
prove_4((HEAD,REST),PROOF) :- 
     !, prove_4(HEAD,HEAD_PROOF), prove_4(REST,REST_PROOF), 
       append(HEAD_PROOF,REST_PROOF,PROOF) .
prove_4(FACT,[FACT]) :- 
     not sys(FACT), not (not clause(FACT,true)) .
prove_4(GOAL,PROOF) :- 
     not sys(GOAL), clause(GOAL,_), !,
     clause1(GOAL,PREMISSES), not(PREMISSES == true),
     prove_4(PREMISSES,PROOF) .
prove_4(GOAL,[GOAL]) .

/******************************************************************/
/*                                                                */
/*  call        : prove_5 (+GOAL,-PROOF,-FACTS)                   */
/*                                                                */
/*  arguments   : GOAL  = uninstantiated goal for a proof         */
/*                PROOF = proof tree for GOAL                     */
/*                FACTS = List of FACTS which must hold for a     */
/*                        proof of GOAL                           */
/*                                                                */
/*  properties  : backtrackable                                   */
/*                                                                */
/******************************************************************/
/* prove_5 is a combination of prove_3 and prove_4 to delivers the*/
/* generalized FACTS that must be true for a proof of GOAL and the*/
/* proof path, if GOAL is deducible from a pure PROLOG program.   */
/* So one can get the information which predicates must be        */
/* instantiated to a particular prove path.                       */
/* On backtracking it gives the next possible prove path and the  */
/* predicats that must be instanciated.                           */
/******************************************************************/
prove_5((HEAD,REST),[PROOF_HEAD|PROOF_REST],LIST) :- 
     !, prove_5(HEAD,PROOF_HEAD,PROOF_LIST1), 
       prove_5(REST,PROOF_REST,PROOF_LIST2), 
       append(PROOF_LIST1,PROOF_LIST2,LIST) .
prove_5(FACT,[FACT],[FACT]) :- 
     not (not clause1(FACT,true)) .
prove_5(GOAL,[GOAL,PROOF],LIST) :- 
     clause1(GOAL,PREMISSES), not(PREMISSES==true),
       prove_5(PREMISSES,PROOF,LIST) .
prove_5(GOAL,[GOAL],[GOAL]) .

/******************************************************************/
/*                                                                */
/*  call        : prove_6 (+GOAL1,+GOAL2,-FACTS)                  */
/*                                                                */
/*  arguments   : GOAL1 = instantiated goal for a paticular proof */
/*                GOAL2 = generalized goal                        */
/*                FACTS = List of FACTS which must hold for a     */
/*                        proof of GOAL                           */
/*                                                                */
/*  properties  : backtrackable                                   */
/*                                                                */
/******************************************************************/
/* prove_6 is an extention of prove_4 to handle the operationality*/
/* criterion mentioned by Mitchell/Keller/Kedar-Cabelli (1986).   */
/* It delivers the generalized FACTS that must be true for a      */
/* paticular proof of GOAL1, if GOAL1 is deducible from a PROLOG  */
/* program.                                                       */
/* On backtracking it gives the next possible prove path.         */
/******************************************************************/
prove_6((HEAD,REST),(GEN_HEAD,GEN_REST),LIST) :- 
     !, prove_6(HEAD,GEN_HEAD,LIST1), 
       prove_6(REST,GEN_REST,LIST2), append(LIST1,LIST2,LIST) .
prove_6(GOAL,GEN_GOAL,[GEN_GOAL]) :- 
     operational(GOAL), ! .
prove_6(GOAL,GEN_GOAL,LIST) :- 
     not operational(GOAL), clause(GEN_GOAL,GEN_PREMISSES), 
       copy((GEN_GOAL:-GEN_PREMISSES),(GOAL:-PREMISSES)), 
       prove_6(PREMISSES,GEN_PREMISSES,LIST) .

/******************************************************************/
/*                                                                */
/*  call        : listify (LIST,PREMISSES)                        */
/*                                                                */
/*  arguments   : LIST      = normal PROLOG list                  */
/*                PREMISSES = normal PROLOG and-concatenated      */
/*                            premisse_list                       */
/*                                                                */
/*  properties  : backtrackable, symmetric                        */
/*                                                                */
/******************************************************************/
/* listify builds a PROLOG and-cocatenated premisse list out of   */
/* every normal list, respecively vice versa.                     */
/* One predicat must be instantiated.                             */
/******************************************************************/
listify([H],H) .
listify([H|R],(H,S)) :- 
     listify(R,S) .

/******************************************************************/
/*                                                                */
/*  call        : copy (+TERM1,-TERM2)                            */
/*                                                                */
/*  arguments   : TERM1 = normal PROLOG term                      */
/*                TERM2 = normal PROLOG term                      */
/*                                                                */
/******************************************************************/
/* copy makes copy's of every PROLOG-Term, with the special       */
/* database trick to ensure that new variables are generated in   */
/* the output term.                                               */
/******************************************************************/
copy(TERM1,TERM2) :- 
/*	inst(TERM1,TERM2), */
	asserta(internal(TERM1)), retract(internal(TERM2)),
	! .

/******************************************************************/
/*                                                                */
/*  call        : operational (+TERM)                             */
/*                                                                */
/*  arguments   : TERM = normal PROLOG term                       */
/*                                                                */
/******************************************************************/
/* operational is an predicat for the decision of operaionality   */
/* in EBL-based algorithms. It's definition must be changed       */
/* depending on the operationality criterion's of a particular    */
/* implementation.                                                */
/******************************************************************/

clause1(X,true):-operational(X),!.
clause1(X,Y):-clause(X,Y).

/* The built-in predicates are operational */
operational(X is Y):- /* X is Y,*/ !.
operational(X > Y):- /* X>Y,*/ !.
operational(X < Y):- /* X<Y,*/ !.
operational(X >= Y):- /* X>=Y,*/ !.
operational(X =< Y):- /* X=<Y,*/ !.

/* The facts are olso operational */
operational(A) :-
     clause(A,true) .

sys(_ is _).
sys(_ > _).
sys(_ < _).
sys(_ >= _).
sys(_ =< _).

/******************************************************************/
/*                                                                */
/*  call        : ebg (GOAL,RULE)                                 */
/*                                                                */
/*  arguments   : GOAL = a goal which is to be proven             */
/*                RULE = a generalized rule for the proof         */
/*                                                                */
/******************************************************************/
/* ebg is a predicate which first proves a goal to find a         */
/* solution, and afterwards it takes the solution and generates a */
/* rule out of the proof tree. The solution is returned as a      */
/* generalisation for the prove tree.                             */
/******************************************************************/

ebg(GOAL,RULE) :-
     functor(GOAL,F,N), functor(COPY,F,N),
     call(GOAL), prove_6(GOAL,COPY,ZWERG1),
       listify(ZWERG1,ZWERG2), RULE = (COPY :- ZWERG2) .
