The CADE-18 Problems and Problem Sets Workshop

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.

• PaPS accepted papers
• PaPS program
• Participant list for PaPS

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!

Submissions

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 <geoff@cs.miami.edu>.

Invited speakers

• John Harrison, Intel, USA
  joint with RADM: Extracting test problems from real applications
• Johann Schumann, NASA Ames, USA
  Using automated theorem provers? using automated theorem provers!

Panel

• Peter B. Andrews, Carnegie Mellon U, USA; Alan Bundy, U Edinburgh, UK; William McCune, Argonne National Laboratory, USA; and Rick Sommer, Stanford U, USA
  joint with RADM: Challenge problems for automated deduction (with special emphasis on mathematics)

Organizers

• Geoff Sutcliffe <geoff@cs.miami.edu>, U Miami, USA
• Jeff Pelletier <jeffp@cs.ualberta.ca>, U Alberta, Canada
• Christian Suttner <email@csuttner.de>, Cirrus Management, Germany