NEWSLETTER

No. 50, February 2001

**Contents**

From the AAR President

Three $1 Challenge Problems

Millennium Prize Problems and Millennium Lectures

Herbrand Award: Call for Nominations

Call for Papers

New Book on

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))).The problem asks one to produce a double-negation-free proof--one that is free of n(n(n(r)), where the function

P(i(i(x,x),i(n(x),n(x))))The proof must be obtained by using an automated reasoning program.

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)))))This problem is significantly harder than MB24, however. Indeed, one might regard it as presenting a "nested" version of the obstacles presented by MB24. Specifically, in the proof we have for this problem, three or four formulas must be proved, each of which is subsumed by a clause along the way.

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.

February 7: The Poincare Conjecture -- Cameron Gordon

February 21: The Birch and Swinnerton-Dyer Conjecture -- Fernando Rodriguez-Villegas

March 7 : Yang-Mills Existence and Mass Gap -- Lorenzo Sadun

March 28 : P versus NP -- Vijaya Ramachandran

April 11 : Navier-Stokes Existence and Smoothness -- Luis Caffarelli

April 25 : The Hodge Conjecture -- Dan Freed

May 2: The Riemann Hypothesis -- Jeff Vaaler

February 21: The Birch and Swinnerton-Dyer Conjecture -- Fernando Rodriguez-Villegas

March 7 : Yang-Mills Existence and Mass Gap -- Lorenzo Sadun

March 28 : P versus NP -- Vijaya Ramachandran

April 11 : Navier-Stokes Existence and Smoothness -- Luis Caffarelli

April 25 : The Hodge Conjecture -- Dan Freed

May 2: The Riemann Hypothesis -- Jeff Vaaler

Lectures will take place at 7:00 pm in TCC 1.110 in the Thompson Conference Center. For further information contact Alan Reid, by e-mail areid@math.utexas.edu, or by phone (512) 471 3153. See also the Web site.

Secretary of AAR and CADE

On behalf of the CADE Inc. Board of Trustees

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.

For further information, see the Web site.

**LICS 2001 Workshop on "Theory and Applications of Satisfiability Testing"**

For more information about the workshop see the Web page or email Henry Kautz kautz@cs.washington.edu.

For further information, see the UNIF 2001 Web site.

**IJCAR Workshop "STRATEGIES 2001"**

For further information, please see the Web site.

**IJCAR Workshop on "Mathematical Induction"**

This one-day workshop will focus on mathematical induction, with
sessions on such areas as the combination of inductive theorem provers
with decision procedures and other reasoning components,
program synthesis and transformation, and
the use of induction in logical frameworks.
Researchers interested in attending the workshop are asked to submit ashort abstract or a position paper describing their current research
in the area or a system description of some relevant implementation
work they have performed.
The submission deadline is **March 31, 2001.**
For details, see the
Web site.

**IJCAR Workshop "Future Directions in Automated Reasoning"**

For further information, see the Web site.

**IJCAI Workshop on "Inconsistency in Data and Knowledge"**

Topics of interest include reasoning in the presence of inconsistency,
inconsistency in formal specifications, and inconsistency in
nonclassical logics and argumentation systems.
The deadline for submitting papers is
**March 8, 2001.**
For further information, see the
Web site.

Two categories of submission are invited:

For more information see the Web page.

The conference will cover original research results, case studies, use
of technologies across application domains, and reports on practical
experiments. Papers
(max. 15 pages)
describing original work in all aspects of formal
hardware and system design and verification methods are invited.
The deadline for submission is **February 23, 2001.**
For information, see the
Web site.

The conference proceedings will appear as a volume in Springer-Verlag's
Lecture Notes in Computer Science series and will be available at the
conference.
Selected contributions may be invited for publication in *STTT*
(International
Journal on Software Tools for Technology Transfer, Springer-Verlag).

An international conference on Logic Programming and Nonmonotonic
Reasoning will be held in Vienna, Austria, September 17-19, 2001.
The conference seeks to facilitate interactions between
researchers interested in the design and implementation of logic-based
programming languages and database systems, and researchers who work in
the areas of knowledge representation and non-monotonic reasoning. LPNMR
strives to encompass these theoretical and experimental studies that lead
to the construction of practical systems for declarative programming and
knowledge representation.
Papers (max. 13 pages, Springer LNCS style) should be submitted
by **April 3, 2001.**
For details, see the
Web site.

A joint German/Austrian conference on artificial intelligence
will take place in Vienna, Austria, September 19-21, 2001.
Research and application papers in artificial intelligence are solicited;
automated reasoning and knowledge representation are among the possible topics.
Papers (max. 15 pages, Springer LNCS style) should be submitted by **April 9, 2001.**
For details, see the
Web site.

Potential participants are invited to submit their papers (max. 10 pages) by
**March 31, 2001.**
Accepted papers will be published in the proceedings, which will be distributed
to the participants at the conference.
For further information,
see the
Web site.

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.