% % This is Stage 1 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. % set(para_into). clear(para_from_left). clear(para_into_left). set(para_ones_rule). 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). end_of_list. list(sos). y != a(f,y) | $Ans(y). % denial of the weak fixed point property end_of_list. % The following discards ground clauses. assign(max_weight, 1). weight_list(purge_gen). weight(x, -1000). end_of_list.