In recent years there has been impressive progress in the development of high-performance ATP systems, and ATP systems are becoming more and more useful as tools of research and commercial application. As the use of ATP systems expands to harder problems and new domains, it is important place new problems and problem types in public view, to foster the development of ATP systems and techniques that will better serve users' needs.

In order to expose and collect new ATP problems, the CADE-18 Problems and Problem Sets Workshop (PaPS-18) will be held on 1 August 2002. This workshop will bring together real ATP system users and developers, in an environment focused on problems and problem sets for ATP systems. Topics of interest include:

• Problems and problem sets generated naturally as part of research or commercial activities.
• Interesting axiomatizations of domains, with corresponding conjectures.
• Problems and problem sets that current state-of-the-art ATP systems cannot solve, but whose solution would have scientific or practical value.
• Problems and problem sets resulting from translation from one logic to another, the translation techniques, the benefits of such translation (e.g., the problems are easier to solve), and the translation of solutions back to the original logic.
• Problems and problem sets that have been solved using special ATP techniques, especially problem sets from applications.

Invited speakers:

• TBA
• TBA

The workshop organizers are Geoff Sutcliffe, Jeff Pelletier and Christian Suttner. If you have any questions about the worksop, please email the organizers.

Submission of papers for presentation at the workshop is now invited. Submissions will be refereed, and balanced program of high-quality contributions will be selected. We are particularly interested in contributions from commercial ATP users.

Submissions can be in PDF or Postscript, with a print area of 16cm x 23cm (6.5in x 9in). There is no page limit, but extremely long listings of problems or computer output should be relegated to a referenced WWW site. All problems and problem sets must be available on the WWW, and the WWW site referenced in the paper.