NEWSLETTER
No. 46, January 2000
Contents
From the AAR President
Shorter Fixed Point Combinators with WALDMEISTER and the Kernel Strategy
Generation of NAFILs of Order 7
News from CADE Inc.
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 (wos@mcs.anl.gov) 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.
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.
This correction will appear in a forthcoming issue of the Journal of Automated Reasoning.
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 l_{n} 56 9,408 16,942,080 Number k_{n} 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) ]The bottleneck of the problem is therefore how to identify isomorphic NAFILs. Two loops (S_{1}, f_{1}) and (S_{2}, f_{2}) 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 30K^{2} 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 I_{7}=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 l_{n} 56 9,408 16,942,080 Number k_{n} 6 109 23,750 Number I_{n} 1 (NA) 33 (7A + 26NA) 2,333 (16A + 2,317NA)
This is a fine day indeed for "loop theory" ... !!!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.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.
CADE-17 Workshops: Call for Papers
The goal of this workshop is to discuss research on the following issues:
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.
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:
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 (Didier.Galmiche@loria.fr) before April 1, 2000.
Additional information will be available through the Web site.
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 (peter@uni-koblenz.de), or (2) upload the problem set(s) by anonymous ftp to ftphost.uni-koblenz.de:/incoming/FTP2000/ and notify peter@uni-koblenz.de , 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.
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.
For further information, see the Web.
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.
The book is available in hardback form (ISBN: 998-02-3910-6) and is 660 pages.
The TPTP Problem Library, Release v2.3.0
Geoff Sutcliffe
Department of Computer Science, James Cook University, Australia
geoff@cs.jcu.edu.au
and
Christian Suttner
Institut für Informatik, TU München, Germany
suttner@informatik.tu-muenchen.de
ftp.cs.jcu.edu.au:pub/research/tptp-library
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:
As noted in the article above, the TPTP (Thousands of Problems for Theorem Provers) Problem Library, created and maintained by Geoff Sutcliffe (geoff@cs.jcu.edu.au) and Christian Suttner (suttner@informatik.tu-muenchen.de), 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.
Analytic Tableaux and Related Methods
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 (wansing@rcs1.urz.tu-dresden.de).
Logical Frameworks and Meta-Languages
Guest editors David Basin (basin@informatik.uni-freiburg.de) and Amy Felty (felty@research.bell-labs.com) 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.