Expansion and Modernisation of the TPTP World

[Geoff Sutcliffe]

HI everyone,

Thanks for joining TPTP World Google Group! One of the reasons I created the group is to keep you informed, and to get your feedback, on things I am planning for the TPTP over the next few years ... provided I get the grant that I have submitted to the NSF (and if I don't get the grant, I hope to be able to do much of this anyway, now I'm no longer department chair and have much more research time). The grant is for "Expansion and Modernisation of the TPTP World". Here's the summary of my plans (extracted from the proposal) ...

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.

Cheers,

Geoff

[Geoff Sutcliffe]

Hi all,

Sadly, the NSF has declined this proposal. This decision will have a downstream impact on what I will be able to do with TPTP World in the coming years. It will also impact the operation of StarExec Miami. To help plan for the future, this proposal, and the future of the TPTP, will be discussed in a presentation at the ARCADE workshop at CADE-28 this year. If you are interested, or have ideas (especially how I can fund the TPTP World), please attend ARCADE! There will also be a TPTP Tea Party after ARCADE, to discuss he more technical details of what I am planning to get done in the TPTP World anyway ... more details in a future posting.

Cheers,

Geoff