1%:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).
    2:- module(mpred_pttp_testing,[]).    3%:- endif.
    4:- '$set_source_module'(baseKB).    5
    6%%% ****h* PTTP/PTTP TESTING INTERFACE
    7%%% 
    8%%% 
    9%%% 
   10%%% 
   11%%% 
   12%%% 
   13%%% 
   14%%% 
   15
   16%:- ensure_loaded(library(pfc)).
   17%:- include(logicmoo('pfc2.0'/'mpred_header.pi')).
   18:- ensure_loaded(dbase_i_mpred_pttp).   19
   20:- kb_shared(pttp_test/2).   21:- discontiguous(pttp_test/2).   22:- kb_shared(pttp_logic/2).   23:- discontiguous(pttp_logic/2).   24
   25pttp_test(chang_lee_example1,
   26	((
   27		p(g(X,Y),X,Y),
   28		p(X,h(X,Y),Y),
   29		(p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
   30		(p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
   31		(query :- p(k(X),X,k(X)))
   32	))).
   33
   34
   35
   36
   37%%% ***
   38%%% ****f* PTTP_Examples/chang_lee_example2
   39%%% DESCRIPTION
   40%%%   In an associative system with an identity element,
   41%%%   if the square of every element is the identity,
   42%%%   the system is commutative.
   43%%% NOTES
   44%%%   this is problem GRP001-5 in TPTP
   45%%% SOURCE
   46
   47pttp_test(chang_lee_example2,
   48	((
   49		p(e,X,X),
   50		p(X,e,X),
   51		p(X,X,e),
   52		p(a,b,c),
   53		(p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
   54		(p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
   55		(query :- p(b,a,c))
   56	))).
   57
   58%%% ***
   59%%% ****f* PTTP_Examples/chang_lee_example3
   60%%% DESCRIPTION
   61%%%   In a group the left identity is also a right identity.
   62%%% NOTES
   63%%%   this is problem GRP003-1 in TPTP
   64%%% SOURCE
   65
   66:- was_export(chang_lee_example3/0).   67pttp_test(chang_lee_example3,
   68	((
   69          p(e,X,X),
   70          p(i(X),X,e),
   71          (p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
   72          (p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
   73          (query :- p(a,e,a))
   74	))).
   75
   76
   77%%% ***
   78%%% ****f* PTTP_Examples/chang_lee_example4
   79%%% DESCRIPTION
   80%%%   In a group with left genlInverse and left identity
   81%%%   every element has a right genlInverse.
   82%%% NOTES
   83%%%   this is problem GRP004-1 in TPTP
   84%%% SOURCE
   85pttp_test(chang_lee_example4,
   86	((
   87          p(e,X,X),
   88          p(i(X),X,e),
   89          (p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
   90          (p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
   91          (query :- p(a,X,e))
   92	))).
   93
   94
   95%%% ***
   96%%% ****f* PTTP_Examples/chang_lee_example5
   97%%% DESCRIPTION
   98%%%   If S is a nonempty subset of a group such that
   99%%%   if x,y belong to S, then x*inv(y) belongs to S,
  100%%%   then the identity e belongs to S.
  101%%% NOTES
  102%%%   this is problem GRP005-1 in TPTP
  103%%% SOURCE
  104
  105pttp_test(chang_lee_example5,
  106	((
  107		p(e,X,X),
  108		p(X,e,X),
  109		p(X,i(X),e),
  110		p(i(X),X,e),
  111		s(a),
  112		(s(Z) :- s(X) , s(Y) , p(X,i(Y),Z)),
  113		(p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
  114		(p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
  115		(query :- s(e))
  116	))).
  117
  118%%% ***
  119%%% ****f* PTTP_Examples/chang_lee_example6
  120%%% DESCRIPTION
  121%%%   If S is a nonempty subset of a group such that
  122%%%   if x,y belong to S, then x*inv(y) belongs to S,
  123%%%   then S contains inv(x) whenever it contains x.
  124%%% NOTES
  125%%%   this is problem GRP006-1 in TPTP
  126%%% SOURCE
  127
  128pttp_test(chang_lee_example6,
  129	((
  130		p(e,X,X),
  131		p(X,e,X),
  132		p(X,i(X),e),
  133		p(i(X),X,e),
  134		s(b),
  135		(s(Z) :- s(X) , s(Y) , p(X,i(Y),Z)),
  136		(p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
  137		(p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
  138		(query :- s(i(b)))
  139	))).
  140
  141%%% ***
  142%%% ****f* PTTP_Examples/chang_lee_example7
  143%%% DESCRIPTION
  144%%%   If a is a prime and a = b*b/c*c then a divides b.
  145%%% NOTES
  146%%%   this is problem NUM014-1 in TPTP
  147%%%
  148%%%   this problem is non-Horn
  149%%%   so clauses are written in disjunction form to
  150%%%   result in generation of all contrapositives
  151%%%
  152%%%   because the query is ground, it is unnecessary
  153%%%   for its negation to be included
  154%%% SEE ALSO
  155%%%   chang_lee_example1, chang_lee_example8
  156%%% SOURCE
  157
  158pttp_test(chang_lee_example7,
  159	((
  160		p(a),
  161		m(a,s(c),s(b)),
  162		m(X,X,s(X)),
  163		(not_m(X,Y,Z) ; m(Y,X,Z)),
  164		(not_m(X,Y,Z) ; d(X,Z)),
  165		(not_p(X) ; not_m(Y,Z,U) ; not_d(X,U) ; d(X,Y) ; d(X,Z)),
  166		(query :- d(a,b))
  167	))).
  168
  169%%% ***
  170%%% ****f* PTTP_Examples/chang_lee_example8
  171%%% DESCRIPTION
  172%%%    Any number greater than one has a prime divisor.
  173%%% NOTES
  174%%%   this is problem NUM015-1 in TPTP
  175%%%
  176%%%   this problem is non-Horn
  177%%%   so clauses are written in disjunction form to
  178%%%   result in generation of all contrapositives
  179%%%
  180%%%   the negation of the query is included
  181%%%   to allow multiple instances to be used in
  182%%%   the proof (and yield an indefinite answer)
  183%%% SEE ALSO
  184%%%   chang_lee_example1, chang_lee_example7
  185%%% SOURCE
  186
  187:- kb_shared(pttp_test_fails_is_ok/1).  188:- discontiguous(pttp_test_fails_is_ok/1).  189
  190% pttp_test_fails_is_ok(chang_lee_example8).
  191pttp_test(chang_lee_example8,
  192	((
  193		l(1,a),
  194		d(X,X),
  195		(p(X) ; d(g(X),X)),
  196		(p(X) ; l(1,g(X))),
  197		(p(X) ; l(g(X),X)),
  198		(not_p(X) ; not_d(X,a)),		% negation of query
  199		(not_d(X,Y) ; not_d(Y,Z) ; d(X,Z)),
  200		(not_l(1,X) ; not_l(X,a) ; p(f(X))),
  201		(not_l(1,X) ; not_l(X,a) ; d(f(X),X)),
  202		(query :- (p(X) , d(X,a)))
  203	))).
  204
  205%%% ***
  206%%% ****f* PTTP_Examples/chang_lee_example9
  207%%% DESCRIPTION
  208%%%   There exist infinitely many primes.
  209%%% NOTES
  210%%%   this is problem NUM016-2 in TPTP
  211%%% SOURCE
  212
  213pttp_test(chang_lee_example9,
  214	((
  215		l(X,f(X)),
  216		not_l(X,X),
  217		(not_l(X,Y) ; not_l(Y,X)),
  218		(not_d(X,f(Y)) ; l(Y,X)),
  219		(p(X) ; d(h(X),X)),
  220		(p(X) ; p(h(X))),
  221		(p(X) ; l(h(X),X)),
  222		(not_p(X) ; not_l(a,X) ; l(f(a),X)),	% negation of query
  223		(query :- p(X) , l(a,X) , not_l(f(a),X))
  224	))).
  225
  226%%% ***
  227%%% ****f* PTTP_Examples/overbeek_example4
  228%%% DESCRIPTION
  229%%%   Show that Kalman's shortest single axiom for the
  230%%%   equivalential calculus, XGK, can be derived from the
  231%%%   Meredith single axiom PYO.
  232%%% NOTES
  233%%%   a harder problem than the Chang and Lee examples
  234%%%   from Overbeek's competition problems
  235%%%
  236%%%   this is problem LCL024-1 in TPTP
  237%%% SOURCE
  238
  239% pttp_test(_,_):- !,fail.
  240
  241pttp_test_skipped(overbeek_example4a,     
  242	((
  243		(p(e(X,e(e(Y,e(Z,X)),e(Z,Y))))),
  244		((p(Y) :- p(e(X,Y)), p(X))),
  245		((queryXXX :- p(e(e(e(a,e(b,c)),c),e(b,a))))),
  246                ((query:- call(pttp_prove(queryXXX,100,0,2))))
  247	))).
  248
  249
  250pttp_test_fails_is_ok(overbeek_example4).
  251pttp_test(overbeek_example4,     
  252	((
  253		(p(e(X,e(e(Y,e(Z,X)),e(Z,Y))))),
  254		((p(Y) :- p(e(X,Y)), p(X))),
  255		((query :- p(e(e(e(a,e(b,c)),c),e(b,a)))))
  256	))).
  257
  258%%% ***
  259pttp_test_query(overbeek_example4,pttp_prove(query,100,0,2)).	% cost 30 proof
  260%%% ***
  261
  262
  263
  264pttp_test(logicmoo_example1,
  265	((
  266          mudMother(iJoe,iSue),
  267          (mudMother(X,Y) => isa(Y,tFemale)),
  268          (mudChild(Y,X) => (mudMother(X,Y);mudFather(X,Y))),          
  269          (query:- isa(Y,tFemale))
  270	))).
  271
  272
  273
  274pttp_test(logicmoo_example1_holds,
  275	((
  276          asserted_t(mudMother,iJoe,iSue),
  277          (asserted_t(mudMother,X,Y) => isa(Y,tFemale)),
  278          (asserted_t(mudChild,Y,X) => (true_t(mudMother,X,Y);true_t(mudFather,X,Y))),          
  279          (query:- isa(Y,tFemale))
  280	))).
  281
  282pttp_logic(logicmoo_prules,
  283        ((      
  284         uses_logic(logicmoo_kb_refution),
  285           (mudMother(X,Y) => isa(Y,tFemale)),
  286           (mudChild(Y,X) => (mudMother(X,Y);mudFather(X,Y))),  
  287           (asserted_t(mudMother,X,Y) => isa(Y,tFemale)),
  288           (asserted_t(mudChild,Y,X) => (true_t(mudMother,X,Y);true_t(mudFather,X,Y)))))).
  289
  290
  291%  kbholds(mudChild,iGun,iSonOfGun,A,B,C,C,D,E,F):- D=[G,[1,F,A,B]|H],E=[G|H].
  292%  not_kbholds(tFemale,iGun,A,B,C,C,D,E,F):- D=[G,[-2,F,A,B]|H],E=[G|H].
  293%  query(A,B,C,D,E,F,G):- (E=[H,[3,query,A,B]|I],J=[H|I]),asserted_t(K,iSonOfGun,iGun,A,B,C,D,J,F).
  294%  asserted_t(A,B,C,D,E,F,G,H,I):- J=asserted_t(A,B,C), (identical_member(J,D)->fail; (identical_member(J,E),!;unifiable_member(J,E)),G=F,H=[K,[red,J,D,E]|L],I=[K|L];kbholds(A,B,C,D,E,F,G,H,I,J)).
  295%  not_kbholds(A,B,C,D,E,F,G,H):- I=asserted_t(A,B), (identical_member(I,D)->fail; (identical_member(I,C),!;unifiable_member(I,C)),F=E,G=[J,[redn,I,C,D]|K],H=[J|K];not_kbholds(A,B,C,D,E,F,G,H,I)).
  296pttp_test(logicmoo_example2,
  297	((         
  298          uses_logic(logicmoo_prules),
  299          mudMother(iJoe,iSue),
  300           asserted_t(mudChild,iGun,iSonOfGun),
  301          (-isa(iGun,tFemale)),
  302          (query:- true_t(What,iSonOfGun,iGun))
  303          % What = mudFather
  304	))):-What='$VAR'('?MUD-FATHER').
  305
  306pttp_test(logicmoo_example22,
  307	((          
  308          uses_logic(logicmoo_prules),
  309           asserted_t(mudChild,iGun,iSonOfGun),
  310          (-isa(iGun,tFemale)),
  311          (query:- true_t(What,iSonOfGun,iGun))
  312          % What = mudFather
  313	))):-What='$VAR'('?MUD-FATHER').
  314
  315
  316% not_firstOrder(tFemale, iGun,E,F,A,B,C,G,D) :- test_and_decrement_search_cost(A, 0, B), C=[H, [-4, D, E, F]|I], G=[H|I].
  317% firstOrder(Pred,Arg1,Arg2,E,F,A,B,C,G,D) :- call_prop_val2(Pred,Arg1,Arg2), test_and_decrement_search_cost(A, 0, B), C=[H, [3, D, E, F]|I], G=[H|I].
  318
  319baseKB:sanity_test:- do_pttp_test(logicmoo_example3).
  320
  321baseKB:regression_test:- do_pttp_test(logicmoo_example3).
  322
  323
  324% pttp_test_fails_is_ok(logicmoo_example3).
  325pttp_test(logicmoo_example3,
  326	((
  327          uses_logic(logicmoo_kb_logic),
  328          pred_t(genlInverse,mudParent,mudChild),
  329          pred_t(genlPreds,mudMother,mudParent),
  330          pred_isa_t(predIrreflexive,mudChild),         
  331          asserted_t(mudParent, iSon1, iFather1),
  332        (query:- (not_true_t(mudChild, iSon1, iFather1)))
  333          
  334          % Expected true
  335	))).
  336
  337
  338
  339
  340% pttp_test_fails_is_ok(logicmoo_example4).
  341pttp_test(logicmoo_example4,
  342	((
  343          uses_logic(logicmoo_kb_logic),
  344          pred_t(genlInverse,mudParent,mudChild),
  345          pred_t(genlPreds,mudMother,mudParent),
  346          pred_isa_t(predIrreflexive,mudChild),         
  347          asserted_t(mudParent, iSon1, iFather1),
  348          (query:- -(possible_t(mudChild, iSon1, iFather1)))
  349          % Expected true
  350	))).
  351
  352
  353pttp_logic(Name,Data):- pttp_test(Name,Data).
  354
  355:- foreach(pttp_logic(N,_),(asserta_if_new(N:- pttp_load_wid(N)),export(N/0))).  356:- foreach(pttp_test(N,_),(asserta_if_new(N:- do_pttp_test(N)),export(N/0))).  357
  358:- if_startup_script(do_pttp_tests).  359
  360
  361:- fixup_exports.