home *** CD-ROM | disk | FTP | other *** search
/ ARM Club 3 / TheARMClub_PDCD3.iso / hensa / programming / binprolog / binprolog_1 / !BinPro330_progs_boyer < prev    next >
Encoding:
Text File  |  1994-12-20  |  10.6 KB  |  394 lines
  1. :-write('use -h8000 -t1000 in BinProlog'),nl.
  2.  
  3. % generated: 20 November 1989
  4. % option(s): 
  5. %
  6. %   boyer
  7. %
  8. %   Evan Tick (from Lisp version by R. P. Gabriel)
  9. %
  10. %   November 1985
  11. %
  12. %   prove arithmetic theorem
  13.  
  14.  
  15. go:-     statistics(runtime,_),
  16.         boyer, statistics(runtime,[_,Y]),
  17.         write('time : '), write(Y), nl.
  18.  
  19.  
  20.  
  21.  
  22. boyer:- wff(Wff),
  23.         write('rewriting...'),nl,
  24.     rewrite(Wff,NewWff),
  25.         write('proving...'),nl,
  26.     tautology(NewWff,[],[]).
  27.  
  28. wff(implies(and(implies(X,Y),
  29.                 and(implies(Y,Z),
  30.                     and(implies(Z,U),
  31.                         implies(U,W)))),
  32.             implies(X,W))) :-
  33.         X = f(plus(plus(a,b),plus(c,zero))),
  34.         Y = f(times(times(a,b),plus(c,d))),
  35.         Z = f(reverse(append(append(a,b),[]))),
  36.         U = equal(plus(a,b),difference(x,y)),
  37.         W = lessp(remainder(a,b),member(a,length(b))).
  38.  
  39. tautology(Wff,Tlist,Flist) :-
  40.         (truep(Wff,Tlist) -> true
  41.         ;falsep(Wff,Flist) -> fail
  42.         ;Wff = if(If,Then,Else) ->
  43.         (truep(If,Tlist) -> tautology(Then,Tlist,Flist)
  44.         ;falsep(If,Flist) -> tautology(Else,Tlist,Flist)
  45.         ;tautology(Then,[If|Tlist],Flist),    % both must hold
  46.          tautology(Else,Tlist,[If|Flist])
  47.                 )
  48.         ),!.
  49.  
  50. rewrite(Atom,Atom) :-
  51.         atomic(Atom),!.
  52. rewrite(Old,New) :-
  53.         functor(Old,F,N),
  54.         functor(Mid,F,N),
  55.         rewrite_args(N,Old,Mid),
  56.         ( equal(Mid,Next),        % should be ->, but is compiler smart
  57.           rewrite(Next,New)       % enough to generate cut for -> ?
  58.         ; New=Mid
  59.         ),!.
  60.  
  61. rewrite_args(0,_,_) :- !.
  62. rewrite_args(N,Old,Mid) :- 
  63.         arg(N,Old,OldArg),
  64.         arg(N,Mid,MidArg),
  65.         rewrite(OldArg,MidArg),
  66.         N1 is N-1,
  67.         rewrite_args(N1,Old,Mid).
  68.  
  69. truep(t,_) :- !.
  70. truep(Wff,Tlist) :- member_chk(Wff,Tlist).
  71.  
  72. falsep(f,_) :- !.
  73. falsep(Wff,Flist) :- member_chk(Wff,Flist).
  74.  
  75. member_chk(X,[X|_]) :- !.
  76. member_chk(X,[_|T]) :- member_chk(X,T).
  77.  
  78.  
  79. equal(  and(P,Q),
  80.         if(P,if(Q,t,f),f)
  81.         ).
  82. equal(  append(append(X,Y),Z),
  83.         append(X,append(Y,Z))
  84.         ).
  85. equal(  assignment(X,append(A,B)),
  86.         if(assignedp(X,A),
  87.            assignment(X,A),
  88.            assignment(X,B))
  89.         ).
  90. equal(  assume_false(Var,Alist),
  91.         cons(cons(Var,f),Alist)
  92.         ).
  93. equal(  assume_true(Var,Alist),
  94.         cons(cons(Var,t),Alist)
  95.         ).
  96. equal(  boolean(X),
  97.         or(equal(X,t),equal(X,f))
  98.         ).
  99. equal(  car(gopher(X)),
  100.         if(listp(X),
  101.         car(flatten(X)),
  102.         zero)
  103.         ).
  104. equal(  compile(Form),
  105.         reverse(codegen(optimize(Form),[]))
  106.         ).
  107. equal(  count_list(Z,sort_lp(X,Y)),
  108.         plus(count_list(Z,X),
  109.              count_list(Z,Y))
  110.         ).
  111. equal(  countps_(L,Pred),
  112.         countps_loop(L,Pred,zero)
  113.         ).
  114. equal(  difference(A,B),
  115.         C
  116.         ) :- difference(A,B,C).
  117. equal(  divides(X,Y),
  118.         zerop(remainder(Y,X))
  119.         ).
  120. equal(  dsort(X),
  121.         sort2(X)
  122.         ).
  123. equal(  eqp(X,Y),
  124.         equal(fix(X),fix(Y))
  125.         ).
  126. equal(  equal(A,B),
  127.         C
  128.         ) :- eq(A,B,C).
  129. equal(  even1(X),
  130.         if(zerop(X),t,odd(decr(X)))
  131.         ).
  132. equal(  exec(append(X,Y),Pds,Envrn),
  133.         exec(Y,exec(X,Pds,Envrn),Envrn)
  134.         ).
  135. equal(  exp(A,B),
  136.         C
  137.         ) :- exp(A,B,C).
  138. equal(  fact_(I),
  139.         fact_loop(I,1)
  140.         ).
  141. equal(  falsify(X),
  142.         falsify1(normalize(X),[])
  143.         ).
  144. equal(  fix(X),
  145.         if(numberp(X),X,zero)
  146.         ).
  147. equal(  flatten(cdr(gopher(X))),
  148.         if(listp(X),
  149.            cdr(flatten(X)),
  150.            cons(zero,[]))
  151.         ).
  152. equal(  gcd(A,B),
  153.         C
  154.         ) :- gcd(A,B,C).
  155. equal(  get(J,set(I,Val,Mem)),
  156.         if(eqp(J,I),Val,get(J,Mem))
  157.         ).
  158. equal(  greatereqp(X,Y),
  159.         not(lessp(X,Y))
  160.         ).
  161. equal(  greatereqpr(X,Y),
  162.         not(lessp(X,Y))
  163.         ).
  164. equal(  greaterp(X,Y),
  165.         lessp(Y,X)
  166.         ).
  167. equal(  if(if(A,B,C),D,E),
  168.         if(A,if(B,D,E),if(C,D,E))
  169.         ).
  170. equal(  iff(X,Y),
  171.         and(implies(X,Y),implies(Y,X))
  172.         ).
  173. equal(  implies(P,Q),
  174.         if(P,if(Q,t,f),t)
  175.         ).
  176. equal(  last(append(A,B)),
  177.         if(listp(B),
  178.            last(B),
  179.            if(listp(A),
  180.               cons(car(last(A))),
  181.               B))
  182.         ).
  183. equal(  length(A),
  184.         B
  185.         ) :- mylength(A,B).
  186. equal(        lesseqp(X,Y),
  187.         not(lessp(Y,X))
  188.         ).
  189. equal(  lessp(A,B),
  190.         C
  191.         ) :- lessp(A,B,C).
  192. equal(  listp(gopher(X)),
  193.         listp(X)
  194.         ).
  195. equal(  mc_flatten(X,Y),
  196.         append(flatten(X),Y)
  197.         ).
  198. equal(  meaning(A,B),
  199.         C
  200.         ) :- meaning(A,B,C).
  201. equal(  member_chk(A,B),
  202.         C
  203.         ) :- mymember(A,B,C).
  204. equal(  not(P),
  205.         if(P,f,t)
  206.         ).
  207. equal(  nth(A,B),
  208.         C
  209.         ) :- nth(A,B,C).
  210. equal(  numberp(greatest_factor(X,Y)),
  211.         not(and(or(zerop(Y),equal(Y,1)),
  212.                 not(numberp(X))))            
  213.         ).
  214. equal(  or(P,Q),
  215.         if(P,t,if(Q,t,f),f)
  216.         ).
  217. equal(  plus(A,B),
  218.         C
  219.         ) :- plus(A,B,C).
  220. equal(  power_eval(A,B),
  221.         C
  222.         ) :- power_eval(A,B,C).
  223. equal(  prime(X),
  224.         and(not(zerop(X)),
  225.             and(not(equal(X,add1(zero))),
  226.                 prime1(X,decr(X))))
  227.         ).
  228. equal(  prime_list(append(X,Y)),
  229.         and(prime_list(X),prime_list(Y))
  230.         ).
  231. equal(  quotient(A,B),
  232.         C
  233.         ) :- quotient(A,B,C).
  234. equal(  remainder(A,B),
  235.         C
  236.         ) :- remainder(A,B,C).
  237. equal(  reverse_(X),
  238.         reverse_loop(X,[])
  239.         ).
  240. equal(  reverse(append(A,B)),
  241.         append(reverse(B),reverse(A))
  242.         ).
  243. equal(  reverse_loop(A,B),
  244.         C
  245.         ) :- reverse_loop(A,B,C).
  246. equal(  samefringe(X,Y),
  247.         equal(flatten(X),flatten(Y))
  248.         ).
  249. equal(  sigma(zero,I),
  250.         quotient(times(I,add1(I)),2)
  251.         ).
  252. equal(  sort2(delete(X,L)),
  253.         delete(X,sort2(L))
  254.         ).
  255. equal(  tautology_checker(X),
  256.         tautologyp(normalize(X),[])
  257.         ).
  258. equal(  times(A,B),
  259.         C
  260.         ) :- times(A,B,C).
  261. equal(  times_list(append(X,Y)),
  262.         times(times_list(X),times_list(Y))
  263.         ).
  264. equal(  value(normalize(X),A),
  265.         value(X,A)
  266.         ).
  267. equal(  zerop(X),
  268.         or(equal(X,zero),not(numberp(X)))
  269.         ).
  270.  
  271. difference(X, X, zero) :- !.
  272. difference(plus(X,Y), X, fix(Y)) :- !.
  273. difference(plus(Y,X), X, fix(Y)) :- !.
  274. difference(plus(X,Y), plus(X,Z), difference(Y,Z)) :- !.
  275. difference(plus(B,plus(A,C)), A, plus(B,C)) :- !.
  276. difference(add1(plus(Y,Z)), Z, add1(Y)) :- !.
  277. difference(add1(add1(X)), 2, fix(X)).
  278.  
  279. eq(plus(A,B), zero, and(zerop(A),zerop(B))) :- !.
  280. eq(plus(A,B), plus(A,C), equal(fix(B),fix(C))) :- !.
  281. eq(zero, difference(X,Y),not(lessp(Y,X))) :- !.
  282. eq(X, difference(X,Y),and(numberp(X),
  283.                           and(or(equal(X,zero),
  284.                                  zerop(Y))))) :- !.
  285. eq(times(X,Y), zero, or(zerop(X),zerop(Y))) :- !.
  286. eq(append(A,B), append(A,C), equal(B,C)) :- !.
  287. eq(flatten(X), cons(Y,[]), and(nlistp(X),equal(X,Y))) :- !.
  288. eq(greatest_factor(X,Y),zero, and(or(zerop(Y),equal(Y,1)),
  289.                                      equal(X,zero))) :- !.
  290. eq(greatest_factor(X,_),1, equal(X,1)) :- !.
  291. eq(Z, times(W,Z), and(numberp(Z),
  292.                       or(equal(Z,zero),
  293.                          equal(W,1)))) :- !.
  294. eq(X, times(X,Y), or(equal(X,zero),
  295.                      and(numberp(X),equal(Y,1)))) :- !.
  296. eq(times(A,B), 1, and(not(equal(A,zero)),
  297.                       and(not(equal(B,zero)),
  298.                           and(numberp(A),
  299.                               and(numberp(B),
  300.                                   and(equal(decr(A),zero),
  301.                                       equal(decr(B),zero))))))) :- !.
  302. eq(difference(X,Y), difference(Z,Y),if(lessp(X,Y),
  303.                                        not(lessp(Y,Z)),
  304.                                        if(lessp(Z,Y),
  305.                                           not(lessp(Y,X)),
  306.                                           equal(fix(X),fix(Z))))) :- !.
  307. eq(lessp(X,Y), Z, if(lessp(X,Y),
  308.                      equal(t,Z),
  309.                      equal(f,Z))).
  310.  
  311. exp(I, plus(J,K), times(exp(I,J),exp(I,K))) :- !.
  312. exp(I, times(J,K), exp(exp(I,J),K)).
  313.  
  314. gcd(X, Y, gcd(Y,X)) :- !.
  315. gcd(times(X,Z), times(Y,Z), times(Z,gcd(X,Y))).
  316.  
  317. mylength(reverse(X),length(X)).
  318. mylength(cons(_,cons(_,cons(_,cons(_,cons(_,cons(_,X7)))))),
  319.          plus(6,length(X7))).
  320.  
  321. lessp(remainder(_,Y), Y, not(zerop(Y))) :- !.
  322. lessp(quotient(I,J), I, and(not(zerop(I)),
  323.                             or(zerop(J),
  324.                                not(equal(J,1))))) :- !.
  325. lessp(remainder(X,Y), X, and(not(zerop(Y)),
  326.                              and(not(zerop(X)),
  327.                                  not(lessp(X,Y))))) :- !.
  328. lessp(plus(X,Y), plus(X,Z), lessp(Y,Z)) :- !.
  329. lessp(times(X,Z), times(Y,Z), and(not(zerop(Z)),
  330.                                   lessp(X,Y))) :- !.
  331. lessp(Y, plus(X,Y), not(zerop(X))) :- !.
  332. lessp(length(delete(X,L)), length(L), member(X,L)).
  333.  
  334. meaning(plus_tree(append(X,Y)),A,
  335.         plus(meaning(plus_tree(X),A),
  336.              meaning(plus_tree(Y),A))) :- !.
  337. meaning(plus_tree(plus_fringe(X)),A,
  338.         fix(meaning(X,A))) :- !.
  339. meaning(plus_tree(delete(X,Y)),A,
  340.         if(member(X,Y),
  341.            difference(meaning(plus_tree(Y),A),
  342.                       meaning(X,A)),
  343.            meaning(plus_tree(Y),A))).
  344.  
  345. mymember(X,append(A,B),or(member(X,A),member(X,B))) :- !.
  346. mymember(X,reverse(Y),member(X,Y)) :- !.
  347. mymember(A,intersect(B,C),and(member(A,B),member(A,C))).
  348.  
  349. nth(zero,_,zero).
  350. nth([],I,if(zerop(I),[],zero)).
  351. nth(append(A,B),I,append(nth(A,I),nth(B,difference(I,length(A))))).
  352.  
  353. plus(plus(X,Y),Z,
  354.      plus(X,plus(Y,Z))) :- !.
  355. plus(remainder(X,Y),
  356.      times(Y,quotient(X,Y)),
  357.      fix(X)) :- !.
  358. plus(X,add1(Y),
  359.      if(numberp(Y),
  360.         add1(plus(X,Y)),
  361.         add1(X))).
  362.  
  363. power_eval(big_plus1(L,I,Base),Base,
  364.            plus(power_eval(L,Base),I)) :- !.
  365. power_eval(power_rep(I,Base),Base,
  366.            fix(I)) :- !.
  367. power_eval(big_plus(X,Y,I,Base),Base,
  368.            plus(I,plus(power_eval(X,Base),
  369.                        power_eval(Y,Base)))) :- !.
  370. power_eval(big_plus(power_rep(I,Base),
  371.                     power_rep(J,Base),
  372.                     zero,
  373.                     Base),
  374.            Base,
  375.            plus(I,J)).
  376.  
  377. quotient(plus(X,plus(X,Y)),2,plus(X,quotient(Y,2))).
  378. quotient(times(Y,X),Y,if(zerop(Y),zero,fix(X))).
  379.  
  380. remainder(_,         1,zero) :- !.
  381. remainder(X,         X,zero) :- !.
  382. remainder(times(_,Z),Z,zero) :- !.
  383. remainder(times(Y,_),Y,zero).
  384.  
  385. reverse_loop(X,Y,  append(reverse(X),Y)) :- !.
  386. reverse_loop(X,[], reverse(X)          ).
  387.  
  388. times(X,         plus(Y,Z),      plus(times(X,Y),times(X,Z))      ) :- !.
  389. times(times(X,Y),Z,              times(X,times(Y,Z))              ) :- !.
  390. times(X,         difference(C,W),difference(times(C,X),times(W,X))) :- !.
  391. times(X,         add1(Y),        if(numberp(Y),
  392.                                     plus(X,times(X,Y)),
  393.                                     fix(X))                       ).
  394.