I find it piquant that, as Bob Boyer has informed me, there now exist million dollar prizes in mathematics; see the announcement in this newsletter about the related lecture series at the University of Texas. Just as Hilbert's posing of twenty-three problems motivated significant new research, so too may these prizes direct the field and lead to extremely interesting results in mathematical analysis.

Of course, I would find it most interesting if our AAR readers would come up with a similar set of challenging problems to stimulate and direct research in automated reasoning. The problems I posed in the book 33 Basic Research Problems were one attempt at challenging researchers. Newer problems were posed in Chapter 11 of A Fascinating Country in the World of Computing; its CD-ROM contains the out-of-print book 33 Basic Research Problems. On a smaller scale, I now issue a challenge to each AAR member: Submit to me one problem or open question that might be profitably attacked by an automated reasoning system. I will collect these in a library and publish them for all our readers to attack. No, I am not offering a million dollars--to submitters or to solvers. Fame and glory might result. I am certain that many find sheer delight in solving an interesting problem and find the research worthwhile.

To provide impetus, I include in this issue three problems. They are not open questions, but I think AAR readers may find them challenging.

Being of sound mind and reasonable wallet, I offer here three $1 automated reasoning problems, in the spirit of the $1 million mathematics problems recently announced in Paris.

1. MB24

The first of our challenge problems involves the following three axioms L1, L2, and L3 of Lukasiewicz for two-valued sentential (propositional) calculus.

   P(i(i(x,y),i(i(y,z),i(x,z)))).
   P(i(i(n(x),x),x)).
   P(i(x,i(n(x),y))).

   P(i(i(x,x),i(n(x),n(x))))

It is known that this area of logic is D-complete; that is, any tautology (theorem) is deducible with condensed detachment. What is not known is whether one can always obtain a double-negation-free proof. Nor does D-completeness tell us how to obtain a condensed detachment proof.

Note, moreover, that the wording of the challenge here is precise: It is not sufficient to produce a proof of a more general theorem; indeed, OTTER can do this easily in the presence of forward subsumption. But subsumption gets in the way of finding the specific result.

Our success involved several steps. First, Dolph Ulrich provided a proof by hand of the specific theorem, assuming the provability of two key lemmas. Next, Brandon Fitelson took Ulrich's proof and, using a special version of OTTER developed by Robert Veroff, obtained a proof. Then, I took Fitelson's proof and, with several tricks, found a means for the publicly available OTTER to derive the desired proof.

Specifically, to avoid having OTTER subsume t, I had OTTER demodulate t to a constant (OTTER performs demodulation before it performs subsumption). I then put the not of that constant in the passive list, took other actions, and--success! Most recently we found a proof of length 25 (applications of condensed detachment) and level 16.

I invite AAR readers to find a more elegant (shorter) proof with OTTER or another automated reasoning program.

2. MB23

Similar to the preceding problem, MB23 begins with the three Lukasiewicz axioms and asks for a condensed-detachment, double-negation-free proof, though of course of a different lemma, the following.

   P(i(i(x,x),i(i(y,y),i(i(x,y),i(x,y)))))

Bob Veroff has solved this problem using his special version of OTTER that includes a more general treatment of the hints strategy [Veroff1996]. The length of the proof is 34; the level of proof is 17. To date, however, no proof has yet been obtained by using the standard arsenal offered by OTTER. I continue to work on the problem; perhaps one of our readers, using OTTER, will beat me to the solution--and win the $1.

3. Commutator Problem

The following problem was provided by Michael Beeson. It is taken from a homework assignment given in an algebra course at MIT.

Problem: Prove the commutator subgroup of a group is normal.

To formulate the problem more symbolically:

Write a* for a-inverse. Define [a,b] =3D aa*bb*. Then prove x*[a,b]x has the form [u,v] for some u and v.

The proof is but one line, if produced by a person with intuition. Indeed, this is the type of problem a mathematician can solve quickly. The challenge, however, lies in getting a computer program to come up with the right choice for u and v.

Consider the following "baby" example: If in a group x times x is the identity e, then the group is commutative.

A person will probably begin to solve such a problem with the simple deduction "Then yz times yz equals e ." But OTTER cannot make this deduction, not offering instantiation. Indeed, if it did, the result would be subsumed. And if one turned off subsumption, the result would be disaster: a combinatorial explosion.

I find such baby problems fascinating because they illustrate the remarkable difference between the approach taken by an unaided person and that taken by a reasoning program.

I offer Beeson's problem (not the "baby" example) as a challenge to our readers; with appropriate choices, OTTER finds a solution very, very quickly.

Reference

[Veroff1996] Veroff, R., "Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies" J. Automated Reasoning 16, no. 3 (1996) 223-239.

In May 2000, at the College de France in Paris, the Clay Mathematics Institute of Cambridge Massachusetts (CMI) announced seven Millennium Prize Problems, designating a $7 million prize fund for the solution to these problems, with $1 million allocated to each.

The Department of Mathematics at the University of Texas is pleased to announce a series of seven general audience evening lectures, "The Millennium Lectures," based on the "Millennium Prize Problems." The aim is to explain to a wide audience the historical background of these problems, why they have resisted many years of serious attempts to solve them, and the roles these problems play in modern mathematics.

The lecture series will run throughout the Spring Semester 2001 on the campus of the University of Texas at Austin and will be given by members of Departments of Mathematics and Computer Sciences. Each lecture will be introduced by Professor John Tate, who helped announce the "Millennium Prize Problems" and will be followed a reception.

The Herbrand Award is given by CADE Inc. to honor a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

Larry Wos (1992)
Woody Bledsoe (1994)
Alan Robinson (1996)
Wu Wen-Tsun (1997)
Gerard Huet (1998)
Robert S. Boyer and J Strother Moore (1999)
William W. McCune (2000).

A nomination is required for consideration for the Herbrand award. Nominations can be made at any time and remain open indefinitely, but only nominations received by March 15, 2001 will be considered for a Herbrand Award at IJCAR in June 2001.

Nominations should consist of a letter (preferably email) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to Ulrich Furbach, President of CADE Inc., uli@informatik.uni-koblenz.de, with copies to bonacina@cs.uiowa.edu.

Call for Papers

A new book entitled Automated Reasoning with Otter, by John Arnold Kalman (with a foreword by Larry Wos), presents an intriguing and thorough treatment of automated reasoning and Otter. The early chapters lead the reader through Otter's fundamental operations and show how to present questions and problems to Otter, beginning with simple examples and including numerous exercises that proceed gently from the basic to the complex. Chapters 6-9 provide a fuller treatment of such concepts as substitution and hyperresolution; the fine detail is complemented nicely by illustrations and case studies, as well as cryptarithmetic puzzles. Chapter 10 shows how, with the help of more sophisticated techniques, the class of reasoning problems that Otter can attack can be greatly extended. In particular, this chapter focuses on propositional connectives such as "not", "or", and "and", and discusses the notion of "logical equivalence." The remaining chapters, Chapters 11-15, are concerned mainly with logical problems whose solution requires reasoning about equality.