A syntax for typed FOF problems is being developed.
The proposed syntax may be found at
http://www.cs.miami.edu/~tptp/TPTP/TypedFOF.html.
Comments are welcome.
For contributing problems:
Argonne National Laboratory,
AR Research Group at TU München,
Jaroslav Barta,
Dan Benanav,
Woody Bledsoe,
Johan Bos,
Marc Boule,
Koen Claessen,
Simon Colton,
Christian Fermüller,
Tim Geisler,
John Harrison,
Lifeng He,
Ullrich Hustadt,
Thomas Jech,
Boris Konev,
Lars Kulik,
Bill McCune,
Andreas Meier,
Jia Meng,
Johan Martensson,
Dominique Pastre,
David Plaisted,
Larry Paulson,
Art Quaife,
Alberto Segre,
Renate Schmidt,
Stefan Schulz,
John Slaney,
Mark Stickel,
Tanel Tammet,
Bob Veroff,
Christoph Weidenbach,
Christoph Wernhard.
For helping with problems and/or pointing out errors:
Geoff Alexander,
Johan Belinfante,
Woody Bledsoe,
Maria Poala Bonacina,
Heng Chu,
Koen Claessen,
Ingo Dahn,
Damien Doligez,
Matthias Fuchs,
Tim Geisler,
John Harrison,
Thomas Jech,
Harald Ganzinger,
Reinhold Letz,
Thomas Ludwig,
Klaus Mayr,
Bill McCune,
Monty Newborn,
Xumin Nie,
Jeff Pelletier,
Petr Pudlak,
Art Quaife,
Dimitris Raptis,
Piotr Rudnicki,
Len Schubert,
Alberto Segre,
John Slaney,
Mark Stickel,
Bob Veroff,
TC Wang,
Christoph Weidenbach,
Hantao Zhang.
For support regarding the utilities:
Kal Hodgson,
Max Moser,
Gerd Neugebauer,
Paul Tarau,
Abdul Sattar,
Christoph Weidenbach,
Jürgen Zimmer.
For general advice and comments:
Reiner Hähnle,
Reinhold Letz,
Jeff Pelletier,
Mark Stickel.
Further Plans
We have several short and long term plans for further development of the TPTP.
The main ideas are listed here.
General guidelines outlining the requirements for ATP system evaluation
will be produced.
A benchmark suite (the BSTP) will be selected from the TPTP.
The BSTP will be a small collection of problems, and will be a
minimal set of problems on which an ATP system evaluation can be based.
The BSTP will be accompanied by specific guidelines for computing a
performance index for an ATP system.
Solutions to TPTP problems from contemporary ATP systems are being
collected for distribution alongside a forthcoming TPTP release.
The TPTP may be extended to include problems expressed in non-classical
and higher order logics.
Acknowledgements
We are indebted to the following people and organizations who have
helped with the construction of the TPTP.