1:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )). 2:- module(mpred_pttp_unused,[]). 3:- endif. 4
18
56
61
71
107
120:- use_module(clause). 121:- use_module(library(basics)). 122:- use_module(library(lists)). 123:- was_dynamic rule/3.
124
127
128clear :- abolish(rule/3),
129 assert_list(
130 [(rule(apply(X,Y),[],1) :- apply(X,Y)),
131 (rule(X is Y,[],1) :- X is Y)
132 ]).
133
134show :- listing(rule/3).
135
136axioms([]).
137axioms([H|T]) :-
138 axiom(H),
139 axioms(T).
140
141axiom(Fol) :-
142 fol_rules(Fol,Clauses),
143 assert_list(Clauses).
144
149
150pttp_prove(Sentence) :- pttp_prove(Sentence,5).
151pttp_prove(Sentence,InitialBound) :- pttp_prove(Sentence,InitialBound,100).
152
153pttp_prove(Sentence0,InitialBound,Max) :-
154 (Sentence0 = Vars^Sentence
155 ->
156 Query = query(Vars)
157 ;
158 Query = query, Sentence = Sentence0),
159 retract_query,
160 axiom(Sentence => Query),
161 prove_goal(Query,InitialBound,Max).
162
163retract_query :-
164 member(Q,[query,~query,query(_),~query(_)]),
165 retractall(rule(Q,_,_)),
166 clause(rule(A,B,C),true),
167 member(Q,B),
168 retract(rule(A,B,C)),
169 fail.
170retract_query.
171
172
173prove_goal(Goal) :- prove_goal(Goal,5,100).
174prove_goal(Goal,InitialBound) :- prove_goal(Goal,InitialBound,100).
175
176prove_goal(Goal,InitialBound,Max) :-
177 id(prove_goal_bounded(Goal,[]),InitialBound,Max).
178
179prove_goal_bounded(Goal,Anc,_B,_B) :-
181
182 identical_member(Goal, Anc),
183 !,
184 fail
184.
185prove_goal_bounded(Goal,Anc,B0,B) :-
187
188 negate(Goal,Negated),
189 identical_member(Negated, Anc),
190 tally(1,B0,B)
190.
191prove_goal_bounded(Goal,Anc,B0,B) :-
192 rule(Goal,Body,MinProofCost),
193 tally(MinProofCost,B0,B1),
194 prove_body(Body,[Goal|Anc],B1,B).
195
196prove_body([],_,B,B).
197prove_body([Goal|Goals],Anc,B0,B) :-
198 prove_goal_bounded(Goal,Anc,B0,B1),
199 prove_body(Goals,Anc,B1,B).
200
206
207fol_rules(Fol,Rules) :-
208 clausal_form(Fol,Clauses),
209 clausal_to_rules(Clauses,Rules).
210
211clausal_to_rules([],[]) :- !.
212clausal_to_rules([Clause|Clauses],Rules) :-
213 contrapositives(Clause,Rules0),
214 clausal_to_rules(Clauses,Rules1),
215 append(Rules0,Rules1,Rules).
216
217contrapositives(clause(Head,Body),C) :-
218 negate_list(Head,Not_Head),
219 append(Not_Head,Body,Atoms),
220 contras(Atoms,Atoms,C).
221
222contras([],_,[]).
223contras([H|T],Body,[Head_Rule|Tail_Rules]) :-
224 negate(H,Not_H),
225 delete(Body,H,ThisBody),
226 length(Body,Cost),
227 Head_Rule = rule(Not_H,ThisBody,Cost),
228 contras(T,Body,Tail_Rules).
229
238
239id(Goal,Bound,Max) :- id(Goal,0,Bound,Max).
240
241id(Goal,PrevBound,Bound,Max) :-
242 Bound =< Max,
243 flag(depth_cutoff,0),
244 245 apply*(Goal,[Bound,Remaining]),
246 Remaining < Bound - PrevBound.
247id(Goal,_,Bound,Max) :-
248 flag(depth_cutoff,Increment),
249 Increment > 0,
250 Bound1 is Bound + Increment,
251 Bound1 =< Max,
252 253 id(Goal,Bound,Bound1,Max).
254
255tally(N,B0,B) :-
256 (B0 >= N 257 ->
258 B is B0 - 1
259 ;
260 D is N - B0 + 1,
261 flag(depth_cutoff,C),
262 (C = 0 ; C > D),
263 flag(depth_cutoff,D),
264 !,
265 fail
266 ).
267
269
270timed(Goal) :-
271 statistics(runtime,[T0,_]),
272 call(Goal),
273 statistics(runtime,[T1,_]),
274 Secs is (T1 - T0) / 1000.0,
275 format('~nExecution took ~p seconds.~n',[Secs]).
276
278apply*(Goal,MoreArgs) :-
279 Goal =.. List0,
280 append(List0,MoreArgs,List),
281 NewGoal =.. List,
282 NewGoal.
283
284apply(Rel,Args) :-
285 Goal =.. [Rel|Args],
286 Goal.
287
288assert_list([]).
289assert_list([H|T]) :- assertz(H),assert_list(T).
290
298
299identical_member(X,[H|T]) :-
300 X == H
301 ->
302 true
303 ;
304 identical_member(X,T).
305
307
308flag(Flag,Val) :-
309 var(Val)
310 ->
311 global(Flag,Val)
312 ;
313 (retractall(global(Flag,_)),
314 assert(global(Flag,Val))).
315
317
318negate_list([],[]).
319negate_list([H|T],[Not_H|Not_T]) :-
320 negate(H,Not_H),
321 negate_list(T,Not_T).
322
323negate(~(G),G) :- !.
324negate(G,~(G)).
325
326
328
329e :- e1,e2,e3,e4,e5,e6,e7,e8,e9,
330 chang_lee_example1, chang_lee_example2.
331
332e1 :-
333 clear,
334 axiom((a or b) and ~(a)),
335 prove_goal(b),
336 \+ prove_goal(a),
337 pttp_prove(a or b).
338
339e2 :- clear,
340 axioms(
341 [rev([],[]),
342 (rev([X|Xs],Zs) <= rev(Xs,Ys) and append(Ys,[X],Zs)),
343 append([],Xs,Xs),
344 (append([X|Xs],Ys,[X|Zs]) <= append(Xs,Ys,Zs))
345 ]),
346 pttp_prove(rev([a,b,c],[c,b,a])),
347 \+ pttp_prove(rev([a,b,c],[c,b,a,z])),
348 e2(30,497).
349
368e2(N,B) :-
369 length(X,N),
370 numbervars(X,0,_),
371 timed(prove_goal(rev(X,Y),B,100000)),
372 reverse(X,Y).
375e3 :-
376 clear,
377 assertz(rule(len([],0),[],0)),
378 assertz(rule(len([_A|B],N),[len(B,N1),N is N1 + 1],2)),
379 pttp_prove(X^len([a,b],X)),
380 X == 2.
381
382e4 :-
383 clear,
384 axioms(
385 [q(X) => p(X),
386 q(2),
387 q(1)]),
388 bagof(X,pttp_prove(X^p(X)),L),
389 (L = [1,2] ; L = [2,1]).
390
391e5_1(0).
392e5_1(N) :- N > 0, axiom(p(N)),N1 is N-1, e5_1(N1).
401e5 :- e5(5).
402e5(N) :-
403 clear, e5_1(N),
404 axiom(q(X) <= p(X)),
405 axiom(r(X,Y) <= p(X) and q(Y)),
406 %%bagof(r(X,Y),pttp_prove([X,Y]^r(X,Y)),L),
407 bagof(r(X,Y),prove_goal(r(X,Y)),L),
408 length(L,Len),
409 Len =:= N*N.
410
411e6 :- clear,
412 axioms(
413 [p(X) <= apply(format,['APPLY: ~p~n',[X]]) and q(X),
414 q(1),
415 q(2)]),
416 bagof(X,pttp_prove(X^p(X)),L),
417 format('Should have done APPLY on ~p.~n',[L]).
418
419e7 :- clear,
420 axiom(a or b or c),
421 axiom(~c),
422 pttp_prove(a or b),
423 \+ pttp_prove(a or c).
424
425e8 :- clear,
426 axiom(a or b or c),
427 pttp_prove(a or b or c),
428 \+ pttp_prove(a or b),
429 \+ pttp_prove(b or c),
430 \+ pttp_prove(a or c).
431
432e9 :- clear,
433 pttp_prove(~(a and b) <=> ~a or ~b).
434
435e10 :- clear,
436 axiom(p(X) or q(X) <= r(X)),
437 axiom(r(a) and r(b)),
438 pttp_prove(X^(p(X) or q(X))),
439 \+ pttp_prove(p(a)),
440 \+ pttp_prove(p(b)),
441 \+ pttp_prove(q(a)),
442 \+ pttp_prove(q(b)),
443 \+ pttp_prove(p(a) or q(b)),
444 pttp_prove(p(a) or q(a)),
445 pttp_prove(p(b) or q(b)).
446
447chang_lee_example1 :-
448 nl,
449 write(chang_lee_example1),
450 clear,
451 axioms([
452 p(g(X,Y),X,Y),
453 p(X,h(X,Y),Y),
454 (p(U,Z,W) <= p(X,Y,U) and p(Y,Z,V) and p(X,V,W)),
455 (p(X,V,W) <= p(X,Y,U) and p(Y,Z,V) and p(U,Z,W)),
456 (query(X) <= p(k(X),X,k(X)))
457 ]),
458 fail. 459chang_lee_example1 :-
461
462
463
464 prove_goal(query(_))
464.
465
466chang_lee_example2 :-
467 nl,
468 write(chang_lee_example2),nl,
469 clear,
470 axioms(
471 [p(e,X,X),
472 p(X,e,X),
473 p(X,X,e),
474 p(a,b,c),
475 (p(U,Z,W) <= p(X,Y,U) and p(Y,Z,V) and p(X,V,W)),
476 (p(X,V,W) <= p(X,Y,U) and p(Y,Z,V) and p(U,Z,W)),
477 (query <= p(b,a,c))
478 ]),
479 fail.
480chang_lee_example2 :-
481 prove_goal(query).
482
483E