With our unit equational deduction system WALDMEISTER [Hillenbrand1999], we have found new fixed point combinators for the B and H fragment of combinatory logic. The new combinators are much shorter than any previously reported. We successfully applied the kernel strategy formulated by L. Wos and W. McCune [Wos1993, McCune1991] in this undertaking.

Recall that in combinatory logic, expressions are left associated unless otherwise indicated. Then,

Bxyz = x(yz)

Hxyz = xyzy

and F is a fixed point combinator if Fx = x(Fx) for all x.

Wos and McCune conducted their studies with the automated reasoning program OTTER. The kernels they found are of the ``cubic" type (kernels of the form ttt for some t). With WALDMEISTER, we also discovered ``square" kernels (kernels of the form tt for some t), as well as other kernels that are neither of the form ttt nor tt, but some other form. These kernels were found without repetition; that is, the same kernel was not reproduced. Specifically, the kernel HH(B(Bx))(HH) led to the fixed point combinator H(B(H(HB)B)B)(HH) of length 9. Moreover, some combinators of lengths 10 and 11 were found. Up to now, no fixed point combinators shorter than length 16 had been reported for the BH fragment.

The study illustrates two important points. First, the kernel strategy is clearly a superb means for attacking problems in combinatory logic. Despite the fact that WALDMEISTER and OTTER differ vastly in implementational aspects, the kernel strategy crushed the problem instantly. Without it, to our knowledge no one has succeeded in finding these combinators or, for that matter, any fixed point combinators for the BH fragment at all.

Second, the study underscores the key role that a program's search approach may play. Since both systems use the identical kernel strategy, one might naturally wonder why they produce different results. Automated theorem proving is, however, far more complicated. A thorough analysis revealed that OTTER enumerates kernel candidates by length, whereas WALDMEISTER's enumeration order additionally takes into account an estimation of how close these candidates are to a possible solution. Consider also the fact that one of the kernels we found has weight 29. OTTER apparently takes a much longer time than does WALDMEISTER to reach such weights. In fact, after we informed Wos and McCune of our success, McCune ran OTTER for a much longer time than would have been feasible in the early 1990s when their original study was done. This time, with faster computers, OTTER was able to go much deeper into the space and was able to get two combinators of length 10.

Our research raises two interesting open questions that we invite AAR researchers to consider:

1. Are there fixed point combinators for B and H of length less than 9?

2. Can you find other fixed point combinators involving B and H alone, without knowing these fixed points and without using the kernel strategy?

References

[Hillenbrand1999] Hillenbrand, Th., Jaeger, A., and Löchner, B., "WALDMEISTER - Improvements in Performance and Ease of Use". In: "Proceedings of the 16th International Conference on Automated Deduction", volume 1632 of LNCS, pages 232-236. Springer Verlag, 1999.

[McCune1991] McCune, W., and Wos, L., "The Absence and the Presence of Fixed Point Combinators". Theoretical Computer Science 87:221-228, 1991.

[Wos1993] Wos, L., "The Kernel Strategy and Its Use for the Study of Combinatory Logic". Journal of Automated Reasoning 10(3):287-343, 1993. Note: An error exists in the strong fixed point combinator reported on page 318 of this article. Instead of

B(B(H(B(BH)(BB))(H(BH)(BB))H)B)B,

the correct fixed point is

B(B(H(B(BH(BB))(H(BH(BB))))H)B)B.

Hantao Zhang
The University of Iowa
hzhang@cs.uiowa.edu

Raoul's team developed a Pascal program called ICONSTRUCT to generate and determine the number I_n of distinct (nonisomorphic) finite invertible loops of given order n. For orders 5 and 6, the numbers are 1 and 33, respectively. For order 7, however, only the Abelian ones were determined (16). The non-Abelian ones were not completely determined because of the enormous number of possible loops to be checked for isomorphism.

The problem of determining the number of nonisomorphic loops of a given type and order is a difficult one. It is known, for instance, that the number l_n of loops (both associative and non-associative) of orders n = 5, 6, and 7 are as follows::

              Order n       5    6        7
            Number ln      56  9,408   16,942,080
            Number kn       6   109     23,760

