My congratulations to Martin Davis as winner of this year's Herbrand Award! The progress in the field of automated reasoning in the past 40 years is amazing, and contributions such as Martin's deserve to be acknowledged.

I encourage AAR members to participate in the CASC competition. This is one way to demonstrate how much our automated reasoning programs have advanced. Of course, I cannot resist the opportunity to also encourage you to attack open questions in various fields.

It is my distinct honor to announce on behalf of the Board of Trustees of CADE Inc. that Martin Davis is to receive the 2005 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his role as

• a founding father of the field of automated reasoning;
• coauthor of both papers that introduce what is now called the Davis-Putnam or Davis-Putnam-Logemann-Loveland procedure, variants of one of the most outstanding and useful proof procedures known today;
• historian regarding the early history of the field of automated deduction;

The Woody Bledsoe Student Travel Award was created to honor the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering much of their expenses.

The board of trustees currently includes (in alphabetical order):

The terms of Andrei Voronkov and Toby Walsh expire after CADE-20, because CADE trustees are elected for three years. The term of office of Robert Nieuwenhuis as program chair of CADE-20 also ends.

Among the outgoing trustees, Andrei Voronkov and Toby Walsh are eligible to be nominated for a second term. Robert Nieuwenhuis as outgoing ex-officio trustee is also eligible to be nominated for a first term as an elected trustee.

The 20th International Conference on Automated Deduction will take place in Tallinn, Estonia, July 22-27, 2005. CADE is the major forum for the presentation of research in all aspects of automated deduction, from logics to methods (e.g., term rewriting, tableaux, model generation) to applications.

Important Dates:

Deadline for early registration: June 20, 2005
Deadline for noncash payments: July 12, 2005
Workshops: July 22-23, 2005
Conference: July 24-27, 2005

Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles Dowek (Ecole Polytechnique), and Frank Wolter (U. Liverpool).

Invited tutorials will be given by Bruno Blanchet on "An Automatic Security Protocol Verifier Based on Resolution Theorem Proving" and by Enrico Giunchiglia on "Beyond SAT: QSAT, and SAT-based Decision Procedures."

In addition, more than two dozen papers have been accepted for presentation. The papers were selected after a rigorous review process and reflect a wide range of topics, from theory to algorithms to applications.

Five system descriptions will also be presented.

In addition, several workshops and tutorials are offered:

The CADE ATP System Competition will be held at the 20th International Conference on Automated Deduction in Tallin, Estonia, July 26, 2005.

The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE conference.

CASC evaluates the performance of sound, fully automatic, classical first-order ATP systems. The evaluation is in terms of the number of problems solved, the number of problems solved with a solution output, and the average runtime for problems solved, in the context of (1) a bounded number of eligible problems, chosen from the TPTP Problem Library, and (2) a specified time limit for each solution attempt.

An international conference in memoriam for A. Mostowski, H. Rasiowa, and C. Rauszer will be held in Warsaw on September 23 and in Ruciane-Nida on September 24-25, 2005. The conference will be held under the auspices of Studia Logica, Fundamenta Informaticae, and the Polish Association for Logic and Philosophy of Science. The goals are to gather the former students and collaborators of Andrzej Mostowski, Helena Rasiowa, and Cecylia Rauszer to recall their scientific and methodological heritage; to review the impact of their results on the foundations of mathematics and computer science; and to discuss future developments of logic and its applications.

The 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12) will be held December 2-6, 2005, in Montego Bay, Jamaica. Submission of papers for presentation at the conference is now invited. Topics of interest include the following:

automated reasoning	propositional reasoning
interactive theorem proving	description logics
proof assistants	modal and temporal logics
proof planning	nonmonotonic reasoning
proof checking	constructive logic and type theory
rewriting and unification	lambda and combinatory calculi
software and hardware verification	logic programming
network and protocol verification	constraint programming
systems specification and synthesis	logical foundations of programming
model checking	computational interpretations of logic
proof-carrying code	logic and computational complexity
logic and databases	logic in artificial intelligence
reasoning over ontologies	knowledge representation and reasoning
reasoning for the semantic web	reasoning about actions

The 2006 Federated Logic Conference will take place in Seattle, Washington, August 10-22, 2006.

The following conferences will participate in FLoC: Int'l Conference on Computer-Aided Verification (CAV), Int'l Conference on Rewriting Techniques and Applications (RTA), IEEE Symposium on Logic in Computer Science (LICS), Int'l Conference on Logic Programming (ICLP), Int'l Conference on Theory and Applications of Satisfiability Testing (SAT), and Int'l Joint Conference on Automated Reasoning (IJCAR).

Preconference workshops will be held on August 10-11. LICS, RTA, and SAT will be held in parallel on August 12-15, to be followed by mid-conference workshops and excursions on August 15-16. CAV, ICLP, and IJCAR will be held in parallel on August 16-21, to be followed by postconference workshops on August 21-22. Plenary events involving all the conferences are planned.

Since 2000, the AAR Newsletter has published the abstracts of new doctorate theses in automated reasoning. We encourage you to submit your own abstract or to invite your students to submit the information. The abstract should indicate authors and title of the thesis, name of the advisor, date of defense and institution granting the degree, and it should provide a brief summary of the thesis, including its table of contents. Please submit the abstracts to Gail Pieper, AAR Newsletter Editor, at pieper@mcs.anl.gov.