1% 2% This is Stage 1 of the Kernel Method. 3% Wos & McCune, "Searching for Fixed Point Combinators ...", ANL-88-10. 4% 5% Stage 1 searches for kernels (reducible fixed points of an 6% arbitrary combinator). 7% Stage 2 attempts to expand a kernel into a fixed point combinator. 8% 9 10set(para_into). 11clear(para_from_left). 12clear(para_into_left). 13set(para_ones_rule). 14 15clear(back_sub). 16clear(print_proofs). 17 18assign(max_proofs, -1). 19assign(max_given, 30). 20 21% set(para_into_vars). 22% set(para_from_vars). 23 24list(usable). 25x = x. 26 27% regular isolators (including replicators) 28 29 a(a(a(B,x),y),z) = a(x,a(y,z)). 30% a(a(L,x),y) = a(x,a(y,y)). 31% a(I,x) = x. 32% a(a(K,x),y) = x. 33% a(a(a(Q1,x),y),z) = a(x,a(z,y)). 34 35% irregular isolators (including replicators) 36 37% a(M,x) = a(x,x). 38% a(a(O,x),y) = a(y,a(x,y)). 39% a(a(T,x),y) = a(y,x). 40% a(a(a(Q,x),y),z) = a(y,a(x,z)). 41 42% regular replicators (non-isolating) 43 44 a(a(W,x),y) = a(a(x,y),y). 45% a(a(a(N,x),y),z) = a(a(a(x,z),y),z). 46% a(a(a(H,x),y),z) = a(a(a(x,y),z),y). 47% a(a(a(S,x),y),z) = a(a(x,z),a(y,z)). 48 49% irregular replicators (non-isolating) 50 51% a(a(W1,x),y) = a(a(y,x),x). 52 53% others (non-isolating non-replicating) 54 55% a(a(a(C,x),y),z) = a(a(x,z),y). 56% a(a(a(R,x),y),z) = a(a(y,z),x). 57 58end_of_list. 59 60list(sos). 61y != a(f,y) | $Ans(y). % denial of the weak fixed point property 62end_of_list. 63 64% The following discards ground clauses. 65 66assign(max_weight, 1). 67 68weight_list(purge_gen). 69weight(x, -1000). 70end_of_list. 71