CADE has an important election coming. Several of the candidates discuss the importance of strengthening CADE and their concern about having CADE (and automated reasoning researchers) place more emphasis on applications. I encourage you to read the statements of the nominees carefully and then vote when you receive your ballot.

These five events will join for the first time at the IJCAR conference in Cork in July 2004.

IJCAR 2004 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited.

Logics of interest include the following: propositional, first-order, classical, equational, higher-order, nonclassical, constructive, modal, temporal, many-valued, substructural, description, metalogics, type theory, and set theory.

Methods of interest include the following: tableaux, sequent calculi, resolution, model-elimination, connection method, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, efficient datastructures and indexing, integration of computer algebra systems and automated theorem provers, and combination of logics or decision procedures.

Applications of interest include the following: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, natural language processing, linguistics, robotics, and planning.

Submitted research papers and system descriptions must be original and not submitted for publication elsewhere. Research papers can be up to 15 proceedings pages long, and system descriptions can be up to 5 pages long. The proceedings of IJCAR 2004 will be published by Springer-Verlag in the LNAI/LNCS series.

IJCAR workshops will be held on July 4 and July 5, 2004. They will run for one or two days, but half-day ones are possible as well. Workshop proposals are solicited on IJCAR-related topics as mentioned previously in the Call for Papers. Particularly welcome are proposals that promise to bring new topics into IJCAR, of either practical or theoretical importance, or provide a forum for more detailed discussion on central topics of continuing importance. Workshops that close the gap between automated reasoning and related areas, for instance formal methods or software engineering, are especially encouraged.

Each workshop must have one or more designated organizers and may have a program committee as well. Workshop proposals must be limited to three pages and provide at least the following information:

• Title of the workshop
• Description of the workshop topic and goals
• Intended audience (From which areas do you expect potential participants to come? How many participants do you expect? Are there any limitations to participation, e.g., maximum number of participants? How are you going to publicize your workshop?)

• Organization of the workshop: format, duration, preferred date. (Are you going to schedule invited talks, presentations, panel discussions, and other methods for ensuring an interactive atmosphere? Are there any plans to document the workshop results beyond online distribution on the Web and IJCAR's workshop notes? Note: we prefer the workshops to be open to anyone who wishes to register, rather than limiting participation to authors or invited people.)

• Organizer details (affiliations and contact details such as email, Web page, phone, and fax of all organizers and committee members, organizers' background in the proposed topic, and a list of workshops previously organized in the workshop's or related areas).

Workshop organizers are expected to maintain a Web site showing all the relevant information of their workshop, including online versions of accepted papers. Workshop organizers are responsible on their own for sufficient distribution of their call for papers and other publicity (general IJCAR announcements will mention the IJCAR workshops as well). The IJCAR organizers offer to copy and distribute the workshop notes to registered workshop participants.

In case of questions or problems, please contact the workshop chair:

An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people are currently serving as trustees of CADE Inc.:

Franz Baader (CADE 2003 Program Chair: term expired)

David Basin (IJCAR 2004 Program Co-chair)

Maria Paola Bonacina (Secretary)

Gilles Dowek (elected 9/2001)

Ulrich Furbach, President (elected 8/1997 and 10/2000: term expired)

Harald Ganzinger (past Program Chair, elected 10/1999 and 10/2002)

John R. Harrison (elected 9/2001)

Michael Kohlhase (elected 10/2000: term expired)

David McAllester (past Program Chair, elected 10/2000: term expired)

Neil V. Murray (Treasurer)

Frank Pfenning, Vice-President (elected 10/1998 and re-elected 9/2001)

Andrei Voronkov (past Program Chair, elected 10/2002)

Toby Walsh (elected 10/2002)

The terms of office of Franz Baader, Ulrich Furbach, Michael Kohlhase and David McAllester are expiring. The position of Franz Baader is taken by David Basin, as IJCAR 2004 program co-chair. Thus, there are three positions to fill, to replace the three trustees that were elected in October 2000, since CADE trustees are elected to serve for three years.

The following candidates were nominated:

Following the tradition of the previous workshops on first-order theorem proving, a special issue will be edited to commemorate the fourth workshop in this series. This special issue will be published by Kluwer Academic Publishers within the Journal of Automated Reasoning.

This special issue will focus on first-order theorem proving as a core theme of automated deduction, including

• Theorem proving in first-order classical, many-valued, and modal logics, including resolution, equational reasoning, term rewriting, model construction, constraint reasoning, unification, description logics, propositional logic, specialized decision procedures
• Strategies and complexity of theorem-proving procedures,
• Applications of first-order theorem provers, for example to problems in verification, artificial intelligence, mathematics or education.

Editors of this special issue:

To submit a paper, send a Postscript or PDF file to ftp2003@uni-koblenz.de. Papers will be refereed following the standard JAR reviewing process.

Important Dates: