The 2nd

TPTP Tea Party

will be held at

The 20th International Conference on Automated Deduction
23rd July 2005
(in the afternoon)

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

The workshop 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 workshop will be structured discussion following an agenda of topics that have been suggested and agreed upon in advance. The topics so far are:

  1. A TPTP syntax for models, as output by finite model generators, and also in other forms.

  2. The semantics of the formula types (i.e., axiom, lemma, negated_conjecture, etc - see the <user type> entry in the syntax BNF) in the TPTP syntax. For example, should a lemma be required to be a logical consequence of the axioms?

  3. The use of 'quoted' predicate and function symbols. For example, should
         'I am a funky predicate!'(of,'2 arguments')
    be allowed in the TPTP syntax?

  4. An XML format for TPTP
Further topics may be proposed by emailing Geoff Sutcliffe (geoff[@]

The 1st TPTP Tea Party was in London in 2004.

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 at least one position statement addressing one of the agenda items. Each position statement must be a separate page, and must conform roughly to the format produced by LaTeX with the following header:

\textwidth  14.63cm
\textheight 22cm
\oddsidemargin  0.65cm
\evensidemargin 0.65cm
\topmargin  0.55cm
\headheight 0.0pt
\headsep    0.0pt
Position statements in PDF must be emailed to Geoff Sutcliffe (geoff[@], by 4th July (so that the entire USA can celebrate the submissions :-). Every submission will be accepted unless it's way off topic, in which case we'll help you get it right.


The TPTP Tea Party will be a half day workshop organized as follows:

Participation is free, but you pay for your own dinner, lunch, beer, accomodation, etc.

The workshop organizers are Geoff Sutcliffe, and Josef Urban.

Confirmed participants are:

Tea Party Pictures