The Good New Days
The TPTP solves all that ...
- On the internet
- Comprehensive
- Diversity of subject matters
- Large enough
- Specifically designed languages
- Problems of varying difficulty
Tuned for a particular ATP system
The TPTP solves all that ...
- Independent of ATP systems
The TPTP solves all that ...
- Documents each problem
- Difficulty ratings for each problem
- Statistics for each problem
- Statistics for the library as a whole
The TPTP solves all that ...
- Unambiguous naming scheme
- Well structured and documented
The TPTP solves all that ...
- Up-to-date
- Axiomatizations
- Distributes new problems
- Corrects errors in existing problems
- Centralizes maintenance efforts
The TPTP solves all that ...
- Recommendations for correct use