The TPTP World will be expanded to add new features, logics, and services, e.g., non-classical logics and the use of machine learning in ATP. The TPTP World will be modernised to take advantage of new technologies, to improve access to and use of the TPTP World. The server that provides access to the TPTP World data and online services will be upgraded to handle the expanded TPTP World, in a configuration that will also support development of the TPTP World. The expansion and modernisation of the TPTP World will enable it to continue its role of providing enabling infrastructure in this technologically important field, with national and international impact.
There will be three aspects to the enhancement of the infrastructure:
Libraries. The existing TPTP and TSTP libraries will be expanded and modernised [this includes moving the TPTP World onto GitHub], and a new library, the TDTP data library, will be added to support research and development of machine learning in ATP.
New Logics. Three new logics/logic families will be added to the TPTP World. These are the extended typed first-order logic, modal logics, and multi-valued logics.
User Services. The various TPTP World tools that are used to manipulate and query the TPTP World data, and services that provide (online) access to the TPTP World, will be expanded and modernised.
If funded, Ruzica Piskac will be working with me as the project's "Community Outreach Director" (the ComODir, which makes sense for someone from Yale :-). She will help keep you informed of progress, solicit feedback from you, and most importantly convene biannual TPTP Tea Parties!
If you would like more details let me know. Otherwise just stay tuned. Right now I'm starting to work with Alex Steen on the modal logic component, and we're making progress.