```    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
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
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)
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.```