1%:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).
    2:- module(mpred_pttp_static,[]).    3%:- endif.
    4
    5:- ensure_loaded(library(pfc_lib)).    6:- ensure_loaded(library('pfc2.0'/'mpred_header.pi')).    7:- '$set_source_module'(baseKB).    8
    9:- 
   10 %swi_module(mpred_pttp_statics,[ 
   11    % pttp1/2,
   12      op(400,fy,-),    % negation
   13      op(500,xfy,&),   % conjunction
   14      op(600,xfy,v),   % disjunction
   15      op(650,xfy,=>),  % implication
   16      op(680,xfy,<=>), % equivalence
   17      op( 500, fy, ~),    % negation
   18      op( 500, fy, all),  % universal quantifier
   19      op( 500, fy, ex),   % existential quantifier
   20  %    op( 500,xfy, :),
   21       % nnf/4,
   22       !.   23
   24/*
   25       pttp_tell_wid/2,
   26       pttp_test/2,
   27       search/7,
   28       do_pttp_test/1,
   29       timed_call/2,
   30       expand_input_proof/2,
   31       contract_output_proof/2
   32        ]).
   33*/
   34
   35
   36
   37%%% ****h* PTTP/PTTP
   38%%% COPYRIGHT
   39%%%   Copyright (c) 1988-2003 Mark E. Stickel, SRI International, Menlo Park, CA 94025  USA
   40%%% 
   41%%%   Permission is hereby granted, free of charge, to any person obtaining a
   42%%%   copy of this software and associated documentation files (the "Software"),
   43%%%   to deal in the Software without restriction, including without limitation
   44%%%   the rights to use, copy, modify, merge, publish, distribute, sublicense,
   45%%%   and/or sell copies of the Software, and to permit persons to whom the
   46%%%   Software is furnished to do so, subject to the following conditions:
   47%%% 
   48%%%   The above copyright notice and this permission notice shall be included
   49%%%   in all copies or substantial portions of the Software.
   50%%% 
   51%%%   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
   52%%%   EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
   53%%%   MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
   54%%%   IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
   55%%%   CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
   56%%%   TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
   57%%%   SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
   58%%% DESCRIPTION
   59%%%  
   60%%%      A Prolog Technology Theorem Prover
   61%%%  
   62%%%               Mark E. Stickel
   63%%%  
   64%%%   Prolog is not a full theorem prover
   65%%%   for three main reasons:
   66%%%  
   67%%%     It uses an unsound unification algorithm without
   68%%%     the occurs check.
   69%%%  
   70%%%     Its inference system is complete for Horn
   71%%%     clauses, but not for more general formulas.
   72%%%  
   73%%%     Its unbounded depth-first search strategy
   74%%%     is incomplete.
   75%%%  
   76%%%   Also, it cannot display the proofs it finds.
   77%%%  
   78%%%   The Prolog Technology Theorem Prover (PTTP)
   79%%%   overcomes these limitations by
   80%%%  
   81%%%     transforming clauses so that head literals have
   82%%%     no repeated variables and unification without the
   83%%%     occurs check is valid; remaining unification
   84%%%     is done using complete unification with the
   85%%%     occurs check in the body;
   86%%%  
   87%%%     adding contrapositives of clauses (so that
   88%%%     any literal, not just a distinguished head
   89%%%     literal, can be resolved on) and the model-
   90%%%     elimination procedure reduction rule that
   91%%%     matches goals with the negations of their
   92%%%     ancestor goals;
   93%%%  
   94%%%     using a sequence of bounded depth-first searches
   95%%%     to pttp prove a theorem;
   96%%%  
   97%%%     retaining information on what formulas are
   98%%%     used for each inference so that the proof
   99%%%     can be printed.
  100%%%  
  101%%%   This version of PTTP translates first-order
  102%%%   predicate calculus formulas written in a Prolog-like
  103%%%   notation into Prolog code.  The resulting code
  104%%%   is then compiled and executed.
  105%%%  
  106%%%   PTTP commands:
  107%%%  
  108%%%     pttp_assert(formula) - translates the first-order formula
  109%%%       (normally a conjunction of formulas) into Prolog
  110%%%       and compiles it
  111%%%
  112%%%     pttp_prove(formula) - tries to pttp prove a formula
  113%%%
  114%%%   Look at the description of these functions
  115%%%   and the examples for more details on how
  116%%%   pttp_assert and pttp_prove should be used.
  117%%%   For more information on PTTP, consult
  118%%%     Stickel, M.E.  A Prolog technology theorem prover:
  119%%%     implementation by an extended Prolog compiler.
  120%%%     Journal of Automated Reasoning 4, 4 (1988), 353-380.
  121%%%     and
  122%%%     Stickel, M.E.  A Prolog technology theorem prover:
  123%%%     a new exposition and implementation in Prolog.
  124%%%     Technical Note 464, Artificial Intelligence Center,
  125%%%     SRI International, Menlo Park, California, June 1989.
  126%%%
  127%%%
  128%%%
  129%%%   Several arguments are added to each predicate:
  130%%%   PosAncestors is list of positive ancestor goals
  131%%%   NegAncestors is list of negative ancestor goals
  132%%%   DepthIn is depth bound before goal is solved
  133%%%   DepthOut will be set to remaining depth bound after goal is solved
  134%%%   ProofIn is dotted-pair difference list of proof so far
  135%%%   ProofOut will be set to list of steps of proof so far after goal is solved
  136%%%  
  137%%%
  138%%%
  139%%%   Depth-first iterative-deepening search.
  140%%%
  141%%%   PTTP adds arguments DepthIn and DepthOut
  142%%%   to each PTTP literal to control bounded depth-first
  143%%%   search.  When a literal is called,
  144%%%   DepthIn is the current depth bound.  When
  145%%%   the literal exits, DepthOut is the new number
  146%%%   of levels remaining after the solution of
  147%%%   the literal (DepthIn - DepthOut is the number
  148%%%   of levels used in the solution of the goal.)
  149%%%
  150%%%   For clauses with empty bodies or bodies
  151%%%   composed only of pttp_builtin functions,
  152%%%   DepthIn = DepthOut.
  153%%%
  154%%%   For other clauses, the depth bound is
  155%%%   compared to the cost of the body.  If the
  156%%%   depth bound is exceeded, the clause fails.
  157%%%   Otherwise the depth bound is reduced by
  158%%%   the cost of the body.
  159%%%
  160%%%   p :- q , r.
  161%%%   is transformed into
  162%%%   p(DepthIn,DepthOut) :-
  163%%%       DepthIn >= 2, Depth1 is DepthIn - 2,
  164%%%       q(Depth1,Depth2),
  165%%%       r(Depth2,DepthOut).
  166%%%
  167%%%   p :- q ; r.
  168%%%   is transformed into
  169%%%   p(DepthIn,DepthOut) :-
  170%%%       DepthIn >= 1, Depth1 is DepthIn - 1,
  171%%%       (q(Depth1,DepthOut) ; r(Depth1,DepthOut)).
  172%%%
  173%%%
  174%%%
  175%%%   Complete inference.
  176%%%
  177%%%   Model elimination reduction operation and
  178%%%   identical ancestor goal pruning.
  179%%%
  180%%%   Two arguments are added to each literal, one
  181%%%   for all the positive ancestors, one for all
  182%%%   the negative ancestors.
  183%%%
  184%%%   Unifiable membership is checked in the list 
  185%%%   of opposite polarity to the goal
  186%%%   for performing the reduction operation.
  187%%%
  188%%%   Identity membership is checked in the list
  189%%%   of same polarity as the goal
  190%%%   for performing the ancestor goal pruning operation.
  191%%%   This is not necessary for soundness or completeness,
  192%%%   but is often effective at substantially reducing the
  193%%%   number of inferences.
  194%%%
  195%%%   The current head goal is added to the front
  196%%%   of the appropriate ancestor list during the
  197%%%   call on subgoals in bodies of nonunit clauses.
  198%%%
  199%%%
  200%%%
  201%%%   Proof Printing.
  202%%%
  203%%%   Add extra arguments to each goal so that information
  204%%%   on what inferences were made in the proof can be printed
  205%%%   at the end.
  206%%% ***
  207%%% ****f* PTTP/pttp
  208%%% DESCRIPTION
  209%%%   pttp is the PTTP compiler top-level predicate.
  210%%%   Its argument is a conjunction of formulas to be compiled.
  211%%% SOURCE
  212
  213
  214
  215%%% ***
  216
  217%%% ****if* PTTP/linearize
  218%%% DESCRIPTION
  219%%%   Prolog's unification operation is unsound for first-order
  220%%%   reasoning because it lacks the occurs check that would
  221%%%   block binding a variable to a term that contains the
  222%%%   variable and creating a circular term.  However, Prolog's
  223%%%   unification algorithm is sound and the occurs check is
  224%%%   unnecessary provided the terms being unified have no
  225%%%   variables in common and at least one of the terms has
  226%%%   no repeated variables.  A Prolog fact or rule head will
  227%%%   not have variables in common with the goal.  The linearize
  228%%%   transformation rewrites a fact or rule so that the fact
  229%%%   or rule head has no repeated variables and Prolog unification
  230%%%   can be used safely.  The rest of the unification can then
  231%%%   be done in the body of the transformed clause, using
  232%%%   the sound unify predicate.
  233%%%
  234%%%   For example,
  235%%%      p(X,Y,f(X,Y)) :- true.
  236%%%   is transformed into
  237%%%      p(X,Y,f(X1,Y1)) :- unify(X,X1), unify(Y,Y1).
  238%%% SOURCE
  239
  240linearize(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut):- linearize(unify, TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut).
  241
  242linearize(Pred, TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut) :-
  243	is_ftNonvar(TermIn) ->
  244		functor(TermIn,F,N),
  245		pttp_functor(TermOut,F,N),
  246		linearize_args(Pred,TermIn,TermOut,VarsIn,VarsOut,
  247		               MatchesIn,MatchesOut,1,N);
  248	identical_member_special(TermIn,VarsIn) ->
  249		((VarsOut = VarsIn,
  250                UNIFY =.. [Pred,TermIn,TermOut],
  251		conjoin_pttp(MatchesIn,UNIFY,MatchesOut)));
  252	%true ->
  253	      ((  TermOut = TermIn,
  254		VarsOut = [TermIn|VarsIn],
  255		MatchesOut = MatchesIn)).
  256
  257linearize_args(Pred,TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut,I,N) :-
  258	I > N ->
  259		VarsOut = VarsIn,
  260		MatchesOut = MatchesIn;
  261	%true ->
  262		arg(I,TermIn,ArgI),
  263		linearize(Pred,ArgI,NewArgI,VarsIn,Vars1,MatchesIn,Matches1),
  264		arg(I,TermOut,NewArgI),
  265		I1 is I + 1,
  266		linearize_args(Pred,TermIn,TermOut,Vars1,VarsOut,Matches1,MatchesOut,I1,N).
  267%%% ***
  268%%% ****if* PTTP/unify
  269%%% DESCRIPTION
  270%%%   Prolog's unification operation is unsound for first-order
  271%%%   reasoning because it lacks the occurs check that would
  272%%%   block binding a variable to a term that contains the
  273%%%   variable and creating a circular term.  Thus, PTTP
  274%%%   must provide a sound unfication algorithm with the occurs
  275%%%   check.
  276%%%
  277%%%   unify(X,Y) is similar to Prolog's X=Y, except that operations
  278%%%   like unify(X,f(X)) fail rather than create circular terms.
  279%%% SOURCE
  280
  281unify(X,Y) :- unify_with_occurs_check(X,Y).
  282
  283unify_cheaper(X,Y) :- compound(X),compound(Y),!,
  284		functor(X,F1,N),
  285		functor(Y,F2,N),
  286
  287                same_functor(F1,F2),
  288		(N = 1 ->
  289			arg(1,X,X1), arg(1,Y,Y1), unify(X1,Y1);
  290		%true ->
  291			unify_args(X,Y,N)).
  292
  293unify_cheaper(X,Y) :- unify_with_occurs_check(X,Y),!.
  294
  295same_functor(F1,F2):- ( F1=F2 -> true ; simular_functors(F1,F2)).
  296
  297simular_functors(F1,F2):-fail,F1=F2.
  298
  299unify_args(X,Y,N) :-
  300	N = 2 ->
  301		arg(2,X,X2), arg(2,Y,Y2), unify(X2,Y2),
  302		arg(1,X,X1), arg(1,Y,Y1), unify(X1,Y1);
  303	%true ->
  304		arg(N,X,Xn), arg(N,Y,Yn), unify(Xn,Yn),
  305		N1 is N - 1, unify_args(X,Y,N1).
  306
  307
  308%%% ***
  309
  310
  311constrain_args_pttp(_P,[AR,GS]):-!,dif(AR,GS).
  312constrain_args_pttp(_,[P,AR,GS]):-P\=d,P\=p,P\=l,!,dif(AR,GS).
  313constrain_args_pttp(_,_).
  314
  315argument_type_checking(HF,HeadArgs,constrain_args(HF,HeadArgs)):-current_predicate(constrain_args/2).
  316argument_type_checking(HF,HeadArgs,constrain_args_pttp(HF,HeadArgs)):-current_predicate(constrain_args_pttp/2).
  317argument_type_checking(_,_,true).
  318
  319:- meta_predicate pretest_call(0).  320pretest_call(C):-call(C).
  321
  322
  323
  324
  325%%% ***
  326%%% ****if* PTTP/unifiable_member
  327%%% DESCRIPTION
  328%%%   unifiable_member(X,L) succeeds each time X is unifiable with an
  329%%%   element of the list L
  330%%% SOURCE
  331
  332unifiable_member(X,[Y|L]) :- unify(X,Y); unifiable_member(X,L).
  333
  334unifiable_member_cheaper(X,[Y|L]) :- unify_cheaper(X,Y); unifiable_member_cheaper(X,L).
  335
  336
  337%%% ***
  338%%% ****if* PTTP/identical_member_special
  339%%% DESCRIPTION
  340%%%   identical_member_special(X,L) succeeds iff X is an element of the list L
  341%%%   it does not use unification during element comparisons
  342%%% SOURCE
  343
  344% from memberchk_eq(X,L).
  345
  346identical_member_cheaper(X,[Y|L]) :- unify_cheaper(X,Y); identical_member_cheaper(X,L).
  347
  348identical_member_special_loop_check(X,L):- 1 is random(9),!,unifiable_member(X,L).
  349identical_member_special_loop_check(X,L):-identical_member_special(X,L).
  350
  351identical_member_special(X,[Y|Ys]) :-
  352	(   X == Y
  353	->  true
  354	;   identical_member_special(X,Ys)
  355	).
  356
  357%%% ***
  358
  359%%% ****if* PTTP/write_proof
  360%%% DESCRIPTION
  361%%%   write_proof prints the proof that PTTP finds
  362%%% SOURCE
  363
  364write_proof(Proof) :-
  365   must_det_l((
  366	write('Proof:'),
  367	nl,
  368	proof_length(Proof,Len),
  369	write('length = '),
  370	write(Len),
  371	write(', '),
  372	proof_depth(Proof,Depth),
  373	write('depth = '),
  374	write(Depth),
  375	nl,
  376	write('Goal#  Wff#  Wff Instance'),
  377	nl,
  378	write('-----  ----  ------------'),
  379	add_proof_query_line(Proof,Proof2),
  380	process_proof(Proof2,0,Proof1),
  381	write_proof1(Proof1),
  382	nl,
  383	write('Proof end.'))).
  384
  385write_proof1([]).
  386write_proof1([[LineNum,X,Head,Depth,Subgoals]|Y]) :-
  387	nl,
  388	write_indent_for_number(LineNum),
  389	write('['),
  390	write(LineNum),
  391	write(']  '),
  392	write_indent_for_number(X),
  393	write(X),
  394	write('   '),
  395	write_proof_indent(Depth),
  396	write(Head),
  397	(Subgoals = [] ->
  398		true;
  399	%true ->
  400		write(' :- '),
  401		write_proof_subgoals(Subgoals)),
  402	write(.),
  403	write_proof1(Y).	
  404
  405write_proof_subgoals([X,Y|Z]) :-
  406	write('['),
  407	write(X),
  408	write('] , '),
  409	write_proof_subgoals([Y|Z]).
  410write_proof_subgoals([X]) :-
  411	write('['),
  412	write(X),
  413	write(']').
  414
  415write_proof_indent(N) :-
  416	N > 0,
  417	write('   '),
  418	N1 is N - 1,
  419	write_proof_indent(N1).
  420write_proof_indent(0).
  421
  422process_proof([Prf|PrfEnd],_LineNum,Result) :-
  423	Prf == PrfEnd,
  424	!,
  425	Result = [].
  426process_proof([[[X,Head,PosAncestors,NegAncestors]|Y]|PrfEnd],LineNum,Result) :-
  427	LineNum1 is LineNum + 1,
  428	process_proof([Y|PrfEnd],LineNum1,P),
  429	(is_query_lit(Head) ->
  430		Depth is 0;
  431	%true ->
  432		list_length_pttp(PosAncestors,N1),	% compute indentation to show
  433		list_length_pttp(NegAncestors,N2),	% level of goal nesting from
  434		Depth is N1 + N2 + 1),		% lengths of ancestor lists
  435	Depth1 is Depth + 1,
  436	collect_proof_subgoals(Depth1,P,Subgoals),
  437	(X = redn ->
  438		X1 = red,
  439		negated_literal(Head,Head1);
  440	 ((number(X) , X < 0); X= (-(_))) ->
  441		isNegOf(X1,X),
  442		negated_literal(Head,Head1);
  443	%true ->
  444		X1 = X,
  445		Head1 = Head),
  446	Result = [[LineNum,X1,Head1,Depth,Subgoals]|P].
  447
  448collect_proof_subgoals(_Depth1,[],Result) :-
  449	Result = [].
  450collect_proof_subgoals(Depth1,[[LineNum,_,_,Depth,_]|P],Result) :-
  451	Depth = Depth1,
  452	collect_proof_subgoals(Depth1,P,R),
  453	Result = [LineNum|R].
  454collect_proof_subgoals(Depth1,[[_,_,_,Depth,_]|P],Result) :-
  455	Depth > Depth1,
  456	collect_proof_subgoals(Depth1,P,Result).
  457collect_proof_subgoals(Depth1,[[_,_,_,Depth,_]|_],Result) :-
  458	Depth < Depth1,
  459	Result = [].
  460
  461add_proof_query_line(Proof,Proof2) :-
  462	Proof = [Prf|_PrfEnd],
  463	is_ftNonvar(Prf),
  464	Prf = [[_,query,_,_]|_],
  465	!,
  466	Proof2 = Proof.
  467add_proof_query_line(Proof,Proof2) :-
  468	Proof = [Prf|PrfEnd],
  469	Proof2 = [[[0,query,[],[]]|Prf]|PrfEnd].
  470%%% ***
  471
  472%%% ****if* PTTP/clauses
  473%%% DESCRIPTION
  474%%%   Negation normal form to Prolog clause translation.
  475%%%   Include a literal in the body of each clause to
  476%%%   indicate the number of the formula the clause came from.
  477%%% SOURCE
  478
  479clauses((A , B),L,WffNum1,WffNum2) :-
  480	!,
  481	clauses(A,L1,WffNum1,W),
  482	clauses(B,L2,W,WffNum2),
  483	conjoin_pttp(L1,L2,L).
  484
  485clauses(PNF,L,WffNum1,WffNum2):- 
  486   save_wid(WffNum1,pttp_in,PNF),
  487   once(pttp_nnf(PNF,OUT)),
  488   save_wid(WffNum1,pttp_nnf,OUT),
  489   clauses1(OUT,L,WffNum1,WffNum2).
  490
  491clauses1(A,L,WffNum1,WffNum2) :-
  492	write_clause_with_number(A,WffNum1),
  493	head_literals(A,Lits),
  494	clauses2(A,Lits,L,WffNum1),
  495	kb_incr(WffNum1 ,WffNum2).
  496
  497clauses2(A,[Lit|Lits],L,WffNum) :-
  498	body_for_head_literal(Lit,A,Body1),
  499	(Body1 == false ->
  500		L = true;
  501	%true ->
  502		conjoin_pttp(infer_by(WffNum),Body1,Body),
  503		clauses2(A,Lits,L1,WffNum),
  504		conjoin_pttp((Lit :- Body),L1,L)).
  505clauses2(_,[],true,_).
  506
  507head_literals(Wff,L) :-
  508	Wff = (A :- _B) ->	% contrapositives not made for A :- ... inputs
  509		head_literals(A,L);
  510	Wff = (A , B) ->
  511		(head_literals(A,L1),
  512		 head_literals(B,L2),
  513		 list_union(L1,L2,L));
  514	Wff = (A ; B) ->
  515		(head_literals(A,L1),
  516		 head_literals(B,L2),
  517		 list_union(L1,L2,L));
  518	%true ->
  519		L = [Wff].
  520
  521body_for_head_literal(Head,Wff,Body) :-
  522	Wff = (A :- B) ->
  523		(body_for_head_literal(Head,A,A1),
  524		 conjoin_pttp(A1,B,Body));
  525	Wff = (A , B) ->
  526		(body_for_head_literal(Head,A,A1),
  527		 body_for_head_literal(Head,B,B1),
  528		 pttp_disjoin(A1,B1,Body));
  529	Wff = (A ; B) ->
  530		(body_for_head_literal(Head,A,A1),
  531		 body_for_head_literal(Head,B,B1),
  532		 conjoin_pttp(A1,B1,Body));
  533	Wff == Head ->
  534		Body = true;
  535	(once(negated_literal(Wff,Was)),Head=@=Was) ->
  536		Body = false;
  537	%true ->
  538		negated_literal(Wff,Body).
  539%%% ***
  540%%% ****if* PTTP/predicates
  541%%% DESCRIPTION
  542%%%   predicates returns a list of the predicates appearing in a formula.
  543%%% SOURCE
  544
  545is_functor_like_search(Search):-atom(Search),arg(_,vv(search,pttp_prove),Search).
  546
  547
  548is_functor_like_firstOrder(Search):-atom(Search),arg(_,vv(asserted_t,secondOrder,pttp_prove),Search).
  549is_functor_like_firstOrder(Search):-atom(Search),is_holds_true_pttp(Search).
  550is_functor_like_firstOrder(Search):-atom(Search),is_holds_false_pttp(Search).
  551
  552predicates(Wff,[]):-is_ftVar(Wff),!.
  553predicates(Wff,[]):-not(compound(Wff)),!.
  554predicates([Lw],L):- predicates(Lw,L),!.
  555predicates([Lw|ISTw],L):- !,
  556   predicates(Lw,L1),
  557   predicates(ISTw,L2),
  558   union(L2,L1,L).
  559
  560predicates(Wff,L):- functor(Wff,Search,_),is_functor_like_search(Search),arg(1,Wff,X),predicates(X,L),!.
  561
  562predicates(Wff,L) :-
  563        Wff = (A :- B) ->
  564                predicates(A,L1),
  565                predicates(B,L2),
  566                union(L2,L1,L);
  567        Wff = (A , B) ->
  568                predicates(A,L1),
  569                predicates(B,L2),
  570                union(L2,L1,L);
  571        Wff = (A ; B) ->
  572                predicates(A,L1),
  573                predicates(B,L2),
  574                union(L2,L1,L);
  575        functor(Wff,search,_) ->        % list predicates in first argument of search
  576                arg(1,Wff,X),
  577                predicates(X,L);
  578        pttp_builtin(Wff) ->
  579                L = [];
  580        %true ->
  581                functor(Wff,F,N),
  582                L = [[F,N]].
  583
  584
  585
  586predicates(Wff,L) :- functor(Wff,F,A), predicates(Wff,F,A,L).
  587
  588skipped_functor(F):- fail,is_2nd_order_holds_pttp(F).
  589
  590predicates(Wff,F,___,L):- logical_functor_pttp(F), Wff=..[_|ARGS], predicates(ARGS,L).
  591predicates(Wff,F,A,  L):- pttp_builtin(F,A), Wff=..[_|ARGS], predicates(ARGS,L).
  592% predicates(Wff,F,___,L):- skipped_functor(F), Wff=..[_|ARGS], predicates(ARGS,L).
  593predicates(Wff,F,A,[[F,A]|L]):- Wff=..[_|ARGS], predicates(ARGS,L).
  594
  595%%% ***
  596%%% ****if* PTTP/procedure
  597%%% DESCRIPTION
  598%%%   procedure returns a conjunction of the clauses
  599%%%   with head predicate P/N.
  600%%% SOURCE
  601
  602
  603procedure(P,N,Clauses,Proc) :-
  604       ( (Clauses = (A , B)) ->
  605		(procedure(P,N,A,ProcA),
  606		 procedure(P,N,B,ProcB),
  607		 conjoin_pttp(ProcA,ProcB,Proc));
  608	((Clauses = (A :- _B) , functor(A,P,N)) ->
  609		Proc = Clauses;
  610	%true ->
  611		Proc = true)).
  612
  613procedures([[P,N]|Preds],Clauses,Procs) :-
  614	procedure(P,N,Clauses,Proc),
  615	procedures(Preds,Clauses,Procs2),
  616	conjoin_pttp(Proc,Procs2,Procs).
  617procedures([],_Clauses,true).
  618%%% ***
  619
  620head_body_was(_,_).
  621
  622:- was_export(is_holds_false_pttp/1).  623is_holds_false_pttp(A):-not(atom(A)),!,fail.
  624is_holds_false_pttp(Prop):-member(Prop,[not,nholds,holds_f,mpred_f,aint,assertion_f,asserted_mpred_f,retraction,not_secondOrder,not_firstOrder]).
  625is_holds_false_pttp(F):-atom_concat(_,'_false',F).
  626%is_holds_false_pttp(F):-atom_concat(_,'_f',F).
  627is_holds_false_pttp(F):-is_p_to_n(_,F).
  628% is_holds_false_pttp(F):-atom_concat('imp',_,F).
  629
  630:- was_export(is_holds_true_pttp/1).  631is_holds_true_pttp(A):-not(atom(A)),!,fail.
  632is_holds_true_pttp(Prop):-arg(_,vvv(holds,holds_t,t,asserted_mpred_t,assertion_t,assertion,secondOrder,asserted_t),Prop).
  633is_holds_true_pttp(F):-atom_concat(_,'_true',F).
  634is_holds_true_pttp(F):-atom_concat(_,'_t',F).
  635%is_holds_true_pttp(F):-atom_concat('pos',_,F).
  636%is_holds_true_pttp(F):-atom_concat('is',_,F).
  637is_holds_true_pttp(F):-atom_concat(_,'_in',F).
  638is_holds_true_pttp(F):-is_p_to_n(F,_).
  639
  640:- was_export(is_2nd_order_holds_pttp/1).  641is_2nd_order_holds_pttp(Prop):- atom(Prop), is_holds_true_pttp(Prop) ; is_holds_false_pttp(Prop).
  642
  643
  644:- style_check(+singleton).  645
  646do_not_wrap(F):-not(atom(F)),!,fail.
  647do_not_wrap(F):-arg(_,vv(query),F).
  648do_not_wrap(F):-atom_concat('int_',_,F).
  649
  650:- was_export(correct_pttp/2).  651%:- was_dynamic t_l:second_order_wrapper/1.
  652:- thread_local t_l:second_order_wrapper/1.  653t_l:second_order_wrapper(true_t).
  654
  655
  656correct_pttp_head(Wrapper,B,A):- locally_tl(second_order_wrapper(Wrapper), correct_pttp(B,A)),!.
  657
  658correct_pttp_body(Wrapper,B,A):- locally_tl(second_order_wrapper(Wrapper), correct_pttp(B,A)),!.
  659
  660correct_pttp(B,A):-must(correct_pttp([],B,A)),!.
  661
  662correct_pttp(LC,B,A):-member_eq(B,LC),A=B.
  663correct_pttp(LC,-B,NA):-!,must((correct_pttp([B|LC],B,A),negated_literal(A,AN),correct_pttp(LC,AN,NA))),!.
  664correct_pttp(LC,n(_,B),NA):-!,must((correct_pttp([B|LC],B,A),negated_literal(A,AN),correct_pttp(LC,AN,NA))),!.
  665correct_pttp(LC,B,A):-once(correct_pttp_0([B|LC],B,A)),B==A,!.
  666correct_pttp(LC,B,A):-once(correct_pttp_0([B|LC],B,A)),!. % dmsg(once(correct_pttp_0(LC,B,A))),term_variables(B,BV),term_variables(A,AV),must(AV==BV).
  667
  668correct_pttp_0(_,Body,Body):-is_ftVar(Body).
  669correct_pttp_0(_,Body,Body):-not(compound(Body)),!.
  670correct_pttp_0(_,BodyIn,Body):- is_ftVar(BodyIn),trace_or_throw(var_correct_lit(BodyIn,Body)).
  671correct_pttp_0(LC,BodyIn,Body):- functor(BodyIn,F,A),'=..'(BodyIn,[F|List]),correct_pttp_1(LC,BodyIn,F,A,List,Body).
  672
  673correct_pttp_1(LC, BodyIn,F,_,_,Body):- sanity(atom(F)), atom_concat('not_',_,F),negated_literal(BodyIn,Neg),!,
  674   correct_pttp(LC,Neg,NegBody), 
  675   negated_literal(NegBody,Body).
  676correct_pttp_1(LC, BodyIn,F,_,_,Body):- is_holds_false_pttp(F),negated_literal(BodyIn,Neg),!,correct_pttp(LC,Neg,NegBody),negated_literal(NegBody,Body),!.
  677correct_pttp_1(LC, BodyIn,F,A,L,Body):- is_holds_false_pttp(F),trace_or_throw(correct_pttp_1(LC,BodyIn,F,A,L,Body)).
  678correct_pttp_1(LC,_BodyIn,F,_,[L|IST],Body):- length([L|IST],A), correct_pttp_2(LC,F,A,[L|IST],Body).
  679
  680:- kb_shared(wrapper_for/2).  681
  682correct_pttp_2(_,F,_,[L|IST],Body):- wrapper_for(F,Wrapper),!, wrap_univ(Body ,[Wrapper,F,L|IST]).
  683correct_pttp_2(_,F,A,[L|IST],Body):- correct_pttp_4(F,A,[L|IST],Body),!.
  684correct_pttp_2(_LC,F,_A,[L|IST],Body):- do_not_wrap(F),!,wrap_univ(Body,[F,L|IST]).
  685correct_pttp_2(_LC,F,A,[L|IST],Body):- atom(F),pttp_builtin(F,A),!,dmsg(todo(warn(pttp_builtin(F,A)))),wrap_univ(Body,[call_builtin,F,L|IST]).
  686correct_pttp_2(LC,F,_, L,Body):- is_ftVar(F),!,trace_or_throw(correct_pttp_2(LC,F,L,Body)).
  687correct_pttp_2(_LC,F,_,[L|IST],Body):- is_holds_true_pttp(F),!,wrap_univ(Body,[F,L|IST]).
  688% uncomment (need it) 
  689correct_pttp_2(_,infer_by,1,[L|IST],Body):- infer_by = F, wrap_univ(Body ,[F,L|IST]).
  690
  691% slow for 7
  692correct_pttp_2(LC,F,A,[L|IST],Body):-correct_pttp_3(LC,F,A,[L|IST],Body),!.
  693
  694correct_pttp_3(_,F,A,[L|IST],Body):- correct_pttp_4(F,A,[L|IST],Body),!.
  695correct_pttp_3(_,F,_,[L|IST],Body):- t_l:second_order_wrapper(Wrapper),!, wrap_univ(Body ,[Wrapper,F,L|IST]).
  696correct_pttp_3(_,F,_,[L|IST],Body):- wrap_univ(Body,[true_t,F,L|IST]).
  697
  698wrap_univ(Body ,[WapperPred,[P]]):-is_wrapper_pred(WapperPred),compound(P),P=..F_ARGS,!,wrap_univ(Body ,[WapperPred|F_ARGS]).
  699wrap_univ(Body ,[WapperPred,P]):-is_wrapper_pred(WapperPred),compound(P),P=..F_ARGS,!,wrap_univ(Body ,[WapperPred|F_ARGS]).
  700wrap_univ(Body ,[F1,F2|ARGS]):- F1==F2,!,wrap_univ(Body ,[F1|ARGS]).
  701wrap_univ(_Body,[F|ARGS]):- must((atom(F),is_list(ARGS))),length(ARGS,A),must(A>1),functor(P,F,A),fail,
  702  (predicate_property(P,_)->fail;(dmsg(once(warn(no_predicate_property(P)))))),fail.
  703wrap_univ(Body ,[F|List]):- must((Body=..[F|List])).
  704
  705is_wrapper_pred(VarPred):-is_ftVar(VarPred),!,fail.
  706is_wrapper_pred(not_possible_t).
  707is_wrapper_pred(call_builtin).
  708is_wrapper_pred(WapperPred):-is_p_or_not(WapperPred),!.
  709
  710% correct_pttp_4(F,A,[L|IST],Body):-...
  711correct_pttp_4(_,_,_,_):-!,fail.
  712
  713%%% ***
  714%%% ****if* PTTP/pttp1
  715%%% SOURCE
  716
  717%:- was_export(pttp1/2).
  718%pttp1(X,Y) :- must_pttp_id(ID), !, pttp1_wid(ID, X,Y).
  719:- was_export(pttp1_wid/3).  720pttp1_wid(ID,X,Y) :-    
  721 must_det_l((   
  722   pttp1a_wid(ID,X,X0),
  723   pttp1b_wid(ID,X0,X8),
  724   pttp1c_wid(ID,X0,X8,IntProcs,Procs),
  725   conjoin_pttp(Procs,IntProcs,Y))).
  726
  727
  728
  729:- was_export(pttp1a_wid/3).  730
  731% pttp1a_wid(ID,X,XX):-pttp1a_wid_0(ID,X,XX),!.
  732
  733pttp1a_wid(ID,X,XX):-pttp1a_wid_0(ID,X,X0),
  734  ((X0=(FOO:-TRUE),TRUE==true)->pttp1a_wid_0(ID,FOO,XX);XX=X0).
  735
  736
  737pttp1a_wid_0(ID,X,X0) :-    
  738 must_det_l((
  739        subst(X , ~,-,XX1),
  740        subst(XX1,~,-,XX2),
  741        subst(XX2,not,-,XX3),
  742	% write('PTTP input formulas:'),        
  743	clauses(XX3,X0,ID,_))).
  744
  745pttp1b_wid(_ID,X0,X8) :- must(apply_to_conjuncts(X0,add_features,X8)).
  746
  747
  748pttp1c_wid(_ID,X0,X8,IntProcs,Procs) :-    
  749 must_det_l((
  750	predicates(X8,IntPreds0),
  751	list_reverse(IntPreds0,IntPreds1),
  752	procedures(IntPreds1,X8,IntProcs),
  753	predicates(X0,Preds0),
  754	list_reverse(Preds0,Preds),
  755	apply_to_elements(Preds,make_wrapper(IntPreds1),Procs))).
  756
  757
  758
  759
  760% :- ensure_loaded(dbase_i_mpred_pttp_compile_stickel_orig).
  761
  762
  763%%% ***
  764%%% ****if* PTTP/pttp2
  765%%% SOURCE
  766
  767:- was_export(pttp2_wid/2).  768pttp2_wid(ID,Y) :- !, must(apply_to_conjuncts(Y,pttp_assert_int_wid_for_conjuncts(ID),_)).
  769/*
  770:- was_export(pttp2/1).
  771pttp2(Y) :- must_pttp_id(ID), pttp2_wid(ID,Y).
  772
  773pttp2(Y) :-
  774%	nl,
  775%	write('PTTP output formulas:'),
  776%	apply_to_conjuncts(Y,write_clause,_),
  777%	nl,
  778	nl,
  779	tell('pttp_temp.pl'),
  780	apply_to_conjuncts(Y,write_clause,_),
  781	nl,
  782	told,
  783	compile('pttp_temp.pl'),
  784	nl,
  785	!.
  786%%% ***
  787%%% ****if* PTTP/expand_input_proof
  788%%% SOURCE
  789*/
  790
  791:- was_export(expand_input_proof/2).  792expand_input_proof([],_Proof).
  793expand_input_proof([N|L],[[N|_]|L1]) :-
  794	expand_input_proof(L,L1).
  795%%% ***
  796%%% ****if* PTTP/contract_output_proof
  797%%% SOURCE
  798
  799:- was_export(contract_output_proof/2).  800contract_output_proof([Prf|PrfEnd],Proof) :-
  801	Prf == PrfEnd,
  802	!,
  803	Proof = [].
  804contract_output_proof([[[N,_,_,_]|L]|PrfEnd],[N|L1]) :-
  805	contract_output_proof([L|PrfEnd],L1).
  806%%% ***
  807%%% ****if* PTTP/proof_length
  808%%% SOURCE
  809
  810proof_length([Prf|PrfEnd],N) :-
  811	Prf == PrfEnd,
  812	!,
  813	N = 0.
  814proof_length([[[_,X,_,_]|L]|PrfEnd],N) :-
  815	proof_length([L|PrfEnd],N1),
  816	(X == query -> N is N1; N is N1 + 1).
  817%%% ***
  818%%% ****if* PTTP/proof_depth
  819%%% SOURCE
  820
  821proof_depth([Prf|PrfEnd],N) :-
  822	Prf == PrfEnd,
  823	!,
  824	N = 0.
  825proof_depth([[[_,_,PosAnc,NegAnc]|L]|PrfEnd],N) :-
  826	proof_depth([L|PrfEnd],N1),
  827	list_length_pttp(PosAnc,N2),
  828	list_length_pttp(NegAnc,N3),
  829	N4 is N2 + N3,
  830	max(N1,N4,N).
  831%%% ***
  832
  833%%% ****if* PTTP/pttp_functor
  834%%% DESCRIPTION
  835%%%   Sometimes the `functor' predicate doesn't work as expected and
  836%%%   a more comprehensive predicate is needed.  The pttp_functor'
  837%%%   predicate overcomes the problem of functor(X,13,0) causing
  838%%%   an error in Symbolics Prolog.  You may need to use it if
  839%%%   `functor' in your Prolog system fails to construct or decompose
  840%%%   terms that are numbers or constants.
  841%%% SOURCE
  842
  843pttp_functor(Term,F,N) :-
  844	is_ftNonvar(F),
  845	atomic(F),
  846	N == 0,
  847	!,
  848	Term = F.
  849pttp_functor(Term,F,N) :-
  850	is_ftNonvar(Term),
  851	atomic(Term),
  852	!,
  853	F = Term,
  854	N = 0.
  855pttp_functor(Term,F,N) :-
  856	functor(Term,F,N).
  857%%% ***
  858%%% ****if* PTTP/list_append
  859%%% SOURCE
  860
  861list_append([X|L1],L2,[X|L3]) :-
  862	list_append(L1,L2,L3).
  863list_append([],L,L).
  864%%% ***
  865%%% ****if* PTTP/list_reverse
  866%%% SOURCE
  867
  868list_reverse(L1,L2) :-
  869	revappend(L1,[],L2).
  870
  871revappend([X|L1],L2,L3) :-
  872	revappend(L1,[X|L2],L3).
  873revappend([],L,L).
  874%%% ***
  875%%% ****if* PTTP/list_union
  876%%% SOURCE
  877
  878list_union([X|L1],L2,L3) :-
  879	identical_member_special(X,L2),
  880	!,
  881	list_union(L1,L2,L3).
  882list_union([X|L1],L2,[X|L3]) :-
  883	list_union(L1,L2,L3).
  884list_union([],L,L).
  885%%% ***
  886%%% ****if* PTTP/list_length_pttp
  887%%% SOURCE
  888
  889list_length_pttp([_X|L],N) :-
  890	list_length_pttp(L,N1),
  891	N is N1 + 1.
  892list_length_pttp([],0).
  893%%% ***
  894%%% ****if* PTTP/min
  895%%% SOURCE
  896
  897min(X,Y,Min) :-
  898	X =< Y ->
  899		Min = X;
  900	%true ->
  901		Min = Y.
  902%%% ***
  903%%% ****if* PTTP/max
  904%%% SOURCE
  905
  906max(X,Y,Max) :-
  907	X =< Y ->
  908		Max = Y;
  909	%true ->
  910		Max = X.
  911%%% ***
  912%%% ****if* PTTP/conjoin_pttp
  913%%% SOURCE
  914
  915:- was_export(conjoin_pttp/3).  916
  917conjoin_pttp(A,B,C) :- A==B, !, C=A.
  918conjoin_pttp(A,B,C) :- var(A),!,conjoin_pttp(varcall(A),B,C).
  919conjoin_pttp(A,B,C) :- var(B),!,conjoin_pttp(A,varcall(B),C).
  920conjoin_pttp(infer_by(_),B,B) :- !.
  921conjoin_pttp(false,true,call(false)).
  922conjoin_pttp(A,B,C) :- B==false,!,conjoin_pttp(false,A,C).
  923conjoin_pttp(A,B,C) :- A==false,!,must(negated_literal(B,C)).
  924conjoin_pttp(A,B,C) :-
  925	A == true ->
  926		C = B;
  927	B == true ->
  928		C = A;
  929        A == false ->
  930		C = false;
  931	B == false ->
  932		C = false;
  933	%true ->
  934		C = (A , B).
  935%%% ***
  936%%% ****if* PTTP/pttp_disjoin
  937%%% SOURCE
  938
  939pttp_disjoin(A,B,C) :-
  940	A == true ->
  941		C = true;
  942	B == true ->
  943		C = true;
  944	A == false ->
  945		C = B;
  946	B == false ->
  947		C = A;
  948	%true ->
  949		C = (A ; B).
  950
  951
  952
  953is_builtin_p_to_n('mudEquals','not_mudEquals').
  954
  955%is_p_to_n_2way('answerable_t','unknown_t').
  956is_p_to_n_2way('askable_t','fallacy_t').
  957
  958
  959%ODD is_p_to_n(',','not_both_t').
  960%ODD is_p_to_n(';','not_either_t').
  961%ODD is_p_to_n('&','not_both_t').
  962%ODD is_p_to_n('v','not_either_t').
  963%ODD is_p_to_n('both_t','not_both_t').
  964%ODD is_p_to_n('not_both_t',',').
  965% is_p_to_n('true_t','not_possible_t').
  966% is_p_to_n('not_true_t','possible_t').
  967is_p_to_n('possible_t','not_possible_t').
  968is_p_to_n('not_possible_t','possible_t').
  969
  970%is_p_to_n(P,N):-is_p_to_n_2way(P,N).
  971%is_p_to_n(P,N):-is_p_to_n_2way(N,P).
  972is_p_to_n('not_unknown_t','not_answerable_t').
  973% TODO is_p_to_n('not_true_t','possible_t').
  974is_p_to_n('proven_in','impossible_in').
  975is_p_to_n(P,N):-is_builtin_p_to_n(P,N).
  976is_p_to_n('isa','not_mudIsa').
  977is_p_to_n(P0,N0):-is_p_to_not(P),atom_concat('not_',P,N),P0=P,N0=N.
  978is_p_to_n(P,N):- false,is_p_to_n1(P,N).
  979
  980is_p_to_not('asserted_t').
  981is_p_to_not('possible_t').
  982is_p_to_not('true_t').
  983is_p_to_not('not_true_t').
  984is_p_to_not('fallacy_t').
  985is_p_to_not('answerable_t').
  986
  987
  988is_p_to_not('unknown_t').
  989is_p_to_not('askable_t').
  990
  991is_p_to_not('pred_isa_t').
  992
  993
  994is_p_to_not('pred_t').
  995
  996
  997is_p_or_not(F):-is_p_to_n(P,N),(F=P;F=N).
  998
  999% possible_t TODO
 1000
 1001is_p_to_n1(P,N):-atom(P),is_p_to_n0(PF,NF),atom_concat(Root,PF,P),atom_concat(Root,NF,N).
 1002is_p_to_n1(P,N):-atom(N),is_p_to_n0(PF,NF),atom_concat(Root,NF,N),atom_concat(Root,PF,P).
 1003is_p_to_n1(P,N):-atom(P),is_p_to_n0(PF,NF),atom_concat(PF,Root,P),atom_concat(NF,Root,N).
 1004is_p_to_n1(P,N):-atom(N),is_p_to_n0(PF,NF),atom_concat(NF,Root,N),atom_concat(PF,Root,P).
 1005
 1006is_p_to_n0('_pos','_neg').
 1007is_p_to_n0('true_','false_').
 1008is_p_to_n0('_true','_false').
 1009is_p_to_n0('pos_','neg_').
 1010is_p_to_n0('when_','unless_').
 1011is_p_to_n0('possible_','impossible_').
 1012
 1013
 1014
 1015%is_p_simple('not_proven_not_t','possible_t').
 1016%is_p_simple('not_possible_t','not_true_t').
 1017%is_p_simple('not_unknown_t','answerable_t').
 1018%is_p_simple('not_answerable_t','unknown_t').
 1019is_p_simple(X,X).
 1020%%% ***
 1021%%% ****if* PTTP/negated_functor
 1022%%% SOURCE
 1023
 1024negated_functor0(_,_):-!,fail.
 1025%negated_functor0(true_t,not_possible_t).
 1026%negated_functor0(not_true_t,possible_t).
 1027
 1028%negated_functor0(F,NotF) :- is_p_to_n(F,NotF).
 1029%negated_functor0(F,NotF) :- is_p_to_n(NotF,F).
 1030
 1031:- was_export(negated_functor/2). 1032negated_functor(F,NotF) :- var(F),!,trace_or_throw(negated_functor(F,NotF)).
 1033%negated_functor(F,NotF) :- sanity(atom(F)),atom_concat('not_',Now,F),!,must(NotF=Now).
 1034negated_functor(F,SNotF) :- negated_functor0(F,NotF),!,is_p_simple(NotF,SNotF).
 1035negated_functor((-),_):-!,dtrace(negated_functor((-),_)),fail.
 1036negated_functor((~),_):-!,dtrace(negated_functor((~),_)),fail.
 1037negated_functor(F,NotF) :- atom_concat('int_',Now,F),!,negated_functor(Now,Then),atom_concat('int_',Then,NotF),!.
 1038negated_functor(F,NotF) :- must( \+member(F,[&,(,),(;),(v),(all),(:-)])),
 1039	name(F,L),
 1040	name('not_',L1),
 1041	(list_append(L1,L2,L) ->
 1042		true;
 1043	%true ->
 1044		list_append(L1,L,L2)),
 1045	name(NotF,L2).
 1046negated_functor(F,NotF) :- is_2nd_order_holds_pttp(F),trace_or_throw(negated_functor(F,NotF) ).
 1047negated_functor(F,NotF) :- is_2nd_order_holds_pttp(NotF),trace_or_throw(negated_functor(F,NotF) ).
 1048
 1049%%% ***
 1050%%% ****if* PTTP/negated_literal
 1051%%% SOURCE
 1052
 1053negated_literal(A,B):-var(A),!,trace_or_throw(var_negated_literal(A,B)),!.
 1054negated_literal(not(A),A):-!.
 1055negated_literal(-(A),A):-!.
 1056negated_literal(A,-(A)):-is_ftVar(A),!.
 1057negated_literal(-(A),(A)):-is_ftVar(A),!.
 1058negated_literal(A,-(A)):-atom(A),A\=(~),A\=(-),!.
 1059negated_literal(A,B):- functor(A,F,_Arity),member(F,[&,(,),(;),(v),(all),(:-)]),must_det_l((as_dlog(A,AA),IN=not(AA), call((nnf('$VAR'('KB'),IN,BB),BB \=@= IN,baseKB:as_prolog(BB,B))))).
 1060negated_literal(not(A),B):-negated_literal(A,AA),!,negated_literal_0(AA,B),!.
 1061negated_literal(-A,B):-negated_literal(A,AA),!,negated_literal_0(AA,B),!.
 1062negated_literal(A,B):- var(B),!,negated_literal_0(A,B),!.
 1063negated_literal(B,-A):-negated_literal(A,AA),!,negated_literal_0(AA,B),!.
 1064negated_literal(A,B):- negated_literal_0(A,B),!.
 1065negated_literal(A,B):- ground(B),not(ground(A)),!,negated_literal(B,A),!.
 1066
 1067negated_literal_0(Lit,NotLit) :-
 1068	Lit =.. [F1|L1],
 1069	negated_functor(F1,F2),
 1070	(is_ftVar(NotLit) ->
 1071		wrap_univ(NotLit , [F2|L1]);
 1072	%true ->
 1073	       
 1074               ( wrap_univ(NotLit , [F2|L2]),
 1075		L1 == L2) ).
 1076
 1077%%% ***
 1078%%% ****if* PTTP/is_negative_functor
 1079%%% SOURCE
 1080
 1081is_negative_functor(F) :- is_holds_false_pttp(F),!.
 1082is_negative_functor(F) :-
 1083	name(F,L),
 1084	name('not_',L1),
 1085	list_append(L1,_,L).
 1086%%% ***
 1087%%% ****if* PTTP/is_negative_literal
 1088%%% SOURCE
 1089
 1090is_negative_literal(Lit) :-
 1091	functor(Lit,F,_),
 1092	is_negative_functor(F).
 1093
 1094%%% ***
 1095%%% ****if* PTTP/internal_functor
 1096%%% SOURCE
 1097
 1098internal_functor(P) :-
 1099	name(P,L),
 1100	name('int_',L1),
 1101	list_append(L1,_,L).
 1102
 1103internal_functor(P,IntP) :-
 1104	name(P,L),
 1105	name('int_',L1),
 1106	list_append(L1,L,L2),
 1107	name(IntP,L2).
 1108%%% ***
 1109%%% ****if* PTTP/apply_to_conjuncts
 1110%%% SOURCE
 1111
 1112apply_to_conjuncts(Wff,P,Wff1) :-
 1113	Wff = (A , B) ->
 1114		apply_to_conjuncts(A,P,A1),
 1115		apply_to_conjuncts(B,P,B1),
 1116		conjoin_pttp(A1,B1,Wff1);
 1117	%true ->
 1118		P =.. G,
 1119		list_append(G,[Wff,Wff1],G1),
 1120		T1 =.. G1,
 1121		call(T1).
 1122%%% ***
 1123%%% ****if* PTTP/apply_to_elements
 1124%%% SOURCE
 1125
 1126apply_to_elements([X|L],P,Result) :-
 1127	P =.. G,
 1128	list_append(G,[X,X1],G1),
 1129	T1 =.. G1,
 1130	call(T1),
 1131	apply_to_elements(L,P,L1),
 1132	conjoin_pttp(X1,L1,Result).
 1133apply_to_elements([],_,true).
 1134
 1135%%% ***
 1136%%% ****if* PTTP/write_clause
 1137%%% SOURCE
 1138
 1139write_clause(A) :-
 1140	nl,
 1141	write(A),
 1142	write(.).
 1143
 1144write_clause(A,_) :-				% 2-ary predicate for use as
 1145	write_clause(A).			% apply_to_conjuncts argument
 1146%%% ***
 1147%%% ****if* PTTP/write_clause_with_number
 1148%%% SOURCE
 1149
 1150write_clause_with_number(A,WffNum) :-
 1151	nl,
 1152	write_indent_for_number(WffNum),
 1153	write(WffNum),
 1154	write('  '),
 1155        copy_term(A,AA),
 1156        numbervars(AA,0,_,[attvar(bind),singletons(true)]),
 1157	write(AA),
 1158	write(.).
 1159
 1160write_indent_for_number(N) :-
 1161	((number(N) , N <  100) -> write(' ') ; true),
 1162	((number(N) , N <   10) -> write(' ') ; true).
 1163%%% ***
 1164
 1165%%% ****if* PTTP/timed_call
 1166%%% DESCRIPTION
 1167%%%   A query can be timed by timed_call(query,'Proof').
 1168%%% NOTES
 1169%%%   assumes that statistics(cputime,T) binds T to run-time in seconds
 1170%%%   different Prolog systems have different ways to get this information
 1171%%% SOURCE
 1172:- was_export(timed_call/2). 1173:- meta_predicate(timed_call(0,+)). 1174timed_call(X,Type) :-
 1175	statistics(cputime,T1),			%SWI Prolog
 1176	(call(time(X)) -> V = success ; V = failure),	%SWI Prolog
 1177	statistics(cputime,T2),			%SWI Prolog
 1178	Secs is T2 - T1,			%SWI Prolog
 1179%	statistics(runtime,[T1,_]),		%Quintus/SICStus Prolog
 1180%	(call(X) -> V = success ; V = failure),	%Quintus/SICStus Prolog
 1181%	statistics(runtime,[T2,_]),		%Quintus/SICStus Prolog
 1182%	Secs is (T2 - T1) / 1000.0,		%Quintus/SICStus Prolog
 1183	nl,
 1184	write(Type),
 1185	write(' time: '),
 1186	write(Secs),
 1187	write(' seconds'),
 1188	nl,
 1189	V = success.
 1190%%% ***
 1191%%% ****if* PTTP/write_search_progress
 1192%%% SOURCE
 1193
 1194write_search_progress(Level) :- Level>100,!.
 1195
 1196write_search_progress(_Level) :- !.
 1197write_search_progress(Level) :-
 1198	% write('cost '),
 1199	write(Level),write('.'),current_output(S),flush_output(S).
 1200
 1201%%% ***
 1202
 1203%%% ****if* PTTP/pttp_builtin
 1204%%% DESCRIPTION
 1205%%%   List of pttp_builtin predicates that can appear in clause bodies.
 1206%%%   No extra arguments are added for ancestor goals or depth-first
 1207%%%   iterative-deepening search.  Also, if a clause body is
 1208%%%   composed entirely of pttp_builtin goals, the head is not saved
 1209%%%   as an ancestor for use in reduction or pruning.
 1210%%%   This list can be added to as required.
 1211%%% SOURCE
 1212
 1213pttp_builtin(T) :-
 1214	functor(T,F,N),
 1215	pttp_builtin(F,N).
 1216
 1217
 1218pttp_builtin(V,A):-is_ftVar(V),!,trace_or_throw(pttp_builtin(V,A)).
 1219pttp_builtin(!,0).
 1220
 1221
 1222pttp_builtin(F,A):- mpred_prop(F,A,prologHybrid),!,fail.
 1223pttp_builtin(isa,2):-!,fail.
 1224pttp_builtin(isa,_):-!,fail.
 1225pttp_builtin(S2,_):-is_p_to_not(S2),!,fail.
 1226
 1227pttp_builtin(call_proof,2).
 1228pttp_builtin(query,0):-!,fail.
 1229pttp_builtin(true,0).
 1230pttp_builtin(false,0).
 1231pttp_builtin(fail,0).
 1232pttp_builtin(succeed,0).
 1233pttp_builtin(dtrace,0).
 1234pttp_builtin(atom,1).
 1235pttp_builtin(integer,1).
 1236pttp_builtin(number,1).
 1237pttp_builtin(F,_):-is_p_or_not(F),!,fail.
 1238pttp_builtin(not_asserted_t,_):-!,fail.
 1239pttp_builtin(clause_u,1).
 1240pttp_builtin(atomic,1).
 1241pttp_builtin(constant,1).
 1242pttp_builtin(functor,3).
 1243pttp_builtin(arg,3).
 1244pttp_builtin(var,1).
 1245%pttp_builtin(->,2).
 1246%pttp_builtin(->,3).
 1247pttp_builtin(nonvar,1).
 1248pttp_builtin(call,1).
 1249pttp_builtin(=,2).
 1250pttp_builtin(\=,2).
 1251pttp_builtin(==,2).
 1252pttp_builtin(\==,2).
 1253pttp_builtin(=\=,2).
 1254pttp_builtin(>,2).
 1255pttp_builtin(<,2).
 1256pttp_builtin(>=,2).
 1257pttp_builtin(loop_check,_).
 1258pttp_builtin(=<,2).
 1259pttp_builtin(is,2).
 1260pttp_builtin(display,1).
 1261pttp_builtin(write,1).
 1262pttp_builtin(nl,0).
 1263pttp_builtin(only_if_pttp,0).
 1264pttp_builtin(ANY,A):-atom(ANY),A==0.
 1265pttp_builtin(infer_by,_).
 1266pttp_builtin(search_cost,_).
 1267pttp_builtin(mudEquals,2):-!.
 1268pttp_builtin(F,A):-functor(P,F,A),prequent(P),!.
 1269pttp_builtin(F,A):-is_builtin_p_to_n(P,N),member(F,[P,N]),member(A,[2,3,4]).
 1270pttp_builtin(test_and_decrement_search_cost,_).
 1271pttp_builtin(unify,_).
 1272pttp_builtin(identical_member_special,_).
 1273pttp_builtin(identical_member_special_loop_check,_).
 1274pttp_builtin(M:P,A):-atom(M),!,pttp_builtin(P,A).
 1275pttp_builtin(F,A):- (mpred_prop(F,A,prologBuiltin)),!. %,fail.
 1276% TODO pttp_builtin(F,_):- (mpred_prop(F,A,prologDynamic)),!. %,fail.
 1277pttp_builtin(unifiable_member,_).
 1278% TODO pttp_builtin(t,_).
 1279%pttp_builtin(F,A):-mpred_prop(F,A,prologPTTP),!,fail.
 1280%pttp_builtin(F,A):-mpred_prop(F,A,prologKIF),!,fail.
 1281pttp_builtin(F,A):-current_predicate(F/A),functor(P,F,A),builtin_why(P,F,A,Why),!,dmsg(todo(warn(builtin_why(F,A,Why)))).
 1282%%% ***
 1283
 1284builtin_why(_,int_query,_,_):-!,fail.
 1285builtin_why(_,query,_,_):-!,fail.
 1286builtin_why(_,F,_,int_):- atom_concat(_,'_int',F),!.
 1287builtin_why(_,F,_,int_):- atom_concat('int_',_,F),!,fail.
 1288builtin_why(P,_,_,meta_predicate(P)):- predicate_property(P,meta_predicate(P)).
 1289builtin_why(P,_,_,thread_local):- predicate_property(P,thread_local).
 1290builtin_why(P,_,_,source_file(F)):- source_file(P,F).
 1291builtin_why(P,_,_,built_in):- real_builtin_predicate(P).
 1292builtin_why(P,_,_,transparent):- predicate_property(P,transparent).
 1293% builtin_why(P,_,_,number_of_rules(N)):- predicate_property(P,number_of_rules(N)),N>0.
 1294builtin_why(X,0):-atom(X).
 1295%builtin_why(P,2,t(P,2)):-t(P,_,_),!,fail.
 1296%builtin_why(P,3,t(P,3)):-t(P,_,_,_),!,fail.
 1297
 1298
 1299
 1300
 1301% -----------------------------------------------------------------
 1302%  pttp_nnf(+Fml,?NNF)
 1303%
 1304% Fml is a first-order formula and NNF its Skolemized negation 
 1305% normal form.
 1306%
 1307% Syntax of Fml:
 1308%  negation: '-', disj: 'v', conj: '&', impl: '=>', eqv: '<=>',
 1309%  quant. 'all(X,<Formula>)', where 'X' is a prolog variable.
 1310%
 1311% Syntax of NNF: negation: '-', disj: ';', conj: ',', quant.:
 1312%  'all(X,<Formula>)', where 'X' is a prolog variable.
 1313%
 1314% Example:  pttp_nnf(ex(Y, all(X, (f(Y) => f(X)))),NNF).
 1315%           NNF =  all(_A,(-(f(all(X,f(ex)=>f(X))));f(_A)))) ?
 1316:- was_export(pttp_nnf/2). 1317pttp_nnf((A,B),(C,D)):- must(is_ftNonvar(A)), !, pttp_nnf(A,C), pttp_nnf(B,D).
 1318pttp_nnf(Fml,NNFOUT) :- pttp_nnf(Fml,[],NNF,_),NNFOUT=NNF.
 1319
 1320:-     op(400,fy,-),    % negation
 1321	op(500,xfy,&),   % conjunction
 1322	op(600,xfy,v),   % disjunction
 1323	op(650,xfy,=>),  % implication
 1324	op(680,xfy,<=>). % equivalence
 1325
 1326
 1327% -----------------------------------------------------------------
 1328%  pttp_nnf(+Fml,+FreeV,-NNF,-Paths)
 1329%
 1330% Fml,NNF:    See above.
 1331% FreeV:      List of free variables in Fml.
 1332% Paths:      Number of disjunctive paths in Fml.
 1333
 1334pttp_nnf_pre_clean(_Type,Atomic,Atomic,[]):-atomic(Atomic),!.
 1335pttp_nnf_pre_clean(_Type,Atomic,Atomic,[]):-is_ftVar(Atomic),!.
 1336pttp_nnf_pre_clean(Type,pttp(A),AA,Vars):- !,pttp_nnf_pre_clean(Type,A,AA,Vars).
 1337pttp_nnf_pre_clean(Type,[A|B],[AA|BB],Vars):-!,
 1338   pttp_nnf_pre_clean(Type,A,AA,Vars1),
 1339   pttp_nnf_pre_clean(Type,B,BB,Vars2),
 1340   append(Vars1,Vars2,Vars).
 1341
 1342pttp_nnf_pre_clean(_Type,C,CC,Vars):-
 1343   C=..[A|B],
 1344   logical_functor_pttp(A),!,
 1345   pttp_nnf_pre_clean_functor(A,AA,Vars1),!,
 1346   pttp_nnf_pre_clean(sent,B,BB,Vars2),
 1347   append(Vars1,Vars2,Vars),
 1348   CC=..[AA|BB],!.
 1349
 1350pttp_nnf_pre_clean(Type,CIN,CC,Vars):-
 1351   Type == sent,
 1352   correct_pttp(CIN,C),
 1353   C=..[A|B],
 1354   pttp_nnf_pre_clean_functor(A,AA,Vars1),!,
 1355   pttp_nnf_pre_clean(arg,B,BB,Vars2),
 1356   append(Vars1,Vars2,Vars),
 1357   CC=..[AA|BB],!.
 1358
 1359pttp_nnf_pre_clean(Type,C,CC,Vars):-
 1360   C=..[A|B],
 1361   pttp_nnf_pre_clean_functor(A,AA,Vars1),!,
 1362   pttp_nnf_pre_clean(Type,B,BB,Vars2),
 1363   append(Vars1,Vars2,Vars),
 1364   CC=..[AA|BB],!.
 1365
 1366
 1367pttp_nnf_post_clean(Atomic,Atomic,[]):-atomic(Atomic),!.
 1368pttp_nnf_post_clean(Atomic,Atomic,[]):-is_ftVar(Atomic),!.
 1369pttp_nnf_post_clean(pttp(A),AA,Vars):- !,pttp_nnf_post_clean(A,AA,Vars).
 1370pttp_nnf_post_clean(-(A),NN,Vars):- !,pttp_nnf_post_clean(A,AA,Vars),negated_literal(AA,NN).
 1371pttp_nnf_post_clean((A,B),(AA , BB),Vars):-
 1372   pttp_nnf_post_clean(A,AA,Vars1),
 1373   pttp_nnf_post_clean(B,BB,Vars2),
 1374   append(Vars1,Vars2,Vars).
 1375pttp_nnf_post_clean((A;B),(AA ; BB),Vars):-
 1376   pttp_nnf_post_clean(A,AA,Vars1),
 1377   pttp_nnf_post_clean(B,BB,Vars2),
 1378   append(Vars1,Vars2,Vars).
 1379pttp_nnf_post_clean([A|B],[AA|BB],Vars):-
 1380   pttp_nnf_post_clean(A,AA,Vars1),
 1381   pttp_nnf_post_clean(B,BB,Vars2),
 1382   append(Vars1,Vars2,Vars).
 1383pttp_nnf_post_clean((A&B),(AA , BB),Vars):- fail,
 1384   pttp_nnf_post_clean(A,AA,Vars1),
 1385   pttp_nnf_post_clean(B,BB,Vars2),
 1386   append(Vars1,Vars2,Vars).
 1387pttp_nnf_post_clean((A v B),(AA ; BB),Vars):- fail,
 1388   pttp_nnf_post_clean(A,AA,Vars1),
 1389   pttp_nnf_post_clean(B,BB,Vars2),
 1390   append(Vars1,Vars2,Vars).
 1391pttp_nnf_post_clean(C,CC,Vars):-
 1392   C=..[A|B],
 1393   A=AA,
 1394   pttp_nnf_post_clean(B,BB,Vars),
 1395   CC=..[AA|BB],!.
 1396
 1397
 1398
 1399pttp_nnf(Fml,FreeV,CleanNNF,Paths):-
 1400   pttp_nnf_pre_clean(sent,Fml,Clean,FreeV),
 1401   pttp_nnf_clean(Clean,FreeV,NNF,Paths),
 1402   pttp_nnf_post_clean(NNF,CleanNNF,FreeV).
 1403
 1404pttp_nnf_clean(Atomic,_,Atomic,1):-atomic(Atomic),!.
 1405pttp_nnf_clean(Atomic,_,Atomic,1):-is_ftVar(Atomic),!.
 1406pttp_nnf_clean(Fml,FreeV,NNF,Paths) :-   
 1407	(Fml = -(-A)      -> Fml1 = A;
 1408	 Fml = -all(X,F)  -> Fml1 = ex(X,-F);
 1409	 Fml = -ex(X,F)   -> Fml1 = all(X,-F);
 1410	 Fml = -(A v B)   -> Fml1 = (-A & -B);
 1411	 Fml = -(A & B)   -> Fml1 = (-A v -B);
 1412	 Fml = (A => B)   -> Fml1 = (-A v B);
 1413	 Fml = -(A => B)  -> Fml1 = A & -B;
 1414	 Fml = (A <=> B)  -> Fml1 = (A & B) v (-A & -B);
 1415	 Fml = -(A <=> B) -> Fml1 = (A & -B) v (-A & B)),!,
 1416	pttp_nnf_clean(Fml1,FreeV,NNF,Paths).
 1417
 1418pttp_nnf_clean(all(X,F),FreeV,all(X,NNF),Paths) :- !,
 1419	pttp_nnf_clean(F,[X|FreeV],NNF,Paths).
 1420
 1421pttp_nnf_clean(ex(X,Fml),FreeV,NNF,Paths) :- !,
 1422	copy_term((X,Fml,FreeV),(sk(X,Fml),Fml1,FreeV)),
 1423	pttp_nnf_clean(Fml1,FreeV,NNF,Paths).
 1424
 1425pttp_nnf_clean((A & B),FreeV,(NNF1,NNF2),Paths) :- !,
 1426	pttp_nnf_clean(A,FreeV,NNF1,Paths1),
 1427	pttp_nnf_clean(B,FreeV,NNF2,Paths2),
 1428	Paths is Paths1 * Paths2.
 1429
 1430pttp_nnf_clean((A v B),FreeV,NNF,Paths) :- !,
 1431	pttp_nnf_clean(A,FreeV,NNF1,Paths1),
 1432	pttp_nnf_clean(B,FreeV,NNF2,Paths2),
 1433	Paths is Paths1 + Paths2,
 1434	(Paths1 > Paths2 -> NNF = (NNF2;NNF1);
 1435		            NNF = (NNF1;NNF2)).
 1436
 1437pttp_nnf_clean(Lit,_,Lit,1).
 1438
 1439
 1440% :- ensure_loaded(dbase_i_mpred_pttp_precompiled).
 1441
 1442
 1443:- fixup_exports.