2:- module(mpred_pttp_static,[]). 4
5:- ensure_loaded(library(pfc_lib)). 6:- ensure_loaded(library('pfc2.0'/'mpred_header.pi')). 7:- '$set_source_module'(baseKB). 8
9:-
10 11 12 op(400,fy,-), 13 op(500,xfy,&), 14 op(600,xfy,v), 15 op(650,xfy,=>), 16 op(680,xfy,<=>), 17 op( 500, fy, ~), 18 op( 500, fy, all), 19 op( 500, fy, ex), 20 21 22 !. 23
34
35
36
212
213
214
216
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 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 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).
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 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 304 arg(N,X,Xn), arg(N,Y,Yn), unify(Xn,Yn),
305 N1 is N - 1, unify_args(X,Y,N1).
306
307
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
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
343
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
358
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 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 432 list_length_pttp(PosAncestors,N1), 433 list_length_pttp(NegAncestors,N2), 434 Depth is N1 + N2 + 1), 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 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].
471
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 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) -> 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 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 538 negated_literal(Wff,Body).
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,_) -> 576 arg(1,Wff,X),
577 predicates(X,L);
578 pttp_builtin(Wff) ->
579 L = [];
580 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).
593predicates(Wff,F,A,[[F,A]|L]):- Wff=..[_|ARGS], predicates(ARGS,L).
594
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 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).
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).
627is_holds_false_pttp(F):-is_p_to_n(_,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).
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). 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)),!. 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]).
689correct_pttp_2(_,infer_by,1,[L|IST],Body):- infer_by = F, wrap_univ(Body ,[F,L|IST]).
690
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
711correct_pttp_4(_,_,_,_):-!,fail.
712
716
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
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 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
761
762
766
767:- was_export(pttp2_wid/2). 768pttp2_wid(ID,Y) :- !, must(apply_to_conjuncts(Y,pttp_assert_int_wid_for_conjuncts(ID),_)).
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).
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).
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).
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).
832
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).
860
861list_append([X|L1],L2,[X|L3]) :-
862 list_append(L1,L2,L3).
863list_append([],L,L).
867
868list_reverse(L1,L2) :-
869 revappend(L1,[],L2).
870
871revappend([X|L1],L2,L3) :-
872 revappend(L1,[X|L2],L3).
873revappend([],L,L).
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).
888
889list_length_pttp([_X|L],N) :-
890 list_length_pttp(L,N1),
891 N is N1 + 1.
892list_length_pttp([],0).
896
897min(X,Y,Min) :-
898 X =< Y ->
899 Min = X;
900 901 Min = Y.
905
906max(X,Y,Max) :-
907 X =< Y ->
908 Max = Y;
909 910 Max = X.
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 934 C = (A , B).
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 949 C = (A ; B).
950
951
952
953is_builtin_p_to_n('mudEquals','not_mudEquals').
954
956is_p_to_n_2way('askable_t','fallacy_t').
957
958
967is_p_to_n('possible_t','not_possible_t').
968is_p_to_n('not_possible_t','possible_t').
969
972is_p_to_n('not_unknown_t','not_answerable_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
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
1019is_p_simple(X,X).
1023
1024negated_functor0(_,_):-!,fail.
1027
1030
1031:- was_export(negated_functor/2). 1032negated_functor(F,NotF) :- var(F),!,trace_or_throw(negated_functor(F,NotF)).
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
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 1073
1074 ( wrap_univ(NotLit , [F2|L2]),
1075 L1 == L2) ).
1076
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).
1089
1090is_negative_literal(Lit) :-
1091 functor(Lit,F,_),
1092 is_negative_functor(F).
1093
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).
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 1118 P =.. G,
1119 list_append(G,[Wff,Wff1],G1),
1120 T1 =.. G1,
1121 call(T1).
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
1138
1139write_clause(A) :-
1140 nl,
1141 write(A),
1142 write(.).
1143
1144write_clause(A,_) :- 1145 write_clause(A). 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).
1164
1172:- was_export(timed_call/2). 1173:- meta_predicate(timed_call(0,+)). 1174timed_call(X,Type) :-
1175 statistics(cputime,T1), 1176 (call(time(X)) -> V = success ; V = failure), 1177 statistics(cputime,T2), 1178 Secs is T2 - T1, 1183 nl,
1184 write(Type),
1185 write(' time: '),
1186 write(Secs),
1187 write(' seconds'),
1188 nl,
1189 V = success.
1193
1194write_search_progress(Level) :- Level>100,!.
1195
1196write_search_progress(_Level) :- !.
1197write_search_progress(Level) :-
1198 1199 write(Level),write('.'),current_output(S),flush_output(S).
1200
1202
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).
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)),!. 1277pttp_builtin(unifiable_member,_).
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)))).
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).
1294builtin_why(X,0):-atom(X).
1297
1298
1299
1300
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,-), 1321 op(500,xfy,&), 1322 op(600,xfy,v), 1323 op(650,xfy,=>), 1324 op(680,xfy,<=>). 1325
1326
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
1441
1442
1443:- fixup_exports.