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
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
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
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