PaPS 2002

Problem and Problem Sets for ATP
Copenhagen, Denmark, July 31st - August 1st, 2002
Affiliated with CADE-18

The CADE-18 Problems and Problem Sets Workshop

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 to 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, 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.

This year's workshop will be limited to problems in propositional and first order logic (including translation from higher order logics to propositional and first order form). There will be no limitation to classical logics - problems and problem sets in other logics, e.g., modal and relevance logics, are of interest, provided that there are ATP systems that can attempt to solve them. The problems and problem sets will be made available online in TPTP format, thus making them easily accessible to ATP system developers as challenge problems.

Changed program!

PaPS will thus run from midday, Wednesday 31 July to midday, Thursday 1 August. The afternoon sessions on Wednesday will be shared with RADM. Note that the registration fee includes lunch on Thursday but not on Wednesday!


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. Submissions must be emailed to Geoff Sutcliffe <>.

Invited speakers