1:- set_prolog_flag(print_depth,1000).    2:- set_prolog_flag(variable_names,off).    3
    4:- dynamic(count_inferences_pred/1).    5:- dynamic(trace_search_progress_pred/1).    6:- dynamic(compile_proof_printing/0).    7:- dynamic(ncalls/1).    8
    9%%% Sound unification.
   10%%%
   11%%% `add_sound_unification' transforms a clause so that its
   12%%% head has no repeated variables.  Unifying a goal with
   13%%% the clause head can then be done soundly without the occurs
   14%%% check.  The rest of the unification can then be done in
   15%%% the body of the transformed clause, using the sound `unify'
   16%%% predicate.
   17%%%
   18%%% For example,
   19%%%    p(X,Y,f(X,Y)) :- true.
   20%%% is transformed into
   21%%%    p(X,Y,f(X1,Y1)) :- unify(X,X1), unify(Y,Y1).
   22
   23add_sound_unification((Head :- Body),(Head1 :- Body1)) :-
   24        linearize(Head,Head1,[],_,true,Matches),
   25        conjoin(Matches,Body,Body1).
   26
   27linearize(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut) :-
   28        nonvar(TermIn) ->
   29                functor(TermIn,F,N),
   30                myfunctor(TermOut,F,N),
   31                linearize_args(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut,1,N);
   32        identical_member(TermIn,VarsIn) ->
   33                VarsOut = VarsIn,
   34                conjoin(MatchesIn,unify(TermIn,TermOut),MatchesOut);
   35        %true ->
   36                TermOut = TermIn,
   37                VarsOut = [TermIn|VarsIn],
   38                MatchesOut = MatchesIn.
   39
   40linearize_args(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut,I,N) :-
   41        I > N ->
   42                VarsOut = VarsIn,
   43                MatchesOut = MatchesIn;
   44        %true ->
   45                arg(I,TermIn,ArgI),
   46                linearize(ArgI,NewArgI,VarsIn,Vars1,MatchesIn,Matches1),
   47                arg(I,TermOut,NewArgI),
   48                I1 is I + 1,
   49                linearize_args(TermIn,TermOut,Vars1,VarsOut,Matches1,MatchesOut,I1,N).
   50
   51%%% Sound unification algorithm with occurs check that is called
   52%%% by code resulting from the `add_sound_unification' transformation.
   53%%% This should be coded in a lower-level language for efficiency.
   54
   55unify(X,Y) :-
   56        var(X) ->
   57                (var(Y) ->
   58                        X = Y;
   59                %true ->
   60                        functor(Y,_,N),
   61                        (N = 0 ->
   62                                true;
   63                        N = 1 ->
   64                                arg(1,Y,Y1), not_occurs_in(X,Y1);
   65                        %true ->
   66                                not_occurs_in_args(X,Y,N)),
   67                        X = Y);
   68        var(Y) ->
   69                functor(X,_,N),
   70                (N = 0 ->
   71                        true;
   72                N = 1 ->
   73                        arg(1,X,X1), not_occurs_in(Y,X1);
   74                %true ->
   75                        not_occurs_in_args(Y,X,N)),
   76                X = Y;
   77        %true ->
   78                functor(X,F,N),
   79                functor(Y,F,N),
   80                (N = 0 ->
   81                        true;
   82                N = 1 ->
   83                        arg(1,X,X1), arg(1,Y,Y1), unify(X1,Y1);
   84                %true ->
   85                        unify_args(X,Y,N)).
   86
   87unify_args(X,Y,N) :-
   88        N = 2 ->
   89                arg(2,X,X2), arg(2,Y,Y2), unify(X2,Y2),
   90                arg(1,X,X1), arg(1,Y,Y1), unify(X1,Y1);
   91        %true ->
   92                arg(N,X,Xn), arg(N,Y,Yn), unify(Xn,Yn),
   93                N1 is N - 1, unify_args(X,Y,N1).
   94
   95not_occurs_in(Var,Term) :-
   96        Var == Term ->
   97                fail;
   98        var(Term) ->
   99                true;
  100        %true ->
  101                functor(Term,_,N),
  102                (N = 0 ->
  103                        true;
  104                N = 1 ->
  105                        arg(1,Term,Arg1), not_occurs_in(Var,Arg1);
  106                %true ->
  107                        not_occurs_in_args(Var,Term,N)).
  108
  109not_occurs_in_args(Var,Term,N) :-
  110        N = 2 ->
  111                arg(2,Term,Arg2), not_occurs_in(Var,Arg2),
  112                arg(1,Term,Arg1), not_occurs_in(Var,Arg1);
  113        %true ->
  114                arg(N,Term,ArgN), not_occurs_in(Var,ArgN),
  115                N1 is N - 1, not_occurs_in_args(Var,Term,N1).
  116
  117%%% Depth-first iterative-deepening search.
  118%%%
  119%%% `add_complete_search' adds arguments DepthIn and DepthOut
  120%%% to each PTTP literal to control bounded depth-first
  121%%% search.  When a literal is called,
  122%%% DepthIn is the current depth bound.  When
  123%%% the literal exits, DepthOut is the new number
  124%%% of levels remaining after the solution of
  125%%% the literal (DepthIn - DepthOut is the number
  126%%% of levels used in the solution of the goal.)
  127%%%
  128%%% For clauses with empty bodies or bodies
  129%%% composed only of builtin functions,
  130%%% DepthIn = DepthOut.
  131%%%
  132%%% For other clauses, the depth bound is
  133%%% compared to the cost of the body.  If the
  134%%% depth bound is exceeded, the clause fails.
  135%%% Otherwise the depth bound is reduced by
  136%%% the cost of the body.
  137%%%
  138%%% p :- q , r.
  139%%% is transformed into
  140%%% p(DepthIn,DepthOut) :-
  141%%%     DepthIn >= 2, Depth1 is DepthIn - 2,
  142%%%     q(Depth1,Depth2),
  143%%%     r(Depth2,DepthOut).
  144%%%
  145%%% p :- q ; r.
  146%%% is transformed into
  147%%% p(DepthIn,DepthOut) :-
  148%%%     DepthIn >= 1, Depth1 is DepthIn - 1,
  149%%%     (q(Depth1,DepthOut) ; r(Depth1,DepthOut)).
  150
  151add_complete_search((Head :- Body),(Head1 :- Body1)) :-
  152        Head =.. L,
  153        append(L,[DepthIn,DepthOut],L1),
  154        Head1 =.. L1,
  155        (functor(Head,query,_) ->
  156                add_complete_search_args(Body,DepthIn,DepthOut,Body1);
  157        nonzero_search_cost(Body,Cost) ->
  158                add_complete_search_args(Body,Depth1,DepthOut,Body2),
  159                conjoin((DepthIn >= Cost , Depth1 is DepthIn - Cost),Body2,Body1);
  160        %true ->
  161                add_complete_search_args(Body,DepthIn,DepthOut,Body1)).
  162
  163add_complete_search_args(Body,DepthIn,DepthOut,Body1) :-
  164        Body = (A , B) ->
  165                add_complete_search_args(A,DepthIn,Depth1,A1),
  166                add_complete_search_args(B,Depth1,DepthOut,B1),
  167                conjoin(A1,B1,Body1);
  168        Body = (A ; B) ->
  169                search_cost(A,CostA),
  170                search_cost(B,CostB),
  171                (CostA < CostB ->
  172                        add_complete_search_args(A,DepthIn,DepthOut,A1),
  173                        add_complete_search_args(B,Depth1,DepthOut,B2),
  174                        Cost is CostB - CostA,
  175                        conjoin((DepthIn >= Cost , Depth1 is DepthIn - Cost),B2,B1);
  176                CostA > CostB ->
  177                        add_complete_search_args(A,Depth1,DepthOut,A2),
  178                        add_complete_search_args(B,DepthIn,DepthOut,B1),
  179                        Cost is CostA - CostB,
  180                        conjoin((DepthIn >= Cost , Depth1 is DepthIn - Cost),A2,A1);
  181                %true ->
  182                        add_complete_search_args(A,DepthIn,DepthOut,A1),
  183                        add_complete_search_args(B,DepthIn,DepthOut,B1)),
  184                disjoin(A1,B1,Body1);
  185        Body = search(Goal,Max,Min,Inc) ->
  186                PrevInc is Min + 1,
  187                add_complete_search_args(Goal,DepthIn1,DepthOut1,Goal1),
  188                DepthIn = DepthOut,
  189                Body1 = search(Goal1,Max,Min,Inc,PrevInc,DepthIn1,DepthOut1);
  190        Body = search(Goal,Max,Min) ->
  191                add_complete_search_args(search(Goal,Max,Min,1),DepthIn,DepthOut,Body1);
  192        Body = search(Goal,Max) ->
  193                add_complete_search_args(search(Goal,Max,0),DepthIn,DepthOut,Body1);
  194        Body = search(Goal) ->
  195                add_complete_search_args(search(Goal,1000000),DepthIn,DepthOut,Body1);
  196        functor(Body,search_cost,_) ->
  197                DepthIn = DepthOut,
  198                Body1 = true;
  199        builtin(Body) ->
  200                DepthIn = DepthOut,
  201                Body1 = Body;
  202        %true ->
  203                Body =.. L,
  204                append(L,[DepthIn,DepthOut],L1),
  205                Body1 =.. L1.
  206
  207nonzero_search_cost(Body,Cost) :-
  208        search_cost(Body,Cost),
  209        Cost > 0.
  210
  211%%% Search cost is computed by counting literals in the body.
  212%%% It can be given explicitly instead by including a number, as in
  213%%%   p :- search_cost(3).     (ordinarily, cost would be 0)
  214%%%   p :- search_cost(1),q,r. (ordinarily, cost would be 2)
  215%%%   p :- search_cost(0),s.   (ordinarily, cost would be 1)
  216%%%
  217%%% Propositional goals are not counted into the search cost so
  218%%% that fully propositional problems can be solved without
  219%%% deepening when iterative-deepening search is used.
  220
  221search_cost(Body,N) :-
  222        Body = search_cost(M) ->
  223                N = M;
  224        Body = (A , B) ->
  225                (A = search_cost(M) ->  % if first conjunct is search_cost(M),
  226                        N = M;          % search cost of the entire conjunction is M
  227                %true ->
  228                        search_cost(A,N1),
  229                        search_cost(B,N2),
  230                        N is N1 + N2);
  231        Body = (A ; B) ->
  232                search_cost(A,N1),
  233                search_cost(B,N2),
  234                min(N1,N2,N);
  235        builtin(Body) ->
  236                N = 0;
  237        functor(Body,_,2) ->  % zero-cost 2-ary (0-ary plus ancestor lists) predicates
  238                N = 0;        % heuristic for propositional problems
  239        %true ->
  240                N = 1.
  241
  242%%% Depth-first iterative-deepening search can be
  243%%% specified for a goal by wrapping it in a call
  244%%% on the search predicate:
  245%%%    search(Goal,Max,Min,Inc)
  246%%% Max is the maximum depth to search (defaults to a big number),
  247%%% Min is the minimum depth to search (defaults to 0),
  248%%% Inc is the amount to increment the bound each time (defaults to 1).
  249%%%
  250%%% Depth-first iterative deepening search can be
  251%%% specified inside the PTTP formula by compiling
  252%%%   query :- search(p(b,a,c),Max,Min,Inc)
  253%%% and executing
  254%%%   query.
  255%%% or directly by the user by compiling
  256%%%   query :- p(b,a,c))
  257%%% and executing
  258%%%   search(query,Max,Min,Inc).
  259%%%
  260%%% The search(Goal,Max,Min,Inc) predicate adds
  261%%% DepthIn and DepthOut arguments to its goal argument.
  262
  263search(Goal,Max,Min,Inc) :-
  264        PrevInc is Min + 1,
  265        add_complete_search_args(Goal,DepthIn,DepthOut,Goal1),
  266        (compile_proof_printing ->
  267                add_proof_recording_args(Goal1,_Proof,_ProofEnd,Goal2);
  268        %true ->
  269                Goal2 = Goal1),
  270        !,
  271        search(Goal2,Max,Min,Inc,PrevInc,DepthIn,DepthOut).
  272
  273search(Goal,Max,Min) :-
  274        search(Goal,Max,Min,1).
  275
  276search(Goal,Max) :-
  277        search(Goal,Max,0).
  278
  279search(Goal) :-
  280        search(Goal,1000000).
  281
  282%%% Actual search driver predicate.
  283%%% Note that depth-bounded execution of Goal is enabled by
  284%%% the fact that the DepthIn and DepthOut arguments of
  285%%% search are also the DepthIn and DepthOut arguments of Goal.
  286
  287search(_Goal,Max,Min,_Inc,_PrevInc,_DepthIn,_DepthOut) :-
  288        Min > Max,
  289        !,
  290        fail.
  291search(Goal,_Max,Min,_Inc,PrevInc,DepthIn,DepthOut) :-
  292        trace_search_progress_pred(P1),
  293        L1 =.. [P1,Min],
  294        call(L1),
  295        DepthIn = Min,
  296        call(Goal),
  297        DepthOut < PrevInc.   % fail if this solution was found in previous search
  298search(Goal,Max,Min,Inc,_PrevInc,DepthIn,DepthOut) :-
  299        Min1 is Min + Inc,
  300        search(Goal,Max,Min1,Inc,Inc,DepthIn,DepthOut).
  301
  302%%% Complete inference.
  303%%%
  304%%% Model elimination reduction operation and
  305%%% identical ancestor goal pruning.
  306%%%
  307%%% Two arguments are added to each literal, one
  308%%% for all the positive ancestors, one for all
  309%%% the negative ancestors.
  310%%%
  311%%% Unifiable membership is checked in the list 
  312%%% of opposite polarity to the goal
  313%%% for performing the reduction operation.
  314%%%
  315%%% Identity membership is checked in the list
  316%%% of same polarity as the goal
  317%%% for performing the ancestor goal pruning operation.
  318%%% This is not necessary for soundness or completeness,
  319%%% but is often effective at substantially reducing the
  320%%% number of inferences.
  321%%%
  322%%% The current head goal is added to the front
  323%%% of the appropriate ancestor list during the
  324%%% call on subgoals in bodies of nonunit clauses.
  325
  326add_ancestor((Head :- Body),(Head1 :- Body1)) :-
  327        functor(Head,query,_) ->
  328                Head1 = Head,
  329                add_ancestor_args(Body,[[],[]],Body1);
  330        %true ->
  331                Head =.. L,
  332                append(L,[PosAncestors,NegAncestors],L1),
  333                Head1 =.. L1,
  334                add_ancestor_args(Body,[NewPosAncestors,NewNegAncestors],Body2),
  335                (Body == Body2 ->
  336                        Body1 = Body2;
  337                negative_literal(Head) ->
  338                        NewPosAncestors = PosAncestors,
  339                        conjoin((NewNegAncestors = [Head|NegAncestors]),Body2,Body1);
  340                %true ->
  341                        NewNegAncestors = NegAncestors,
  342                        conjoin((NewPosAncestors = [Head|PosAncestors]),Body2,Body1)).
  343
  344add_ancestor_args(Body,AncestorLists,Body1) :-
  345        Body = (A , B) ->
  346                add_ancestor_args(A,AncestorLists,A1),
  347                add_ancestor_args(B,AncestorLists,B1),
  348                conjoin(A1,B1,Body1);
  349        Body = (A ; B) ->
  350                add_ancestor_args(A,AncestorLists,A1),
  351                add_ancestor_args(B,AncestorLists,B1),
  352                disjoin(A1,B1,Body1);
  353        Body =.. [search,Goal|L] ->
  354                add_ancestor_args(Goal,AncestorLists,Goal1),
  355                Body1 =.. [search,Goal1|L];
  356        builtin(Body) ->
  357                Body1 = Body;
  358        %true ->
  359                Body =.. L,
  360                append(L,AncestorLists,L1),
  361                Body1 =.. L1.
  362
  363ancestor_tests(P,N,Result) :-
  364        P == query ->
  365                Result = true;
  366        %true ->
  367                negated_functor(P,NotP),
  368                N2 is N - 2,            % N - 2 due to two ancestor-list arguments
  369                functor(Head1,P,N2),
  370                Head1 =.. [P|Args1],
  371                Head2 =.. [NotP|Args1],
  372                append(Args1,[PosAncestors,NegAncestors],Args),
  373                Head =.. [P|Args],
  374                (negative_functor(P) ->
  375                        C1Ancestors = NegAncestors, C2Ancestors = PosAncestors;
  376                %true ->
  377                        C1Ancestors = PosAncestors, C2Ancestors = NegAncestors),
  378                C1 = (Head :- identical_member(Head1,C1Ancestors), !, fail),
  379                count_inferences_pred(IncNcalls),
  380                (N2 = 0 ->              % special case for propositional calculus
  381                        conjoin((identical_member(Head2,C2Ancestors) , !),IncNcalls,V);
  382                %true ->
  383                        conjoin(unifiable_member(Head2,C2Ancestors),IncNcalls,V)),
  384                (compile_proof_printing ->
  385                        conjoin(V,infer_by(red),V1);
  386                %true ->
  387                        V1 = V),
  388                C2 = (Head :- V1),
  389                conjoin(C1,C2,Result).
  390
  391procedures_with_ancestor_tests([[P,N]|Preds],Clauses,Procs) :-
  392        procedure(P,N,Clauses,Proc1),
  393        ancestor_tests(P,N,Tests),
  394        conjoin(Tests,Proc1,Proc),
  395        procedures_with_ancestor_tests(Preds,Clauses,Procs2),
  396        conjoin(Proc,Procs2,Procs).
  397procedures_with_ancestor_tests([],_Clauses,true).
  398
  399identical_member(X,[Y|_])  :-           % run-time predicate for
  400        X == Y,                         % finding identical ancestor
  401        !.
  402identical_member(X,[_|L]) :-
  403        identical_member(X,L).
  404
  405unifiable_member(X,[Y|_]) :-            % run-time predicate for
  406        unify(X,Y).                     % finding complementary ancestor
  407unifiable_member(X,[_|L]) :-
  408        unifiable_member(X,L).
  409
  410%%% Proof Printing.
  411%%%
  412%%% Add extra arguments to each goal so that information
  413%%% on what inferences were made in the proof can be printed
  414%%% at the end.
  415
  416add_proof_recording((Head :- Body),(Head1 :- Body1)) :-
  417        Head =.. L,
  418        append(L,[Proof,ProofEnd],L1),
  419        Head1 =.. L1,
  420        add_proof_recording_args(Body,Proof,ProofEnd,Body2),
  421        (functor(Head,query,_) ->
  422                conjoin(Body2,write_proved(Proof,ProofEnd),Body1);
  423        %true ->
  424                Body1 = Body2).
  425
  426add_proof_recording_args(Body,Proof,ProofEnd,Body1) :-
  427        Body = (A , B) ->
  428                add_proof_recording_args(A,Proof,Proof1,A1),
  429                add_proof_recording_args(B,Proof1,ProofEnd,B1),
  430                conjoin(A1,B1,Body1);
  431        Body = (A ; B) ->
  432                add_proof_recording_args(A,Proof,ProofEnd,A1),
  433                add_proof_recording_args(B,Proof,ProofEnd,B1),
  434                disjoin(A1,B1,Body1);
  435        Body =.. [search,Goal|L] ->
  436                add_proof_recording_args(Goal,Proof,ProofEnd,Goal1),
  437                Body1 =.. [search,Goal1|L];
  438        Body = infer_by(X) ->
  439                Body1 = (Proof = [X|ProofEnd]);
  440        Body = fail ->
  441                Body1 = Body;
  442        builtin(Body) ->
  443                Proof = ProofEnd,
  444                Body1 = Body;
  445        %true ->
  446                Body =.. L,
  447                append(L,[Proof,ProofEnd],L1),
  448                Body1 =.. L1.
  449
  450write_proved(Proof,ProofEnd) :-
  451        write('proved by'),
  452        write_proof(Proof,ProofEnd).
  453
  454write_proof(Proof,ProofEnd) :-
  455        Proof == ProofEnd,
  456        !.
  457write_proof([X|Y],ProofEnd) :-
  458        write(' '),
  459        write(X),
  460        write_proof(Y,ProofEnd).
  461
  462%%% Negation normal form to Prolog clause translation.
  463%%% Include a literal in the body of each clause to
  464%%% indicate the number of the formula the clause came from.
  465
  466clauses((A , B),L,WffNum) :-
  467        !,
  468        clauses(A,L1,WffNum),
  469        WffNum2 is WffNum + 1,
  470        clauses(B,L2,WffNum2),
  471        conjoin(L1,L2,L).
  472clauses(A,L,WffNum) :-
  473        head_literals(A,Lits),
  474        clauses(A,Lits,L,WffNum).
  475
  476clauses(A,[Lit|Lits],L,WffNum) :-
  477        body_for_head_literal(Lit,A,Body1),
  478        (compile_proof_printing ->
  479                conjoin(infer_by(WffNum),Body1,Body);
  480        %true ->
  481                Body = Body1),
  482        clauses(A,Lits,L1,WffNum),
  483        conjoin((Lit :- Body),L1,L).
  484clauses(_,[],true,_).
  485
  486head_literals(Wff,L) :-
  487        Wff = (A :- B) ->               % contrapositives are not formed for A :- ... inputs
  488                head_literals(A,L);
  489        Wff = (A , B) ->
  490                head_literals(A,L1),
  491                head_literals(B,L2),
  492                union(L1,L2,L);
  493        Wff = (A ; B) ->
  494                head_literals(A,L1),
  495                head_literals(B,L2),
  496                union(L1,L2,L);
  497        %true ->
  498                L = [Wff].
  499
  500body_for_head_literal(Head,Wff,Body) :-
  501        Wff = (A :- B) ->
  502                body_for_head_literal(Head,A,A1),
  503                conjoin(A1,B,Body);
  504        Wff = (A , B) ->
  505                body_for_head_literal(Head,A,A1),
  506                body_for_head_literal(Head,B,B1),
  507                disjoin(A1,B1,Body);
  508        Wff = (A ; B) ->
  509                body_for_head_literal(Head,A,A1),
  510                body_for_head_literal(Head,B,B1),
  511                conjoin(A1,B1,Body);
  512        Wff == Head ->
  513                Body = true;
  514        negated_literal(Wff,Head) ->
  515                Body = false;
  516        %true ->
  517                negated_literal(Wff,Body).
  518
  519%%% predicates returns a list of the predicates appearing in a formula.
  520
  521predicates(Wff,L) :-
  522        Wff = (A :- B) ->
  523                predicates(A,L1),
  524                predicates(B,L2),
  525                union(L2,L1,L);
  526        Wff = (A , B) ->
  527                predicates(A,L1),
  528                predicates(B,L2),
  529                union(L2,L1,L);
  530        Wff = (A ; B) ->
  531                predicates(A,L1),
  532                predicates(B,L2),
  533                union(L2,L1,L);
  534        functor(Wff,search,_) ->        % list predicates in first argument of search
  535                arg(1,Wff,X),
  536                predicates(X,L);
  537        builtin(Wff) ->
  538                L = [];
  539        %true ->
  540                functor(Wff,F,N),
  541                L = [[F,N]].
  542
  543%%% procedure returns a conjunction of the clauses
  544%%% with head predicate P/N.
  545
  546procedure(P,N,Clauses,Proc) :-
  547        Clauses = (A , B) ->
  548                procedure(P,N,A,ProcA),
  549                procedure(P,N,B,ProcB),
  550                conjoin(ProcA,ProcB,Proc);
  551        (Clauses = (A :- B) , functor(A,P,N)) ->
  552                Proc = Clauses;
  553        %true ->
  554                Proc = true.
  555
  556%%% pttp is the PTTP compiler top-level predicate.
  557
  558pttp(X) :-
  559        time(pttp1(X),'Compilation').
  560
  561pttp1(X) :-
  562        nl,
  563        write('PTTP input formulas:'),
  564        apply_to_conjuncts(X,write_clause,_),
  565        nl,
  566        clauses(X,X0,1),
  567        apply_to_conjuncts(X0,add_count_inferences,X1),
  568        apply_to_conjuncts(X1,add_ancestor,X2),
  569        predicates(X2,Preds0),
  570        reverse(Preds0,Preds),
  571        procedures_with_ancestor_tests(Preds,X2,X3),
  572        apply_to_conjuncts(X3,add_sound_unification,X4),
  573        apply_to_conjuncts(X4,add_complete_search,X5),
  574        (compile_proof_printing ->
  575                apply_to_conjuncts(X5,add_proof_recording,Y);
  576        %true ->
  577                Y = X5),
  578        nl,
  579        write('PTTP output formulas:'),
  580        apply_to_conjuncts(Y,write_clause,_),
  581        nl,
  582        nl,
  583
  584        File = 'temp.prolog',                     % Quintus Prolog on Sun
  585%       File = 'darwin:>stickel>pttp>temp.prolog',% change file name for other systems
  586
  587        open(File,write,OutFile),
  588        write_clause_to_file(Y,OutFile),
  589        close(OutFile),
  590        compile(File),
  591        nl,
  592        !.
  593
  594write_clause_to_file((A,B),OutFile) :-
  595	write_clause_to_file(A,OutFile),
  596	write_clause_to_file(B,OutFile),
  597        !.
  598write_clause_to_file(A,OutFile) :-
  599	nl(OutFile),
  600	write(OutFile,A),
  601	write(OutFile,.),
  602	!.
  603
  604
  605query(M) :-                             % call query with depth bound M
  606        compile_proof_printing -> 
  607                query(M,_N,_Proof,_ProofEnd);
  608        %true ->
  609                query(M,_N).
  610
  611query :-                                % unbounded search of query
  612        query(1000000).
  613
  614%%% Utility functions.
  615
  616%%% Sometimes the `functor' predicate doesn't work as expected and
  617%%% a more comprehensive predicate is needed.  The `myfunctor'
  618%%% predicate overcomes the problem of functor(X,13,0) causing
  619%%% an error in Symbolics Prolog.  You may need to use it if
  620%%% `functor' in your Prolog system fails to construct or decompose
  621%%% terms that are numbers or constants.
  622
  623myfunctor(Term,F,N) :-
  624        nonvar(F),
  625        atomic(F),
  626        N == 0,
  627        !,
  628        Term = F.
  629myfunctor(Term,F,N) :-
  630        nonvar(Term),
  631        atomic(Term),
  632        !,
  633        F = Term,
  634        N = 0.
  635myfunctor(Term,F,N) :-
  636        functor(Term,F,N).
  637
  638nop(_).
  639
  640append([],L,L).
  641append([X|L1],L2,[X|L3]) :-
  642        append(L1,L2,L3).
  643
  644reverse([X|L0],L) :-
  645        reverse(L0,L1),
  646        append(L1,[X],L).
  647reverse([],[]).
  648
  649union([X|L1],L2,L3) :-
  650        identical_member(X,L2),
  651        !,
  652        union(L1,L2,L3).
  653union([X|L1],L2,[X|L3]) :-
  654        union(L1,L2,L3).
  655union([],L,L).
  656
  657intersection([X|L1],L2,[X|L3]) :-
  658        identical_member(X,L2),
  659        !,
  660        intersection(L1,L2,L3).
  661intersection([_X|L1],L2,L3) :-
  662        intersection(L1,L2,L3).
  663intersection([],_L,[]).
  664
  665%%% min(X,Y,Min) :-
  666%%%        X =< Y ->
  667%%%                Min = X;
  668%%%        %true ->
  669%%%                Min = Y.
  670
  671conjoin(A,B,C) :-
  672        A == true ->
  673                C = B;
  674        B == true ->
  675                C = A;
  676        A == false ->
  677                C = false;
  678        B == false ->
  679                C = false;
  680        %true ->
  681                C = (A , B).
  682
  683disjoin(A,B,C) :-
  684        A == true ->
  685                C = true;
  686        B == true ->
  687                C = true;
  688        A == false ->
  689                C = B;
  690        B == false ->
  691                C = A;
  692        %true ->
  693                C = (A ; B).
  694
  695negated_functor(F,NotF) :-
  696        name(F,L),
  697        name(not_,L1),
  698        (append(L1,L2,L) ->
  699                true;
  700        %true ->
  701                append(L1,L,L2)),
  702        name(NotF,L2).
  703
  704negated_literal(Lit,NotLit) :-
  705        Lit =.. [F1|L1],
  706        negated_functor(F1,F2),
  707        (var(NotLit) ->
  708                NotLit =.. [F2|L1];
  709        %true ->
  710                NotLit =.. [F2|L2],
  711                L1 == L2).
  712
  713negative_functor(F) :-
  714        name(F,L),
  715        name(not_,L1),
  716        append(L1,_,L).
  717
  718negative_literal(Lit) :-
  719        functor(Lit,F,_),
  720        negative_functor(F).
  721
  722apply_to_conjuncts(Wff,P,Wff1) :-
  723        Wff = (A , B) ->
  724                apply_to_conjuncts(A,P,A1),
  725                apply_to_conjuncts(B,P,B1),
  726                conjoin(A1,B1,Wff1);
  727        %true ->
  728                T1 =.. [P,Wff,Wff1],
  729                call(T1).
  730
  731write_clause(A) :-
  732        nl,
  733        write(A),
  734        write(.).
  735
  736write_clause(A,_) :-                    % 2-ary predicate can be used as
  737        write_clause(A).                % argument of apply_to_conjuncts
  738
  739%%% Inference counting is turned on by count_inferences,
  740%%% off by dont_count_inferences.
  741%%%
  742%%% Inferences are counted by retracting the current count
  743%%% and asserting the incremented count, so inference counting
  744%%% is very slow.
  745
  746count_inferences :-                     % enables compilation of inference counting
  747        retract(count_inferences_pred(_)),% this slows down the code substantially
  748        fail.
  749count_inferences :-
  750        assert(count_inferences_pred(inc_ncalls)).
  751
  752dont_count_inferences :-                % disables compilation of inference counting
  753        retract(count_inferences_pred(_)),% this is the default for acceptable performance
  754        fail.
  755dont_count_inferences :-
  756        assert(count_inferences_pred(true)).
  757
  758:- dont_count_inferences.               % default is to not count inferences
  759
  760%%% Transformation to add inference counting to a clause.
  761
  762add_count_inferences((Head :- Body),(Head :- Body1)) :-
  763        functor(Head,query,_) ->
  764                Body1 = Body;
  765        %true ->
  766                count_inferences_pred(P),
  767                conjoin(P,Body,Body1).
  768
  769clear_ncalls :-
  770        retract(ncalls(_)),
  771        fail.
  772clear_ncalls :-
  773        assert(ncalls(0)).
  774
  775inc_ncalls :-
  776        retract(ncalls(N)),
  777        N1 is N + 1,
  778        assert(ncalls(N1)),
  779        !.
  780
  781%%% Search tracing is turned on by trace_search,
  782%%% off by dont_trace_search.
  783
  784trace_search :-                         % enables search progress reports
  785        retract(trace_search_progress_pred(_)),
  786        fail.
  787trace_search :-
  788        assert(trace_search_progress_pred(write_search_progress)).
  789
  790dont_trace_search :-                    % disables search progress reports
  791        retract(trace_search_progress_pred(_)),
  792        fail.
  793dont_trace_search :-
  794        assert(trace_search_progress_pred(nop)).
  795
  796:- trace_search.                        % default is to trace searching
  797
  798write_search_progress(Level) :-
  799        ncalls(N),
  800        (N > 0 -> write(N) , write(' inferences so far.') ; true),
  801        nl,
  802        write('Begin cost '),
  803        write(Level),
  804        write(' search...  ').
  805
  806%%% Proof printing is turned on by print_proof,
  807%%% off by dont_print_proof.
  808%%%
  809%%% print_proof or dont_print_proof should be
  810%%% executed before the problem is compiled.
  811
  812print_proof :-                          % enable proof printing
  813        retract(compile_proof_printing),
  814        fail.
  815print_proof :-
  816        assert(compile_proof_printing).
  817
  818dont_print_proof :-                     % disable proof printing
  819        retract(compile_proof_printing),
  820        fail.
  821dont_print_proof.
  822
  823:- print_proof.                         % default is to print proof
  824
  825%%% A query can be timed by time(query).
  826
  827time(X) :-
  828        time(X,'Execution').
  829
  830time(X,Type) :-
  831        clear_ncalls,
  832
  833        statistics(runtime,[T1,_]),     % Quintus Prolog on Sun
  834%        T1 is get-internal-run-time,  % Common Lisp time function
  835
  836        call(X),
  837
  838        statistics(runtime,[T2,_]),     % Quintus Prolog on Sun
  839        Secs is (T2 - T1) / 1000.0,     % Quintus measures runtime in milliseconds
  840%        T2 is get-internal-run-time,  % Common Lisp time function
  841%        Secs is (T2 - T1) / 977.0,      % internal-time-units-per-second on Darwin
  842
  843        nl,
  844        write(Type),
  845        write(' time: '),
  846        ncalls(N),
  847        (N > 0 -> write(N) , write(' inferences in ') ; true),
  848        write(Secs),
  849        write(' seconds, including printing'),
  850        nl.
  851
  852%%% List of builtin predicates that can appear in clause bodies.
  853%%% No extra arguments are added for ancestor goals or depth-first
  854%%% iterative-deepening search.  Also, if a clause body is
  855%%% composed entirely of builtin goals, the head is not saved
  856%%% as an ancestor for use in reduction or pruning.
  857%%% This list can be added to as required.
  858
  859builtin(T) :-
  860        functor(T,F,N),
  861        builtin(F,N).
  862
  863builtin(!,0).
  864builtin(true,0).
  865builtin(fail,0).
  866builtin(succeed,0).
  867builtin(trace,0).
  868builtin(atom,1).
  869builtin(integer,1).
  870builtin(number,1).
  871builtin(atomic,1).
  872builtin(constant,1).
  873builtin(functor,3).
  874builtin(arg,3).
  875builtin(var,1).
  876builtin(nonvar,1).
  877builtin(call,1).
  878builtin(=,2).
  879builtin(\=,2).
  880builtin(==,2).
  881builtin(\==,2).
  882builtin(>,2).
  883builtin(<,2).
  884builtin(>=,2).
  885builtin(=<,2).
  886builtin(is,2).
  887builtin(display,1).
  888builtin(write,1).
  889builtin(nl,0).
  890builtin(infer_by,_).
  891builtin(write_proved,_).
  892builtin(search,_).
  893builtin(search_cost,_).
  894builtin(unify,_).
  895builtin(identical_member,_).
  896builtin(unifiable_member,_).
  897builtin(inc_ncalls,0).
  898
  899%%% Theorem proving examples from
  900%%%   Chang, C.L. and R.C.T. Lee.
  901%%%   Symbolic Logic and Mechanical Theorem Proving.
  902%%%   Academic Press, New York, 1973, pp. 298-305.
  903
  904%%% Note that the search driver predicate
  905%%% can be invoked by search(query) as in
  906%%% chang_lee_example8 or can be explicitly
  907%%% included in the query as in chang_lee_example2.
  908
  909chang_lee_example2 :-
  910        nl,
  911        write(chang_lee_example2),
  912        pttp((
  913                p(e,X,X),
  914                p(X,e,X),
  915                p(X,X,e),
  916                p(a,b,c),
  917                (p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
  918                (p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
  919                (query :- search(p(b,a,c)))
  920        )),
  921        time(query).
  922
  923chang_lee_example8 :-
  924        nl,
  925        write(chang_lee_example8),
  926        pttp((
  927                l(1,a),
  928                d(X,X),
  929                (p(X) ; d(g(X),X)),
  930                (p(X) ; l(1,g(X))),
  931                (p(X) ; l(g(X),X)),
  932                (not_p(X) ; not_d(X,a)),
  933                (not_d(X,Y) ; not_d(Y,Z) ; d(X,Z)),
  934                (not_l(1,X) ; not_l(X,a) ; p(f(X))),
  935                (not_l(1,X) ; not_l(X,a) ; d(f(X),X)),
  936                (query :- (p(X) , d(X,a)))
  937        )),
  938        time(search(query))