After studying the matter, I successfully used my programs systems, SEM [5] and SATO [4], to determine the number of distinct NAFILs of order n=7. Given a set of logic formulas and a number n, SEM will generate models of size n satisfying the formulas. SATO can do the same; however, its input must be a set of propositional formulas. It is well known that a set of formulas with fixed size can be easily transformed to a set of propositional formulas.

Both SEM and SATO can easily generate all the NAFILs of a given small order. In fact, SATO generated 195,924 NAFILs of order 7 and SEM generated 29,679 (approximately 30K), both in a couple of minutes. The reason why SEM produced fewer NAFILs than SATO does is that SEM has a better heuristic to eliminate some isomorphic loops. However, both SATO and SEM were not designed to produce only nonisomorphic NAFILs.

A loop is a quasigroup with an identity. Below is the input file of SEM, which gives the definition of an a finite invertible loop. We could also add another clause to specify that a loop is not associative; but that would increase substantially the number of loops generated by SEM.

 # Sorts
 ( elem [7] )
 
 # Functions
 { f : elem elem - elem }
 
 # Variables
 < x, y, z : elem >
 
 # Definition of a loop
 [ -EQ(f(x,z), f(y,z)) | EQ(x,y) ]
 [ -EQ(f(x,y), f(x,z)) | EQ(y,z) ]
 # 0 is the identity
 [ EQ(f(0,x), x) ]  
 [ EQ(f(x,0), x) ]
 
 # Definition of ``Invertible''
 [ -EQ(f(x,y), 0) | EQ(f(y,x), 0) ]

Using a supercomputer of 48 Pentium II 400 processors we recently built for automated reasoning, I finished all the checkings in about three days. The supercomputer also makes the rerun feasible. The result is as follows. There are exactly I₇=2,333 distinct (nonisomorphic) NAFILs of order n=7 (16 Abelian and 2,317 non-Abelian). I also processed the NAFILs of orders 5 and 6 and obtained the same results as those obtained by ICONSTRUCT. Hence we now have the following complete figures for all loops and nonisomorphic NAFILs of orders and 7:

      Order n          5        6                 7
      Number ln       56      9,408           16,942,080
      Number kn       6       109               23,750
      Number In       1 (NA)   33 (7A + 26NA)   2,333 (16A + 2,317NA)

This is a fine day indeed for "loop theory" ... !!!

After a long struggle to "carack" the problem of generating all nonisomorphic NAFILs (Non-Associative Finite Invertible Loops) of orders 5 (1 loop) and 6 (33 loops), we finally "bagged" the first hard case of order 7. And the number, as you say, is: 2333 nonisomorphic loops. At this point, I feel that we have to "congratulate" ourselves for this delightful accomplishment. So, I say MABUHAY (= Long live! in the Filipino language).

I've just began studying the 2333 loops you generated and after looking at just about 33 of them, I already found some really very interesting things. I guess this will keep me and my assistant pleasantly busy during the Christmas holidays!

CADE Trustee Elections
Maria Paola Bonacina (Secretary of AAR and CADE)
E-mail: bonacina@cs.uiowa.edu

After the CADE Trustee elections held in October, the Board of Trustees elected Ulrich Furbach, of Universität Koblenz-Landau, and Frank Pfenning, of Carnegie Mellon University, President and Vice-President, respectively, of CADE Inc., resulting in the following list of CADE Trustees:

Ulrich Furbach, President (Elected 8/1997)

Frank Pfenning, Vice-President (Elected 10/1998)

Harald Ganzinger (Past Program Chair, elected 10/1999)

Claude Kirchner (Past Program Co-chair, elected 10/1998)

William W. McCune (Past Program Chair, elected 8/1997)

David A. Plaisted (Elected 10/1999)

Maria Paola Bonacina (Secretary)

David McAllester (CADE-17 Program Chair)

Neil V. Murray (Treasurer)

Congratulations to Uli and Frank on this honor and opportunity to better serve CADE and the field of automated reasoning.

The emphasis is on model construction principles for the first-order case, although we also welcome contributions concentrating on finite-domain propositional logics and more expressive logics such as higher-order and modal logics.

Submissions (10 pages, LNCS format) should be sent by email in Postscript format to Peter Baumgartner (peter@uni-koblenz.de). The deadline for submission is April 1, 2000.

We announce here two new books that we believe will be of interest to AAR members. Anyone wishing to write a review of either book for the Journal of Automated Reasoning should send email to pieper@mcs.anl.gov.