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:

TPTP general

Geoff: "Distinct objects" and $distinct will start to appear in
problems of TPTP v5.3.0.
 "Apple" != "Microsoft" is implicit
 fof(first_names,axiom,$distinct(geoff,stephan,chris)).
fof(family_names,axiom,$distinct(sutcliffe,schulz,benzmueller)).

Geoff: FOFX  should we start using it?
FOFX is the extended FOF syntax, including ... <fof_let> ::= := [<fof_let_list>] : <fof_unitary_formula>
<fof_let_list> ::= <fof_defined_var> 
<fof_defined_var>,<fof_let_list>
<fof_defined_var> ::= <variable> := <fof_logic_formula> 
<variable> : <term>  (<fof_defined_var>)
<fof_conditional> ::= $itef(<fof_logic_formula>,<fof_logic_formula>,
<fof_logic_formula>)
<fof_sequent> ::= <fof_logic_formula> <gentzen_arrow>
<fof_logic_formula>  (<fof_sequent>)
%Conditional terms should not be used by THF. Use $itett in the TFF
%context and $itetf in the FOF/CNF context. $itetf is part of FOFX.
<conditional_term> ::= $itett(<tff_logic_formula>,<term>,<term>) 
$itetf(<fof_logic_formula>,<term>,<term>)

Geoff, Chad Brown, Chris Benzmüller: Definitions.
The TPTP "definition" role has been intended to be a way for users to
indicate that the formula is intended to somehow define a symbol. The
formulae are often equations, e.g., ... thf(a,definition,p = ^ [X: $i] : q @ X ).
fof(a,definition,! [X] : f(X) = g(a,X) ).
... or equivalences, e.g., ... tff(a,definition,! [X: human] : eating(X) <=> (has_food(X) & chewing(X)) ).
So far definitions have been used only in THF problems, but they are
available in TFF and FOF.
Definitions can be treated just like axioms, but the user's intention
is often a useful hint about how to treat the formula. Chad Brown has
expressed some concern about the unconstrained nature of definition
formulae. He has proposed that either definitions be removed
(changed to axioms), or the nature of definitions should be more
formally stated.
There seem to be three possibilties:
 Change definitions to axioms, and thus expect ATP systems to
analyse axioms to determine if they should be treated as
definitions.
 The status quo. This also admits the possibility of ATP systems
ignoring the "definition" role, treating them as axioms, and
then doing the analysis as in 1.
 Formally state what a definition can be, and have a tool to
check that definitions meet the criteria (much akin to type
checking). The formal statement would need to be agreed upon
by all/most users.

Chris Benzmüller: System versioning.
We should discuss system versioning, and how we can assure that
experiments, e.g., with the SystemOnTPTP infrastructure become
maximally reproducable.

Stephan: How to print several statuses in SZS.

TFF/TFA

Koen Claessen: $quotient.
I hear you saying: The danger is that if you implement arithmetic
wrong, it gets all wrong!
What is the point you want to make?
Dealing with / in the same way as we already deal with functions like
head is the simplest way to go IMO.
Geoff: I do like "allow x / 0 but not constrain it to be anything"
 it gives you more models and hence less theorems. Soundness is
retained. Hence we could add $quotient.

Peter Baumgartner: Adhoc polymorphism over atomic types.
What about allowing adhoc polymorphism over atomic types?
Are there reasons to not include it (beyond equality) in the
first place?
Geoff: It's too late to add more to the TFF0 core (it was
released in TPTP v5.0.0), but certainly we should discuss features
to add in the full TFF.

Christoph Weidenbach: SMTLIB style metasyntax, compatibility with
SMTLIB, supporting (inductive) theories.

Geoff: $kind instead of/as an alternative to $tType.

THF

Chris Benzmüller: Type constraints for terms.
Larry Paulson commented "And this reminds me, according to
Nik, THF provides no simple way of attaching a type constraint to
a term, the equivalent of t::T in ML. I gather that you have to
introduce a dummy identity function and write some thing like
(lambda x::T)t. Tolerable but not ideal."
In the long run we may want to support such type constraints.
If no one complains we can add it to the THF syntax.
It will require an adaptation of some TPTP support tools.
Further topics may be proposed by emailing Geoff Sutcliffe
(geoff[@]cs.miami.edu).
Participation and Position Statements
In order to participate, you must be a
registered TPTP user (email Geoff Sutcliffe
(geoff[@]cs.miami.edu) to be added to this list).
Please let Geoff know if you will attend, so we can plan the catering.
Organization
The TPTP Tea Party will be organized as follows:
 Discussions, Thursday 4th August, 10:00am
 Refreshments, as soon as discussions are productive.
Participation is free.
The organizers are
Geoff Sutcliffe,
Chris Benzmüller.
Confirmed participants are:
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.
The 6th TPTP Tea Party
was in Montreal in 2009.
Tea Party Pictures