1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%%                                                                           %%
    3%%      Version:  1.00   Date: 15/03/98   File: defaults.pl
    4%% Last Version:                          File:                              %%
    5%% Changes:                                                                  %%
    6%% 18/03/95 Created                                                          %%
    7%% 14/07/96 added configuration utilities
    8%% 15/03/98 added pttp config and optional proof printing
    9%%                                                                           %%
   10%% Purpose:                                                                  %%
   11%%                                                                           %%
   12%% Author:  Torsten Schaub                                                   %%
   13%%                                                                           %%
   14%% Usage:   prolog defaults.pl                                               %%
   15%%                                                                           %%
   16%%                                                                           %%
   17%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   18
   19:- ensure_loaded(base).   20:- ensure_loaded(pttp).   21:- ensure_loaded(builtin).   22:- ensure_loaded(model).   23:- ensure_loaded(io).   24:- ensure_loaded(db).   25:- ensure_loaded(herbrand).   26:- ensure_loaded(hooks).   27:- ensure_loaded(lemma).   28:- ensure_loaded(xray_config).   29
   30%%% ----------------------------------------------------------------------
   31%%% XRay COMPILATION (patches pttp)
   32
   33%%% Negation normal form/Defaults to Prolog clause translation.
   34%%% Include a literal in the body of each clause to
   35%%% indicate the number of the formula the clause came from.
   36
   37clauses((A , B),L,WffNum) :-
   38        !,
   39        clauses(A,L1,WffNum),
   40        WffNum2 is WffNum + 1,
   41        clauses(B,L2,WffNum2),
   42        conjoin(L1,L2,L).
   43clauses( (Gamma :- Alpha : Beta) , L , WffNum ) :-
   44	!,
   45	clauses((Gamma :- gamma(WffNum,Gamma)),L1,WffNum),
   46	clauses((alpha(WffNum,Alpha) :- Alpha),L2,WffNum),
   47	conjoin(L1,L2,L3),
   48	conjoin(Gamma,Beta,C0),                             % ConDL-specific
   49	cnf(C0,C1),
   50	make_matrix(C1,C2),
   51	matrix_reduction(C2,Justification),
   52	(delta_ordering(compatibility>admissibility) ->
   53	    conjoin(justification(Justification),
   54	            alpha(WffNum,Alpha),
   55		    Body);
   56	%true ->
   57	    conjoin(alpha(WffNum,Alpha),
   58		    justification(Justification),
   59	            Body)),
   60	(compile_proof_printing ->
   61	    Record = infer_by(default(WffNum:(Gamma :- Alpha : Justification)));
   62	%true ->
   63	    Record = true),
   64	conjoin(Record,Body,Body1),
   65	DRule= (gamma(WffNum,Gamma) :- Body1),
   66	conjoin(DRule,L3,L).
   67
   68clauses(A,L,WffNum) :-
   69        head_literals(A,Lits),
   70        clauses(A,Lits,L,WffNum).
   71
   72clauses(A,[Lit|Lits],L,WffNum) :-
   73        body_for_head_literal(Lit,A,Body1),
   74        ((compile_proof_printing,Body1 = true) ->
   75                Record = infer_by(unit(WffNum:Lit));
   76         compile_proof_printing ->
   77                Record = infer_by(extension(WffNum:Lit));
   78        %true ->
   79		Record = true),
   80	conjoin(Record,Body1,Body),
   81        clauses(A,Lits,L1,WffNum),
   82        conjoin((Lit :- Body),L1,L).
   83clauses(_,[],true,_).
   84
   85%%% This patches the original predicate
   86%%%
   87%%%
   88
   89add_ancestor((Head :- Body),(Head1 :- Body1)) :-
   90        functor(Head,query,_) ->
   91                Head1 = Head,
   92                add_ancestor_args(Body,[[],[],[]],Body1);
   93	functor(Head,gamma,_) ->                      
   94                Head =.. L,                             
   95                append(L,[_,_,Defaults],L1),                             
   96                Head1 =.. L1,                                   
   97                add_ancestor_args(Body,[[],[],NewDefaults],Body2),
   98		conjoin((NewDefaults = [Head|Defaults]),Body2,Body1); 
   99	functor(Head,alpha,_) ->                      
  100                Head =.. L,                             
  101                append(L,[_,_,Defaults],L1),                             
  102                Head1 =.. L1,                                   
  103                add_ancestor_args(Body,[[],[],Defaults],Body1); 
  104        %true ->
  105                Head =.. L,
  106                append(L,[PosAncestors,NegAncestors,Defaults],L1),
  107                Head1 =.. L1,
  108                add_ancestor_args(Body,[NewPosAncestors,NewNegAncestors,Defaults],Body2),
  109                (Body == Body2 ->
  110                        Body1 = Body2;
  111                negative_literal(Head) ->
  112                        NewPosAncestors = PosAncestors,
  113                        conjoin((NewNegAncestors = [Head|NegAncestors]),Body2,Body1);
  114                %true ->
  115                        NewNegAncestors = NegAncestors,
  116                        conjoin((NewPosAncestors = [Head|PosAncestors]),Body2,Body1)).
  117
  118
  119ancestor_tests(P,N,Result) :-
  120        P == query ->
  121                Result = true;
  122	P == gamma ->
  123		Head = gamma(DefaultID,DefaultConseq,_,_,Defaults),
  124		Default = gamma(DefaultID,DefaultConseq),
  125		Result = (Head :- identical_member(Default,Defaults), !, fail);
  126	P == alpha ->
  127		Result = true;          % ??? <== Please, VERIFY !
  128        %true ->
  129                negated_functor(P,NotP),
  130                N3 is N - 3,            % N - 3 due to 3 ancestor-lists
  131                functor(Head1,P,N3),
  132                Head1 =.. [P|Args1],
  133                Head2 =.. [NotP|Args1],
  134                append(Args1,[PosAncestors,NegAncestors,_],Args),
  135                Head =.. [P|Args],
  136                (negative_functor(P) ->
  137                        C1Ancestors = NegAncestors, 
  138			C2Ancestors = PosAncestors;
  139                %true ->
  140                        C1Ancestors = PosAncestors, 
  141			C2Ancestors = NegAncestors),
  142                C1 = (Head :- identical_member(Head1,C1Ancestors), !, fail),
  143                count_inferences_pred(IncNcalls),
  144                (N3 = 0 ->              % special case for propositional calculus
  145                        conjoin((identical_member(Head2,C2Ancestors) , !),IncNcalls,V);
  146                %true ->
  147                        conjoin(unifiable_member(Head2,C2Ancestors),IncNcalls,V)),
  148                (compile_proof_printing ->
  149                        conjoin(V,infer_by(reduction(Head2)),V1);
  150                %true ->
  151                        V1 = V),
  152                C2 = (Head :- V1),
  153                conjoin(C1,C2,Result).
  154
  155
  156procedures_with_tests([[P,N]|Preds],Clauses,Procs) :-
  157        procedure(P,N,Clauses,Proc0),
  158
  159        ancestor_tests(P,N,TestsA),
  160	lemma_tests(P,N,TestsL),
  161	conjoin(TestsA,TestsL,Tests),
  162
  163	phook_tests(P,N,Tests,Proc0,ProcP),
  164
  165        procedures_with_tests(Preds,Clauses,ProcsPs),
  166        conjoin(ProcP,ProcsPs,Procs).
  167procedures_with_tests([],_Clauses,true).
  168
  169
  170%%% Consistency checking.
  171%%%
  172%%% Add extra arguments to each goal so that information
  173%%% on what assumptions were made in the proof can be checked
  174%%% at each step/the end.
  175%%%
  176%%% I suppose Wff has to be replaced by cmm(Model,ModelStructure) ...
  177%%% [all this is a quick copy of add_proof_recording ...]
  178
  179add_consistency_checking((Head :- Body),(Head1 :- Body1)) :-
  180        functor(Head,query,_) ->
  181                Head1 = Head,
  182		conjoin(model_initialization(MM0),Body,Body2),
  183		add_consistency_checking_args(Body2,MM0,MMOut,Body1);
  184        %true ->
  185		Head =.. L,
  186		append(L,[MMIn,MMOut],L1),
  187		Head1 =.. L1,
  188		add_consistency_checking_args(Body,MMIn,MMOut,Body1).
  189
  190add_consistency_checking_args(Body,MMIn,MMOut,Body1) :-
  191        Body = (A , B) ->
  192                add_consistency_checking_args(A,MMIn,MMIn1,A1),
  193                add_consistency_checking_args(B,MMIn1,MMOut,B1),
  194                conjoin(A1,B1,Body1);
  195        Body = (A ; B) ->
  196                add_consistency_checking_args(A,MMIn,MMOut,A1),
  197                add_consistency_checking_args(B,MMIn,MMOut,B1),
  198                disjoin(A1,B1,Body1);
  199        Body =.. [search,Goal|L] ->
  200                add_consistency_checking_args(Goal,MMIn,MMOut,Goal1), % ???
  201                Body1 =.. [search,Goal1|L];
  202        Body = justification(X) ->
  203		Body1 = compatible(X,MMIn,MMOut);
  204        Body = fail ->
  205                Body1 = Body;
  206        builtin(Body) ->
  207                MMIn = MMOut,
  208                Body1 = Body;
  209        %true ->
  210                Body =.. L,
  211                append(L,[MMIn,MMOut],L1),
  212                Body1 =.. L1.
  213
  214add_model_structure(WffI,Q,C,WffO) :-
  215	WffI = (A , B) ->
  216                add_model_structure(A,Q,C,A1),
  217                add_model_structure(B,Q,C,B1),
  218		conjoin(A1,B1,WffO);
  219        WffI = (A ; B) ->
  220                add_model_structure(A,Q,C,A1),
  221                add_model_structure(B,Q,C,B1),
  222		disjoin(A1,B1,WffO);
  223        WffI = (A :- B) ->
  224                add_model_structure(B,Q,C,B1),
  225		WffO = (A :- B1);
  226	WffI = model_initialization(Var) ->
  227	        combine_clauses(Q,C,Matrix),
  228		WffO = model_initialization(Matrix,Var);
  229        %true ->
  230	        WffO = WffI.
  231
  232classical_clauses(WffI,WffO) :-
  233        WffI = (A , B) ->
  234                classical_clauses(A,A1),
  235                classical_clauses(B,B1),
  236		conjoin(A1,B1,WffO);
  237        WffI = (A ; B) ->
  238                classical_clauses(A,A1),
  239                classical_clauses(B,B1),
  240		disjoin(A1,B1,WffO);
  241        WffI = (A :- B) ->                        % ??? (special case query elim. TS Apr04)
  242	        WffO = true;
  243        builtin(WffI) ->
  244                WffO = true;
  245        %true ->
  246	        WffI = WffO.
  247
  248query_clause(WffI,WffO) :-
  249        WffI = (A , B) ->
  250	        (query_clause(A,WffO);
  251                 query_clause(B,WffO));
  252        WffI = (A ; B) ->
  253                (query_clause(A,WffO);
  254                 query_clause(B,WffO));
  255        WffI = (A :- B) ->
  256	        (A = query ->
  257                      classical_clauses(B,WffO);
  258		 %true ->
  259                      fail);
  260        %true ->
  261	        fail.
  262
  263query(M) :-                             % call query with depth bound M
  264	(compile_complete_search, compile_proof_printing , lemma_handling_flag) ->
  265	        query(M,_N,_LemProof,_LemProofEnd,_Proof,_ProofEnd);
  266        (compile_complete_search, (compile_proof_printing ; lemma_handling_flag)) -> 
  267                query(M,_N,_Proof,_ProofEnd);
  268        compile_complete_search ->
  269                query(M,_N).
  270
  271query :-                                % unbounded search of query
  272        (compile_complete_search ->
  273	    query(1000000);
  274	%true ->
  275	    ((compile_proof_printing , lemma_handling_flag) ->
  276	         query(_LemProof,_LemProofEnd,_Proof,_ProofEnd);
  277	     (compile_proof_printing ; lemma_handling_flag) -> 
  278		 query(Proof,_ProofEnd);
  279             %true ->
  280		 query)).
  281	    
  282
  283
  284%%% ----------------------------------------------------------------------
  285%%% XRay: THE ACTUAL COMPILATION PROCEDURES
  286%%%
  287
  288xray(Name) :-
  289	read_kb(Name,KB),
  290	dpttp(Name,KB).
  291	
  292
  293dpttp(Name,X) :-
  294        time(dpttp1(X,Y:Z),'Compilation Phase I'),
  295	time(dpttp2(Name,Y:Z),'Compilation Phase II'),
  296	time(dpttp3(Name),'Compilation Phase III').
  297
  298dpttp(X) :-
  299	Name = 'temp',
  300	dpttp(Name,X).
  301
  302dpttp1(X,Y:C) :-
  303        nl,
  304        write('XRay input formulas:'),
  305        apply_to_conjuncts(X,write_clause,_),
  306        nl,
  307
  308	constants(X,H),
  309	(H = [] ->
  310	    nl,write('Empty Herbrand universe.'),nl;
  311	 %true ->
  312	    nl,write('Herbrand universe':H),nl),
  313
  314	classical_clauses(X,C0),
  315	cnf(C0,C1),
  316	make_matrix(C1,C2),
  317	instantiation(C2,H,C3),
  318	matrix_reduction(C3,C),
  319
  320        (verbose_flag ->
  321	     nl,
  322	     write('Classical output formulas:'),
  323	     apply_to_list(C,write_clause,_),
  324	     nl;
  325	%true ->
  326	     true),
  327
  328	dpttp1(X,C,Y:C).
  329
  330dpttp1(X,C,Y:C) :- 
  331	query_clause(X,Q0),
  332	variables(Q0,Vars),
  333	(Vars=[] ->
  334	         cnf(Q0,Q1),
  335		 make_matrix(Q1,Q2),
  336		 matrix_reduction(Q2,Q),
  337
  338		 XQ=X;
  339	%true ->
  340		 Q = [],
  341
  342		 apply_to_conjuncts(X,add_answer_preds,XQ)),
  343
  344        (verbose_flag ->
  345	     nl,
  346	     write('Query formula:'),
  347	     apply_to_conjuncts(Q0,write_clause,_),
  348	     nl,
  349	     write('      compiled:'),
  350	     apply_to_list(Q,write_clause,_),
  351	     nl,nl;
  352	%true ->
  353	     true),
  354
  355	dpttp1(XQ,Q,C,Y:C).
  356
  357dpttp1(X,Q,C,Y:C) :- 
  358        clauses(X,XC,1),
  359
  360	constants(X,H),
  361	(H = [] ->
  362	    XH=true,
  363	    X0=XC;
  364	 %true ->
  365	    herbrand_preds(H,XH),
  366	    apply_to_conjuncts(XC,add_herbrand_preds,X0)),
  367
  368        apply_to_conjuncts(X0,add_count_inferences,X1),
  369        apply_to_conjuncts(X1,add_ancestor,X2),
  370        predicates(X2,Preds0),
  371        reverse(Preds0,Preds),
  372	procedures_with_tests(Preds,X2,X3),
  373	/* all contrapositives available */
  374        apply_to_conjuncts(X3,add_sound_unification,X4),
  375	apply_to_conjuncts(X4,add_consistency_checking,X5),
  376        (compile_complete_search ->
  377	    apply_to_conjuncts(X5,add_complete_search,X6);
  378	%true ->
  379	    X5=X6),
  380	apply_to_conjuncts(X6,add_lemmatization,XL), /* relies on 'infer_by */
  381	(compile_proof_printing ->
  382                apply_to_conjuncts(XL,add_proof_recording,X7);
  383	%true ->
  384                X7 = XL),
  385	add_model_structure(X7,Q,C,X8),
  386
  387	apply_to_conjuncts(X8,add_body_hooks,XD),
  388
  389	apply_to_conjuncts(X,prolog_clause,XP),
  390	conjoin(XP,XD,XR),
  391
  392	conjoin(XH,XR,Y),
  393
  394        (verbose_flag -> 
  395	     nl,
  396	     write('XRay output formulas:'),
  397	     apply_to_conjuncts(Y,write_clause,_),
  398	     nl;
  399	%true ->
  400	     true),
  401	!.
  402
  403dpttp1(X) :-
  404	dpttp1(X,_).
  405
  406dpttp2(Name,Y:Z) :-
  407        nl,
  408        write('XRay writing compiled clauses ... '),
  409        write_ckb(Name,Y),
  410	write_cmm(Name,Z),
  411	write('done.'),
  412	!.
  413
  414dpttp2(Y:Z) :-
  415	Name = 'temp',
  416	dpttp2(Name,Y:Z).
  417
  418dpttp3(Name) :-
  419	nl,
  420        write('XRay compiling clauses ... '),
  421        compile_ckb(Name),
  422	write('done.'),
  423        nl,
  424        write('XRay compiling query ... '),
  425        compile_query(Name),
  426	write('done.'),
  427        nl,
  428        !.
  429dpttp3 :-
  430	Name = 'temp',
  431	dpttp3(Name)