NEWSLETTER

No. 58, February 2003

**Contents**

From the AAR President

Herbrand Award: Call for Nominations

Huet Elected to the Academie des Sciences

Call for Papers for Conferences

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.

Call for Nominations

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)

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

Ulrich Furbach

President of CADE Inc.

uli@informatik.uni-koblenz.de

with copies to mariapaola.bonacina@univr.it.
President of CADE Inc.

uli@informatik.uni-koblenz.de

Academie des Sciences

(Secretary of AAR and CADE)

E-mail: mariapaola.bonacina@univr.it

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.

For all information concerning ESSLLI-2003, please consult the ESSLLI-2003 Web site. For more information concerning the ESSLLI-2003 Student Session, please consult the Web site. For other questions please send e-mail to Balder ten Cate (b.ten.cate@hum.uva.nl).

**Joint Conference CSL'03 and KGC**

Researchers are encouraged to submit articles on the following topics:

- automated deduction and interactive theorem proving
- constructive mathematics and type theory
- equational logic and term rewriting
- fuzzy logic
- modal and temporal logics
- higher-order logic
- model checking

The deadline for title and abstract is March 31, 2003, and the deadline for the full paper is April 7, 2003. For the required format of submissions see the Web site.

A lecture, jointly invited by the CSL'03 & KGC and the European Summer Schiol in Logic Language and Information, will be given by Sergei Artemov (CUNY, USA). Additional lectures are being arranged. Several tutorials also are planned: verification of infinite state systems, computational epsilon calculus, quantifier elimination, and winning strategies and controller synthesis.

**Fourth Panhellenic Logic Symposium**

Please submit the abstract to kirousis@ceid.upatras.gr by March 28, 2003. For further information, see the Web site.

- theorem proving in first-order classical, many-valued, and modal logics
- strategies and complexity of theorem proving procedures, and
- applications of first-order theorem provers.

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.

For regularly updated details of the workshop organization,
visit the FTP'2003
Web page.

For contacting the PC chairs: ftp2003@uni-koblenz.de.

Submissions must be made by March 29, 2003, and must be no more than 12 pages in standard ACM conference format. Details on formatting are available at the Web site..

The proceedings will be published by ACM Press.

PPDP 2003 is part of a federation meeting known as Principles, Logics and Implementations of high-level programming languages (PLI 2003), which includes the ACM SIGPLAN International Conference on Functional Programming (ICFP 2003). PLI will run August 25-29, 2003. The meetings will take place on the Uppsala University campus. Students who have a paper accepted for the conference are offered student membership in SIGPLAN free for one year; as members of SIGPLAN, they may apply for travel fellowships from the PAC fund.

For further information, see the following Web sites:

PPDP 2003

PLI 2003

Or, send e-mail to the conference chair Konstantinos Sagonas (kostis@it.uu.se).

Papers are solicited in the following areas:

automated reasoning | description logics |

interactive theorem proving | nonmonotonic reasoning |

implementations of logic | specification using logics |

design of logical frameworks | logic in artificial intelligence |

program and system verification | lambda and combinatory calculi |

model checking | constructive logic and type theory |

rewriting | computional interpretations of logic |

logic programming | logical foundations of programming |

constraint programming | logical aspects of concurrency |

logic and databases | program extraction from proofs |

logic and computational complexity | modal and temporal logics |

translation validation | knowledge representation and reasoning |

proof-carrying code | reasoning about actions |

logic in semantic web | effectively presented structures |

proof planning |

All questions related to submission should be sent to the program chairs: Moshe Y. Vardi (vardi@cs.rice.edu) and Andrei Voronkov (voronkov@cs.man.ac.uk). For further information, please see the Web site.

- algorithms and data structures to implement decision procedures
- techniques for the rapid prototyping of decision procedures
- techniques to implement combination or incorporation schemes
- benchmarks to evaluate and/or to compare decision procedures
- methodologies to test decision procedures
- the role of decision procedures in real-world verification efforts
- techniques to promote the re-use and the exchange of code implementing decision procedures, combination and integration schemas

Another goal of the workshop is to provide a discussion forum for the SMT-LIB initiative, a research initiative aimed at establishing a common standard for the specification of benchmarks and background theories for satisfiability modulo theories, and at creating a repository of such benchmarks. (See the Web for more information.) The workshop will host panel discussions on the SMT-LIB format.

Extended abstracts (up to 8 pages) addressing the pragmatical aspects of decision procedures are solicited. Submissions should be sent by email to pdpar03@cs.uiowa.edu by April 14, 2003. The authors of accepted submissions are expected to give a 25-minute presentation at the workshop. The proceedings of PDPAR'03 will be published as an INRIA technical report, and will be distributed at the workshop.

Joint registration with the CADE-19 conference is possible but is not required. Refer to the CADE-19 Web site for registration instructions and deadlines: CADE-19.

For further information, see the PDPAR'03 Web site.

Gail W. Pieper

February 2003