The 6th

TPTP Tea Party

will be held on Monday 3rd August, after lunch, at the

22nd International Conference on Automated Deduction
August 2009

This meeting will bring together developers and users of TPTP related resources, including (but not limited to):

The meeting aims to elicit feedback, suggestions, criticisms, etc, of these resources, in order to ensure that their continued development meets the needs of successful automated reasoning. The meeting will be structured discussion following an agenda of topics that have been suggested and agreed upon in advance. The topics so far are:

  1. The next planned major development in the TPTP is the addition of problems with arithmetic, as typed first-order problems in the TFF language. These are bold steps, in the idiom of the LPAR mission. Will developers adapt their systems to these problems? (Geoff's item)

  2. Should we add the definition operator := to the first-order languages? It is part of the THF language (in the THFX layer). It would also be useful for recording oriented equalities in equational reasoning, e.g., Waldmeister's TPTP format derivations. (Geoff's item)
  3. Should we add the sequent operator --> to the first-order languages? It is part of the THF language (in the THFX layer). It would be useful for recording natural deduction proofs. (Geoff's item)

  4. How can we generalize the Problem Status such that it can contain everything we currently know about a problem, without necessarily being complete information about a problem? Examples are "has a finite model", "has an infinite counter model", "has no finite model", "has only infinite models", "has no models", "has no finite counter models", etc. Some of these can be true simultaneously, breaking the barrier of Problem Status and Substatus. (Koen's item)

  5. Recently the TPTP was extended to higher-order logic, and further extensions such as polymorphism and sorted first-order logic are planned. This raises two principal concerns. Firstly, type-checking is no longer trivial and can thus not be handled by a context-free grammar anymore. Secondly, it is unclear if and in what way the first-order language of TPTP can be semantically embedded into the extended languages. For the former problem, type-checking was borrowed from the Edinburgh Logical Framework LF by representing TPTP's higher-order logic in LF. This topic is to discuss expanding on this approach using LF to represent TPTP's first-order logic and systems from the lambda cube, and relate them to each other. The aim is to yield a general recipe how TPTP can be extended to other logics in a way that preserves the simplicity of TPTP while precisely defining its semantics. (Florian's item)
Further topics may be proposed by emailing Geoff Sutcliffe (geoff[@]

The 1st TPTP Tea Party was in London in 2004. The 2nd TPTP Tea Party was in Tallin in 2005. The 3rd TPTP Tea Party was in Seattle in 2006. The 4th TPTP Tea Party was in London in 2007. The 5th TPTP Tea Party was in Sydney in 2008.

Participation and Position Statements

In order to participate, you must be a registered TPTP user (email Geoff Sutcliffe (geoff[@] to be added to this list), and must submit a position statement about at least one of the agenda topics. Each position statement must be a separate HTML web page, and must conform roughly to the style of this sample page (copy the source and make your changes). Position statements must be emailed to Geoff by 31st July.


The TPTP Tea Party will be organized as follows:

Participation is free.

The organizer is Geoff Sutcliffe,

Confirmed participants are:

Tea Party Pictures