1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%%                                                                           %%
    3%%      Version:  1.00   Date: 24/04/95   File: lemma.pl                     %%
    4%% Last Version:                          File:                              %%
    5%% Changes:                                                                  %%
    6%% 04/04/95 Created                                                          %%
    7%%                                                                           %%
    8%% Purpose:                                                                  %%
    9%%                                                                           %%
   10%% Author:  Torsten Schaub                                                   %%
   11%%                                                                           %%
   12%% Usage:   prolog lemma.pl                                                  %%
   13%%                                                                           %%
   14%%                                                                           %%
   15%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   16
   17:- dynamic(dynamic_lemma/3).   18:- dynamic(static_lemma/3).   19
   20:- dynamic(lemma_handling_flag/0).   21
   22:- dynamic(lemma_mode_parameter/1).   23:- dynamic(lemma_format_parameter/1).   24:- dynamic(lemma_type_parameter/1).   25
   26%%% ----------------------------------------------------------------------
   27%%% LEMMA CONFIGURATION
   28
   29lemma_configuration :-
   30	nl,write('LEMMA CONFIGURATION:'),nl,nl,
   31	
   32	write("Lemma handling"),
   33	write(' = '),
   34	(lemma_handling_flag ->
   35	    write(on),
   36	    nl,nl,
   37	
   38	    write(lemma_format),
   39	    write(' = '),
   40	    (lemma_format_parameter(P), write(P),write(' '),fail ; write('.')),
   41	    nl,
   42	    
   43	    write(lemma_mode),
   44	    write(' = '),
   45	    (lemma_mode_parameter(M),   write(M),write(' '),fail ; write('.')),
   46	    nl,
   47	    
   48	    write(lemma_type),
   49	    write(' = '),
   50	    (lemma_type_parameter(T),   write(T),write(' '),fail ; write('.')),
   51	    nl;
   52	%true ->
   53	    write(off)),
   54	nl.
   55
   56%%% Lemma handling is turned on by lemma_handling,
   57%%% off by no_lemma_handling.
   58
   59lemma_handling :-                          % enable lemma handling
   60        retract(lemma_handling_flag),
   61        fail.
   62lemma_handling :-
   63        assert(lemma_handling_flag).
   64
   65no_lemma_handling :-                       % disable lemma handling
   66        retract(lemma_handling_flag),
   67        fail.
   68no_lemma_handling.
   69
   70%%% Lemma mode indicates the usage of dynamic, static
   71%%% or dystatic modes of lemmas
   72%%% depending on lemma_mode_parameter(dynamic),lemma_mode_parameter(static), 
   73%%% and lemma_mode_parameter(dystatic)
   74
   75lemma_mode(dynamic) :-                          % enable DYNAMIC lemmas
   76        retract(lemma_mode_parameter(_)),
   77        fail.
   78lemma_mode(dynamic) :-
   79        assert(lemma_mode_parameter(dynamic)).
   80
   81lemma_mode(dystatic) :-                         % enable DYSTATIC  lemmas
   82        retract(lemma_mode_parameter(_)),
   83        fail.
   84lemma_mode(dystatic) :-
   85        assert(lemma_mode_parameter(dystatic)).
   86
   87lemma_mode(static) :-                           % enable STATIC  lemmas
   88        retract(lemma_mode_parameter(_)),
   89        fail.
   90lemma_mode(static) :-
   91        assert(lemma_mode_parameter(static)).
   92
   93%%% Dynamic lemma handling is alternatively turned on by dynamic_lemmas,
   94%%% off by no_dynamic_lemmas.
   95
   96dynamic_lemmas :- lemma_mode(dynamic).                       % enable  DYNAMIC lemma handling
   97
   98add_dynamic_lemmas :-                                        % add     DYNAMIC lemma handling
   99        retract(lemma_mode_parameter(dynamic)),
  100        fail.
  101add_dynamic_lemmas :-
  102        assert(lemma_mode_parameter(dynamic)).
  103
  104no_dynamic_lemmas :-                                         % disable DYNAMIC lemma handling
  105        retract(lemma_mode_parameter(dynamic)),
  106        fail.
  107no_dynamic_lemmas.
  108
  109%%% Static lemma handling is alternatively turned on by static_lemmas,
  110%%% off by no_static_lemmas.
  111
  112static_lemmas :- lemma_mode(static).                        % enable  STATIC lemma handling
  113
  114add_static_lemmas :-                                        % add     STATIC lemma handling
  115        retract(lemma_mode_parameter(static)),
  116        fail.
  117add_static_lemmas :-
  118        assert(lemma_mode_parameter(static)).
  119
  120no_static_lemmas :-                                         % disable STATIC lemma handling
  121        retract(lemma_mode_parameter(static)),
  122        fail.
  123no_static_lemmas.
  124
  125%%% Dystatic lemma handling is alternatively turned on by dystatic_lemmas,
  126%%% off by no_dystatic_lemmas.
  127%%% dystatic lemmas are static lemmas stemming from dynamic ones
  128
  129dystatic_lemmas :- lemma_mode(dystatic).                    % enable  DYSTATIC lemma handling
  130
  131add_dystatic_lemmas :-                                      % add     DYSTATIC lemma handling
  132        retract(lemma_mode_parameter(dystatic)),
  133        fail.
  134add_dystatic_lemmas :-
  135        assert(lemma_mode_parameter(dystatic)).
  136
  137no_dystatic_lemmas :-                                       % disable DYSTATIC lemma handling
  138        retract(lemma_mode_parameter(dystatic)),
  139        fail.
  140no_dystatic_lemmas.
  141
  142%%% some macros for easier lemma configuration.
  143
  144lemma_flag :- lemma_mode_parameter(X).
  145dynamic_lemma_flag  :- lemma_mode_parameter(dynamic).
  146static_lemma_flag   :- lemma_mode_parameter(static).
  147dystatic_lemma_flag :- lemma_mode_parameter(dystatic).
  148
  149no_lemmas :- no_dynamic_lemmas,no_static_lemmas,no_dystatic_lemmas.
  150
  151%%% Lemma type indicates the location of the lemmatization predicates
  152%%%   DELTA lemmas are attached to rules stemming from default rules
  153%%%                ( Head =.. [gamma|-] or infer_by(default(_)) )
  154%%%   OMEGA lemmas are attached to rules stemming from classical rules
  155%%%                ( infer_by(extension(_) )
  156%%% depends on lemma_type_parameter(delta),lemma_type_parameter(omega), 
  157%%% and lemma_type_parameter(all)
  158
  159lemma_type(delta) :-                          % enable DELTA lemmas
  160        retract(lemma_type_parameter(_)),
  161        fail.
  162lemma_type(delta) :-
  163        assert(lemma_type_parameter(delta)).
  164
  165lemma_type(omega) :-                          % enable OMEGA  lemmas
  166        retract(lemma_type_parameter(_)),
  167        fail.
  168lemma_type(omega) :-
  169        assert(lemma_type_parameter(omega)).
  170
  171lemma_type(all) :-                            % enable ALL  lemmas
  172        retract(lemma_type_parameter(_)),
  173        fail.
  174lemma_type(all) :-
  175        assert(lemma_type_parameter(delta)),
  176        assert(lemma_type_parameter(omega)).
  177
  178%%% Delta lemma handling is alternatively added  by delta_lemmas,
  179%%% disabled by no_delta_lemmas.
  180
  181add_delta_lemmas :-                                        % add     DELTA lemma handling
  182        retract(lemma_type_parameter(delta)),
  183        fail.
  184add_delta_lemmas :-
  185        assert(lemma_type_parameter(delta)).
  186
  187no_delta_lemmas :-                                         % disable DELTA lemma handling
  188        retract(lemma_type_parameter(delta)),
  189        fail.
  190no_delta_lemmas.
  191
  192%%% Omega lemma handling is alternatively added  by omega_lemmas,
  193%%% disabled by no_omega_lemmas.
  194
  195add_omega_lemmas :-                                        % add     OMEGA lemma handling
  196        retract(lemma_type_parameter(omega)),
  197        fail.
  198add_omega_lemmas :-
  199        assert(lemma_type_parameter(omega)).
  200
  201no_omega_lemmas :-                                         % disable OMEGA lemma handling
  202        retract(lemma_type_parameter(omega)),
  203        fail.
  204no_omega_lemmas.
  205
  206%%% Lemma format indicates the usage of unit or disjunctive lemmas
  207%%% depending on lemma_format_parameter(unit) and lemma_format_parameter(disj)
  208
  209lemma_format(unit) :-                          % enable UNIT lemmas
  210        retract(lemma_format_parameter(_)),
  211        fail.
  212lemma_format(unit) :-
  213        assert(lemma_format_parameter(unit)).
  214
  215lemma_format(disj) :-                          % enable DISJUNCTIVE  lemmas
  216        retract(lemma_format_parameter(_)),
  217        fail.
  218lemma_format(disj) :-
  219        assert(lemma_format_parameter(disj)).
  220
  221%%% SETTINGS for LEMMA HANDLING
  222%%%
  223
  224:- compile(lemma_config).  225
  226%%% ----------------------------------------------------------------------
  227%%% LEMMA GENERATION during COMPILATION
  228
  229%%% Add extra arguments to each goal so that information
  230%%% on what inferences were made in the proof can be printed
  231%%% at the end.
  232
  233add_lemmatization((Head :- Body),(Head1 :- Body1)) :-
  234	lemma_handling_flag,
  235	!,
  236        Head =.. L,
  237        append(L,[ProofOut,ProofEnd],L1),
  238        Head1 =.. L1,
  239        add_lemmatization_args(Body,Proof,ProofEnd,Body2,Lemma),
  240        (Lemma = true ->
  241	    Body1 = Body2,
  242	    ProofOut = Proof;
  243	 add_lemmatization_p(Head :- Body) ->
  244	    Lemmatization =.. [lemmatize,Lemma,Proof,ProofOut,ProofEnd],
  245	    conjoin(Body2,Lemmatization,Body1),
  246	    verbose("Lemmatization ":Lemma);
  247        %true ->
  248             Body1 = Body2,
  249             ProofOut = Proof).
  250add_lemmatization((Head :- Body),(Head :- Body)).
  251
  252add_lemmatization_p(Head :- Body) :-
  253	lemma_flag,
  254	!,
  255	(functor(Head,query,_) -> fail;
  256         functor(Head,alpha,_) -> fail;
  257	 functor(Head,gamma,_) -> lemma_type_parameter(delta);
  258	 true ->                  lemma_type_parameter(omega)).
  259         
  260add_lemmatization_args(Body,Proof,ProofEnd,Body1,Lemma) :-
  261        Body = (A , B) ->
  262                add_lemmatization_args(A,Proof,Proof1,A1,L1),
  263                add_lemmatization_args(B,Proof1,ProofEnd,B1,L2),
  264                conjoin(A1,B1,Body1),
  265                conjoin(L1,L2,Lemma);
  266        Body = (A ; B) ->
  267                add_lemmatization_args(A,Proof,ProofEnd,A1,L1),
  268                add_lemmatization_args(B,Proof,ProofEnd,B1,L2),
  269                disjoin(A1,B1,Body1),
  270                conjoin(L1,L2,Lemma);
  271        Body = infer_by(X) ->
  272	        add_lemmatization_inference(X,Proof,ProofEnd,Record,Lemma),
  273		conjoin(Body,Record,Body1);
  274        Body =.. [search,Goal|L] ->
  275                add_lemmatization_args(Goal,Proof,ProofEnd,Goal1),
  276                Body1 =.. [search,Goal1|L],
  277                Lemma = true;
  278        Body = fail ->
  279                Body1 = Body,
  280                Lemma = true;
  281        builtin(Body) ->
  282                Proof = ProofEnd,
  283                Body1 = Body,
  284                Lemma = true;
  285        %true ->
  286                Body =.. L,
  287                append(L,[Proof,ProofEnd],L1),
  288                Body1 =.. L1,
  289                Lemma = true.
  290
  291add_lemmatization_inference(Inference,Proof,ProofEnd,Record,Lemma) :-
  292	Inference = reduction(_) ->
  293	    /* ancestor test */
  294	    Lemma = true,
  295            (lemma_type_parameter(omega) ->
  296		Record = (Proof = [Inference|ProofEnd]);
  297	    %true ->
  298		Proof = ProofEnd,
  299		Record = true);
  300        Inference = extension(_) ->
  301            /* omega rule */
  302	    Proof = ProofEnd,
  303	    Record = true,
  304	    (lemma_type_parameter(omega) ->
  305		Lemma = Inference;
  306	    %true ->
  307		Lemma = true);
  308	Inference = default(_) ->
  309	    /* delta rule */
  310	    Lemma = Inference,
  311	    ((static_lemma_flag;dystatic_lemma_flag) ->
  312		Record = (Proof = [Inference|ProofEnd]);
  313	    %true ->
  314		Proof = ProofEnd,
  315		Record =true);
  316	Inference = static_lemma(_) ->
  317	    /* static lemma test (implicit (dy)static_lemma_flag)*/
  318	    Record = (Proof = [Inference|ProofEnd]),
  319	    Lemma = true;
  320	Inference = dynamic_lemma(_) ->
  321	    /* dynamic lemma test */
  322	    Lemma = true,
  323	    ((static_lemma_flag;dystatic_lemma_flag) ->
  324		Record = (Proof = [Inference|ProofEnd]);
  325	    %true ->
  326		Proof = ProofEnd,
  327		Record =true);
  328	%true ->
  329            /* unit. etc */
  330	    Proof = ProofEnd,
  331	    Record = true,
  332	    Lemma = true.
  333
  334
  335lemma_tests_p(P,N) :-
  336	lemma_handling_flag, (dynamic_lemma_test_p(P,N) ; static_lemma_test_p(P,N)).
  337
  338dynamic_lemma_test_p(P,N) :-
  339	(dynamic_lemma_flag;dystatic_lemma_flag),
  340	!,
  341	(P == query -> fail;
  342         P == alpha -> fail;
  343	 P == gamma -> lemma_type_parameter(delta);
  344	 true       -> lemma_type_parameter(omega)).
  345
  346static_lemma_test_p(P,N) :-
  347	(static_lemma_flag;dystatic_lemma_flag),
  348	!,
  349	(P == query -> fail;
  350         P == alpha -> fail;
  351	 P == gamma -> lemma_type_parameter(delta);
  352	 true       -> lemma_type_parameter(omega)).
  353
  354lemma_tests(P,N,Result) :-
  355	lemma_handling_flag,
  356	lemma_tests_p(P,N),     % for avoiding problems with query/0
  357	!,
  358	N3 is N - 3,            % N - 3 due to 3 ancestor-lists
  359	functor(Head3,P,N3),
  360	Head3 =.. [P|Args1],
  361	append(Args1,[_,_,_],Args),
  362	Head =.. [P|Args],
  363	
  364	(dynamic_lemma_test_p(P,N) ->
  365	    dynamic_lemma_test(Head,Head3,DynamicLemmaBody);
  366	%true ->
  367	    DynamicLemmaBody=true),
  368
  369	(static_lemma_test_p(P,N) ->
  370	    static_lemma_test(Head,Head3,StaticLemmaBody);
  371	%true ->
  372	    StaticLemmaBody=true),
  373
  374	conjoin(DynamicLemmaBody,StaticLemmaBody,Result).
  375lemma_tests(_,_,true).
  376
  377dynamic_lemma_test(Head,Head3,Test) :-
  378	lemma_format_parameter(unit) ->
  379	     ((static_lemma_flag;dystatic_lemma_flag) ->
  380		 Body = (infer_by(dynamic_lemma(Head3:Assumptions)),
  381		         dynamic_lemma(Head3,false,Assumptions)) ;
  382	     %true ->
  383        	 Body = (infer_by(dynamic_lemma(Head3)),
  384		         dynamic_lemma(Head3,false,[]))),
  385	     Test = (Head :- Body,!); /* REQUIRES FULLY INSTANTIIATED SUBGOALS */
  386	lemma_format_parameter(disj) ->
  387	%true              ->
  388	        not_yet_implemented.
  389		          
  390static_lemma_test(Head,Head3,Test) :-
  391	lemma_format_parameter(unit) ->
  392        	Body = (infer_by(static_lemma(Head3:Assumptions)),
  393		        static_lemma(Head3,false,Assumptions),
  394			justification(Assumptions)),
  395		Test = (Head :- Body);
  396	lemma_format_parameter(disj) ->
  397	%true              ->
  398	        not_yet_implemented.
  399
  400%%% ----------------------------------------------------------------------
  401%%% LEMMA UTILIZATION during RUN-TIME
  402
  403lemmatize(default(N:(Gamma :- _)),Proof,ProofOut,ProofEnd) :-
  404	verbose("Using static lemma code: ":lemmatize),
  405        !,
  406        remove_reductions(Proof,ProofOut),
  407        default_assumptions(ProofOut,ProofEnd,Ass),
  408        lemmatize_dynamically(gamma(N,Gamma),false,Ass).
  409%        lemmatize_statically(gamma(N,Gamma),false,Ass).
  410lemmatize(extension(_N:Goal),Proof,ProofOut,ProofEnd) :-
  411	verbose("Using static lemma code: ":lemmatize),
  412        !,
  413        skim_reductions(Goal,Proof,ProofOut,ProofEnd,Ancs),
  414        default_assumptions(ProofOut,ProofEnd,Ass),
  415        lemmatize_dynamically(Goal,Ancs,Ass).
  416%        lemmatize_statically(Goal,Ancs,Ass).
  417lemmatize(_Lemmatization,_Proof,_ProofOut,_ProofEnd) :-
  418        error_in_lemmatize.
  419
  420lemmatize_statically(Goal,Ancestors,Assumptions) :-
  421        static_lemma(Goal,Ancestors,Assumptions),            % UNIFY, ==, ... ???
  422        !.
  423lemmatize_statically(Goal,Ancestors,Assumptions) :-
  424        assert(static_lemma(Goal,Ancestors,Assumptions)),
  425        verbose(static_lemma(Goal,Ancestors,Assumptions)).
  426
  427lemmatize_dynamically(Goal,Ancestors,_) :-
  428        dynamic_lemma(Goal,Ancestors,_),                        % UNIFY, ==, ... ???
  429        !.
  430%lemmatize_dynamically(Goal,Ancestors,[]) :-               <=== only if cases below
  431%        !,
  432%        assert(dynamic_lemma(Goal,Ancestors,[])),
  433%        lemmatize_statically(Goal,Ancestors,[]),
  434%        verbose(dynamic_lemma(Goal,Ancestors)).
  435lemmatize_dynamically(Goal,Ancestors,Assumptions) :-
  436        (assert(dynamic_lemma(Goal,Ancestors,Assumptions)),
  437         verbose(activated:(dynamic_lemma(Goal,Ancestors,[Assumptions])));
  438         retract(dynamic_lemma(Goal,Ancestors,Assumptions)),
  439         verbose(deactivated:(dynamic_lemma(Goal,Ancestors,[Assumptions]))),
  440%         lemmatize_statically(Goal,Ancestors,Assumptions), <=== only if cases below
  441         !,
  442         fail).
  443
  444% No check for ProofEnd, since default(...) should be contained
  445% Because only invoked in case of default inference
  446
  447remove_reductions([default(X)|Proof],[default(X)|Proof]) :- 
  448        !.
  449remove_reductions([static_lemma(X)|Proof],[static_lemma(X)|ProofOut]) :- 
  450        !,
  451        remove_reductions(Proof,ProofOut).
  452remove_reductions([dynamic_lemma(X)|Proof],[dynamic_lemma(X)|ProofOut]) :- 
  453	/* ==> when using static lemmas <== */
  454        !,
  455        remove_reductions(Proof,ProofOut).
  456remove_reductions(Proof,ProofOut) :-
  457        Proof = [_|RestProof],
  458        remove_reductions(RestProof,ProofOut).
  459
  460skim_reductions(_Goal,Proof,Proof,ProofEnd,false) :-
  461        Proof == ProofEnd,
  462        !.
  463skim_reductions(_Goal,Proof,Proof,_ProofEnd,false) :-
  464        Proof = [default(_)|_],
  465        !.
  466skim_reductions(Goal,[reduction(Anc)|Proof],Proof1,ProofEnd,Ancs) :-
  467        Goal == Anc,
  468        skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs),
  469        !.
  470skim_reductions(Goal,[reduction(Anc)|Proof],[reduction(Anc)|Proof1],ProofEnd,Ancs1) :-
  471        !,
  472        skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs),
  473        disjoin1(Anc,Ancs,Ancs1).
  474skim_reductions(Goal,[static_lemma(X)|Proof],[static_lemma(X)|Proof1],ProofEnd,Ancs) :-
  475        skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs).
  476skim_reductions(Goal,[dynamic_lemma(X)|Proof],[dynamic_lemma(X)|Proof1],ProofEnd,Ancs) :-
  477	/* ==> when using static lemmas <== */
  478        skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs).
  479
  480%%% ----------------------------------------------------------------------
  481%%% default_assumptions/3 
  482%%%         extracts all neccessary default assunptions from a proof
  483%%%
  484
  485default_assumptions(Proof,ProofEnd,[]) :-
  486        Proof == ProofEnd,
  487        !.
  488default_assumptions([default(_N:(_ :- _ : Just))|Proof],ProofEnd,Assumptions) :-
  489        !,
  490        default_assumptions(Proof,ProofEnd,Justs),
  491        combine_clauses(Just,Justs,Assumptions).
  492default_assumptions([static_lemma(_  : Just)|Proof],ProofEnd,Assumptions) :-
  493        !,
  494        default_assumptions(Proof,ProofEnd,Justs),
  495        combine_clauses(Just,Justs,Assumptions).
  496default_assumptions([dynamic_lemma(_ : Just)|Proof],ProofEnd,Assumptions) :-
  497	/* ==> when using static lemmas <== */
  498        !,
  499        default_assumptions(Proof,ProofEnd,Justs),
  500        combine_clauses(Just,Justs,Assumptions).
  501default_assumptions([_|Proof],ProofEnd,Wff) :-
  502        default_assumptions(Proof,ProofEnd,Wff).
  503
  504%%% A is supposed to be a literal
  505%%% disjoin2 removes A from B; results in C
  506
  507disjoin1(A,B,C) :-
  508        disjoin2(A,B,C1),
  509        disjoin(A,C1,C).
  510
  511disjoin2(A,(B ; C),D) :-
  512        !,
  513        disjoin2(A,B,B1),
  514        disjoin2(A,C,C1),
  515        disjoin(B1,C1,D).
  516disjoin2(A,B,false) :-
  517        A == B,
  518        !.
  519disjoin2(_,B,B).
  520
  521
  522%%% ----------------------------------------------------------------------
  523%%% SOME helpful IO-Routines
  524
  525write_lemmas(File) :-   
  526        concatenate(File,'.lem',LFile),
  527        open(LFile,write,LStream),
  528        !,
  529        (static_lemma(X,Y,Z),
  530         write_clauses(LStream,static_lemma(X,Y,Z)),
  531         fail;
  532         close(LStream)).
  533
  534show_lemmas :-  
  535        show_dynamic_lemmas,fail;
  536        nl,show_static_lemmas.
  537
  538show_dynamic_lemmas :- 
  539        (dynamic_lemma(X,Y,Z),
  540         write(dynamic_lemma(X,Y,Z)),
  541         nl,
  542         fail;
  543         true).
  544show_static_lemmas :-
  545        (static_lemma(X,Y,Z),
  546         write(static_lemma(X,Y,Z)),
  547         nl,
  548         fail;
  549         true).
  550
  551remove_lemmas :-
  552        remove_static_lemmas,
  553        remove_dynamic_lemmas.
  554remove_dynamic_lemmas :-
  555        retract_all(dynamic_lemma(_,_,_)).
  556remove_static_lemmas :-
  557        retract_all(static_lemma(_,_,_))