No. 46, January 2000


From the AAR President
Shorter Fixed Point Combinators with WALDMEISTER and the Kernel Strategy
Generation of NAFILs of Order 7
News from CADE Inc.

  • CADE Elections
  • CADE-17 Workshops - Call for Papers
    FTP'2000 - Call for Problem Sets
    Calls for Papers
  • AiML-ICTL 2000
  • ADG
    New Books
  • Term Rewriting and All That
  • A Fascinating Country in the World of Computing

  • TPTP Library Announcements
  • The TPTP Problem Library, Release v2.3.0
  • An Online Interface to TPTP

  • Special Issues Announced
  • Analytic Tableaux
  • Logical Frameworks and Meta-Languages
  • From the AAR President

    From the AAR President, Larry Wos...

    A new century (and, for some, a new millenium) brings with it an interesting article by T. Hillenbrand and B. Löchner on fixed point combinators. I have two reasons for encouraging you to read the article: it shows the power of the kernel strategy, which I and my colleague William McCune formulated; and it offers two open questions for AAR members to answer. As always, I welcome such questions. Indeed, I would be more than pleased to find my email ( filled with your challenging open questions in mathematics and logic.

    In this respect, I am delighted to include an article by Hantao Zhang reporting his success in answering a question posed by R. Cawagas about nonassociative loops. My own experience in this area, with Moufang loops, has made me appreciate the d ifficulty of the problem Zhang attacked, and the significance of his achievement .

    On a related note, I mention two other items in this issue of the AAR Newsletter. First, in my new book A Fascinating Country in the World of Computing, I present numerous and challenging open questions in mathematics and logic. Second, for the forthcoming FTP'2000 workshop , the organizers are collecting problems -- both open questions and interesting problems that have been solved but continue to challenge the researcher to find, say, a more elegant proof. Be warned: Elegant proofs can become a preoccupation, as those who are familiar with my work can attest.

    Shorter Fixed Point Combinators with WALDMEISTER and the
    Kernel Strategy

    Thomas Hillenbrand and Bernd Löchner
    Universität Kaiserslautern (

    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?


    [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


    the correct fixed point is


    This correction will appear in a forthcoming issue of the Journal of Automated Reasoning.

    Generation of NAFILs of Order 7

    Hantao Zhang
    The University of Iowa

    In November 1999, I received a request from Dr. Raoul Cawagas at the Polytechnic University of the Philippines. He asked me if I could help him to generate non-associative finite invertible loops (NAFIL) of order 7. This is a class of non-associative loops in which every element has a unique inverse and it includes the familiar IP, Moufang, and Bol loops [3]. There are many interesting loops in this class that have not yet been studied as much as other loops.

    Raoul's team developed a Pascal program called ICONSTRUCT to generate and determine the number In 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 ln 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

    where kn is the number of isomorphy classes (or nonisomorphic loops) of order n. Except for n=5, which were completely determined by construction by Albert [1] in 1944, the figures given above were determined by calculation [2] using combinatorial formulas. What these loops actually are were not known because their Cayley tables were not generated.

    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) ]
    The bottleneck of the problem is therefore how to identify isomorphic NAFILs. Two loops (S1, f1) and (S2, f2) are isomorphic if there is a one-to-one mapping such that for every . Given two loops, I used SATO to check if there exists such a mapping. Such a checking takes almost no time (about 0.01 second). I then developed a simple shell script that removes, from a list of NAFILs, all loops isomorphic to a given NAFIL. Taking the approximately 30K NAFILs of order 7 yielded by SEM, the script would make approximately 30K2 isomorphism checkings if they were all distinct. The script takes about 0.1 second for each checking/removal of isomorphs. So it would take about 90 million seconds or over 10,000 days to finish the job. Fortunately, it turns out that only 2,333 of them are distinct. So, using a PC with a single processor, the total computing time would have been about 30K 2,333 0.1 seconds, or 81 days. Clearly, this would still have been not very practical to undertake.

    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 I7=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)

    On the day he received the list of 2,333 loops from me, Raoul wrote:
    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!

    For order 8, I have not been able to generate all distinct NAFILs, because they require too much disk space. It is only feasible to generate Abelian loops of order 8. On the other hand, a C program could replace the shell script so that it can be run at least twice faster.


    Albert, A. A., Quasigroups II, Trans. Amer. Math. Soc. 55 (1944)

    Bryant, B. F., Schneider, H., Principal loop-isotopes of quasigroups, Canad. J. Math. 18 (1966), 120-125. MR 32 (1966) #5772.

    Cawagas, R. E., Terminal Report: Development of the Theory of Finite Pseudogroups (1998). Research supported by the National Research Council of the Philippines (1996-1998) under Project B-88 and B-95.

    Zhang, H., Bonacina, M.P., Hsiang, H., PSATO: a distributed propositional prover and its application to quasigroup problems . Journal of Symbolic Computation (1996) 21, 543-560

    Zhang, J., Zhang, H., Generating models by SEM, Proc. of International Conference on Automated Deduction (CADE-96), pp. 308-312, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.

    News from CADE Inc.

    CADE Trustee Elections
    Maria Paola Bonacina (Secretary of AAR and CADE)

    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.

    CADE-17 Workshops: Call for Papers

    Model Computation

    A workshop on ``Model Computation - Principles, Algorithms, Applications" will be held at CADE-17 in Pittsburgh, Pennsylvania, on June 16, 2000.

    Computing models is becoming an increasingly important topic in automated deduction. This is due to the potential application areas, such as software verification, discourse representation in natural language, deductive databases, product configuration, hardware verification, and model-based diagnosis.

    The goal of this workshop is to discuss research on the following issues:

  • Theoretical background, such as representation formalisms for models and their properties (like expressivity and complexity).
  • Calculi and respective procedures to compute models, implementations, experiments and performance issues.
  • Applications and related topics, such as finding the appropriate formulation, application problems, and problem sets.
  • 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 ( The deadline for submission is April 1, 2000.

    For further information, please see the Web site.

    Type-Theoretic Languages

    A one-day workshop on "Type-Theoretic Languages: Proof Search and Semantics" will be held in June 2000 in conjunction with CADE-17. Final proceedings will be published as a volume in Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers.

    The objective of the workshop is to provide a forum for discussion between researchers interested in proof-search in type theory, logical frameworks, and their underlying logics and researchers interested in the semantics of computation.

    Topics of interest include the following:

  • Foundations of proof-search in type-theoretic languages (sequent calculi, natural deduction, logical frameworks, etc.)
  • Systems, methods and techniques related to proof construction or to countermodels generation (tableaux, matrix, resolution, semantic techniques, proof plans, etc.)
  • Decision procedures, strategies, complexity results
  • Logic programming as search-based computation, integration of model-theoretic semantics, semantic foundations for search spaces
  • Computational models based on structures as games and realizability
  • Proof synthesis vs. program-synthesis and applications, equational theories and rewriting
  • Applications of proof-theoretic and semantics techniques to the design and implementation of theorem provers
  • Researchers interested in presenting their works are invited to send an extended abstract (up to 10 pages) by e-mail submissions of Postscript files to the program chair D. Galmiche ( before April 1, 2000.

    Additional information will be available through the Web site.

    FTP'2000 - Call for Problem Sets

    The FTP'2000 workshop to be held July 3--5, 2000, in St. Andrews, Scotland, provides researchers the opportunity to present and discuss problem sets centered on first-order theorem provers. An initial set of problems has been assembled by the workshop organizers; see the Web site.

    Further problems sets are solicited. Of particular interest are problems related to `real-world' applications (e.g., problems coming from software/hardware verification or planning). Problems do not need to be open: already solved problems that still offer some challenge (e.g., a faster solution, a shorter or otherwise better proof, comparative usage of different strategies, parallelization)are welcome, including both unsatisfiable and satisfiable problems.

    The problems may be given in plain English, a formal language, or some mixed form. For a formal first-order logic presentation, TPTP-Syntax is preferred; see the Web site. The organizers will help with the conversion if necessary. The Web page contains an interactive utility to convert the problems from TPTP to various other formats.

    The intent is that the problems will be picked up by authors who will solve them and submit a paper on the solution to FTP2000. For this purpose, the problems will be made public on a server at the organizer's site, the FTP2000 call for papers explicitly mentions them, and they should come with a short description. If a problem generates multiple submissions, a comparison of approaches may follow during the workshop. However, we emphasize that such a comparison is not intended as a contest!

    In addition to submissions presenting solutions, submissions presenting solution attempts and experimental work toward a solution are also encouraged. For this purpose, authors may use the third format in the FTP2000 call for papers (1--5 pages summaries).

    During the workshop, those who submitted a problem set are invited to give a short presentation of aspects such as its significance, difficulty, history, and solutions or solution attempts. Although not mandatory, such a presentation may be supplemented by a 1--5 pages summary.

    People who are interested in submitting their problem set(s) are asked to do so in one of the following ways: (1) send the problem set(s) to Peter Baumgartner by email (, or (2) upload the problem set(s) by anonymous ftp to and notify , or (3) offer the problem set(s) for download by us by anonymous ftp. In any case, the problem set(s) should come with a surrounding Web page. For examples, please visit the Web site.

    The deadline for submission of problem sets is February 2, 2000. For questions and general information on the FTP'2000 workshop please visit the Web site.

    Calls for Papers

    AiML-ICTL 2000

    The Advances in Modal Logic workshop and the International Conference on Temporal Logic will be run as a combined event, meeting at the University of Leipzig, Germany, on October 4-7, 2000. The combined event will bring together the strongly related modal logic and computer science-oriented temporal logic communities to present the latest exciting results in all relevant areas. In addition to regular papers, there will be a special session on description logics and applications of modal logic in knowledge representation.

    Authors are invited to submit a detailed abstract of a full paper (at most 10 pages) by May 15, 2000. Publication details are available at on the Web.


    The Third International Workshop on Automated Deduction in Geometry will be held in Zurich, Switzerland, September 25-27, 2000. These international workshops have become a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools.

    Specific topics of interest to AAR members include techniques for automated geometric reasoning, automated generation and manipulation with diagrams, automated theorem provers, and robotics.

    Potential participants are invited to submit an extended abstract of three or more pages or a full paper describing their work. The deadline for submission is June 20, 2000. Electronic submissions are preferred, and should be sent to both of the PC co-chairs: Prof. Juergen Richter-Gebert ( and Dr. Dongming Wang ( It is expected that the accepted papers will be published as a volume in the LNAI series by Springer-Verlag.

    For further information, see the Web.

    New Books

    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

    Term Rewriting

    A new book Term Rewriting and All That, by Franz Baader and Tobias Nipkow, has been published by Cambridge University Press. The book offers a unified and self-contained introduction to the field of term rewriting, as well as information about closely connected subjects such as universal algebra and unification theory. Many examples and over 170 exercises are included. The book is intended as a reference book for professional researchers: it collects in one place, and in one notation, results that have been presented at many conferences and in many journals. Detailed proofs of almost all theorems are provided.

    The book is available in both hardback (ISBN 0-521-45520-0) and paperback (ISBN 0-521-77920-0). It is 301 pages.

    Automated Reasoning

    A new book A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, by Larry Wos with Gail Pieper, has been published by World Scientific. The book includes a CD-ROM with OTTER. Because the intended audience includes students and teachers, the book presents many exercises (with hints and also answers), as well as tutorial chapters that gently introduce readers to the field of logic and to automated reasoning in general. For more advanced researchers, the book presents challenging questions, many of which are still unsolved.

    Contents: Introduction and Map for Reading the Book; Learning Logic by Example; A Brisk Introduction to Automated Reasoning; Logic Circuit Design; Logic Circuit Verification; Research in Mathematics and Logic; Formal Underpinnings; Guidelines for OTTER; Historical Vignettes; Open Questions; Appendixes with Input and Output Files and Proofs.

    The book is available in hardback form (ISBN: 998-02-3910-6) and is 660 pages.

    TPTP Library Announcements

    The TPTP Problem Library, Release v2.3.0
    Geoff Sutcliffe
    Department of Computer Science, James Cook University, Australia
    Christian Suttner
    Institut für Informatik, TU München, Germany

    The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems.

    TPTP v2.3.0 is now available from the Department of Computer Science, James Cook University, Australia. It may be obtained either by anonymous FTP from

    or from the Web.

    The TPTP is regularly updated with new problems, additional information, and enhanced utilities. Anyone who would like to register as a TPTP user and be kept informed of such developments should send email to Sutcliffe or Suttner.

    This new release, which will be used in CADE-17 ATP System Competition, contains 4229 problems in 28 domains. Changes (after v2.2.1) are as follows:

    An Online Interface to TPTP

    As noted in the article above, the TPTP (Thousands of Problems for Theorem Provers) Problem Library, created and maintained by Geoff Sutcliffe ( and Christian Suttner (, provides a database of test problems for Automated Theorem Proving (ATP) systems. Users can copy the TPTP database from the Web and install it on their computer.

    Recently, a graduate student at the University of Iowa, James Qin, built a Web interface for the TPTP database, so that a user can get any ATP problem from TPTP without installing the whole TPTP database.

    The interface is located on the Web. By clicking the mouse, the user can choose any problem and transform it into any format supported by the TPTP2X utility. Currently the formats for the following theorem provers are supported: Bliksem, Clin\_s, DFG, Dimacs, Finder, Ilf, Kif, Leantap, Tap, Metror, Mgtp, Oscar, Otter, Protein, Pttp, Setheo, Sprfn, Thinker, and Waldmeister. For people who are interested only in a few problems in a given format, this is a convenient tool to use. Comments may be left on the Web site for further improvement.

    Special Issues Announced

    Analytic Tableaux and Related Methods

    Studia Logica will devote a special issue to papers concerned with analytic tableaux and related methods of automated reasoning.

    Tableau methods are a convenient formalism for automating deduction in various nonstandard logics as well as in classical logic. Areas of application include verification of software and computer systems, deductive databases, knowledge representation (and its required inference engines) and system diagnosis.

    Suitable topics include

    The special issue will consist mainly of significant extensions of selected papers from the Tableaux 2000 Conference; but other papers may be submitted specially for the issue. See the Web site for details of the conference.

    The deadline for submission is May 30, 2000. Authors should send complete papers electronically in PostScript format (preferred) or hardcopy to Heinrich Wansing, Institute for Philosophy, Dresden University of Technology, Dresden, Germany (

    Logical Frameworks and Meta-Languages

    Guest editors David Basin ( and Amy Felty ( are planning a special issue for the Journal of Automated Reasoning on the design of logical frameworks and meta-theoretical studies. Topics of interest include comparative studies, implementation, and techniques of representation of formal systems. The deadline for submissions is January 31, 2000. For further information, see the Web site.