% % This is Stage 2 of the Kernel Method. % Wos & McCune, "Searching for Fixed Point Combinators ...", ANL-88-10. % % Stage 1 searches for kernels (reducible fixed points of an % arbitrary combinator). % Stage 2 attempts to expand a kernel into a fixed point combinator. % % This is the "sound" version of Stage 2, in which each proof % represents a fixed point combinator. (In the original, "unsound" % version, the user had to filter out answers containing a Skolem % constant.) % % "grep UNIT " to see the finxed-point combinators. % set(para_into). clear(para_from_left). set(para_ones_rule). set(bird_print). clear(back_sub). clear(print_proofs). assign(max_proofs, -1). assign(max_given, 30). % set(para_into_vars). % set(para_from_vars). list(usable). x = x. % regular isolators (including replicators) a(a(a(B,x),y),z) = a(x,a(y,z)). % a(a(L,x),y) = a(x,a(y,y)). % a(I,x) = x. % a(a(K,x),y) = x. % a(a(a(Q1,x),y),z) = a(x,a(z,y)). % irregular isolators (including replicators) % a(M,x) = a(x,x). % a(a(O,x),y) = a(y,a(x,y)). % a(a(T,x),y) = a(y,x). % a(a(a(Q,x),y),z) = a(y,a(x,z)). % regular replicators (non-isolating) a(a(W,x),y) = a(a(x,y),y). % a(a(a(N,x),y),z) = a(a(a(x,z),y),z). % a(a(a(H,x),y),z) = a(a(a(x,y),z),y). % a(a(a(S,x),y),z) = a(a(x,z),a(y,z)). % irregular replicators (non-isolating) % a(a(W1,x),y) = a(a(y,x),x). % others (non-isolating non-replicating) % a(a(a(C,x),y),z) = a(a(x,z),y). % a(a(a(R,x),y),z) = a(a(y,z),x). -FIXED(a(y,g(y)), g(y)) | $Ans(y). % Deny: Exists T All x FIXED(Tx,x). end_of_list. list(sos). % FIXED(a(a(W,a(B,xf)),a(W,a(B,xf))), xf). % FIXED(a(a(W,a(a(B,a(B,xf)),W)),a(a(B,a(B,xf)),W)), xf). % FIXED(a(a(W,a(B,xf)),a(W,a(B,xf))), xf). % FIXED(a(a(a(a(B,W),B),xf),a(a(a(B,W),B),xf)), xf). % FIXED(a(a(W,a(a(a(a(B,B),B),xf),W)),a(a(a(a(B,B),B),xf),W)), xf). FIXED(a(a(a(W,a(B,a(B,xf))),a(W,a(B,a(B,xf)))),x), xf). % FIXED(a(a(W,a(a(B,a(a(B,a(B,xf)),W)),a(B,a(a(B,a(B,xf)),W)))),a(B,a(a(B,a(B,xf)),W))), xf). % FIXED(a(a(W,a(a(B,a(B,xf)),W)),a(a(B,a(B,xf)),W)), xf). % FIXED(a(a(a(a(a(B,W),B),a(B,xf)),a(a(a(B,W),B),a(B,xf))),x), xf). % FIXED(a(a(a(a(B,W),a(B,a(B,xf))),a(a(B,W),a(B,a(B,xf)))),a(a(B,W),a(B,a(B,xf)))), xf). % FIXED(a(a(W,a(a(a(a(W,B),B),xf),W)),a(a(a(a(W,B),B),xf),W)), xf). % FIXED(a(a(a(W,a(a(a(B,B),B),xf)),a(W,a(a(a(B,B),B),xf))),x), xf). % FIXED(a(a(W,a(a(B,a(a(a(a(B,B),B),xf),W)),a(B,a(a(a(a(B,B),B),xf),W)))),a(B,a(a(a(a(B,B),B),xf),W))), xf). % FIXED(a(a(W,a(a(a(a(B,B),B),xf),W)),a(a(a(a(B,B),B),xf),W)), xf). % FIXED(a(a(a(a(a(B,a(a(B,W),B)),B),xf),a(a(a(B,a(a(B,W),B)),B),xf)),x), xf). % FIXED(a(a(a(a(a(B,a(B,W)),B),a(B,xf)),a(a(a(B,a(B,W)),B),a(B,xf))),a(a(a(B,a(B,W)),B),a(B,xf))), xf). % FIXED(a(a(a(a(B,a(a(B,W),a(B,a(B,xf)))),a(B,a(a(B,W),a(B,a(B,xf))))),a(B,a(a(B,W),a(B,a(B,xf))))),a(B,a(a(B,W),a(B,a(B,xf))))), xf). end_of_list.