As I have occasionally done before, I am beginning the new year with a research challenge to AAR members. Specifically, from my various studies in logic and algebra, I have noticed that one is more likely to succeed in obtaining a proof if the axiom system has three or more axioms rather than a single axiom. The practical deductive power of a multiaxiom axiom system is greater than that of a single-axiom system. And this situation appears to be true regardless of whether one uses as a metric CPU time or length of proof or actual researcher's time or number of applications of a particular inference rule. Similarly, I have noticed that having a dependency in an axiom system gives that system more power, especially if the dependency is ``natural'' (for example, in group theory). The challenge then is the following. Establish the truth or falsity of the following conjecture: If one is working on an open question in logic or in algebra, one is more likely to succeed with a multiaxiom system than with a single axiom system and, similarly, one is more likely to succeed if the axiom system has dependencies.

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)
Gérard Huet (1998)
Robert S. Boyer and J Strother Moore (1999)
William W. McCune (2000)
Donald W. Loveland (2001)
Mark E. Stickel (2002).

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

Nominations should consist of a letter (preferably e-mail) of up to 2,000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2,000 words of endorsement from two other seconders. Nominations should be sent to

I am happy to inform all members of the Association for Automated Reasoning that on November 19, 2002, AAR member and Herbrand award winner Gérard Huet of INRIA was elected to the French Académie des Sciences. I learned this good news from Claude Kirchner, also a member of our association.

Gérard Huet received the Herbrand award in 1998, and the Herbrand award is listed prominently among his many honors in the article announcing his election on the INRIA site (see http://www.inria.fr).

It is very important for the field of automated reasoning that members already recognized as leaders by our scientific community be elected to national academies, as such election represents an external recognition first and foremost to the individual, but also to the fields he chose to contribute to.

Authors are invited to submit papers in the following categories: (1) extended abstracts of 8-10 pages, describing original results not published elsewhere; (2) system descriptions of 3-5 pages, describing new systems or significant upgrades of existing ones, especially including experiments (systems will have to be freely available online); and (3) position papers of 2 pages, describing the authors' research interests in the field, work in progress, or future directions of research. Papers should be sent as a postscript or pdf file to ftp2003@uni-koblenz.de by April 1, 2003.

Accepted submissions will be published in the ENTCS series (Electronic Notes in Theoretical Computer Science) and will be available electronically before the workshop.

The workshop will be part of the Federated Conference on Rewriting, Deduction and Programming (RDP'03, http://www.dsic.upv.es/ rdp03/), together with RTA (the 14th International Conference on Rewriting Techniques and Applications), TLCA (the 6th International Conference on Typed Lambda Calculi and Applications), and several workshops.