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:
- 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)
- 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)
- 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)
- 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)
- 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[@]cs.miami.edu).
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[@]cs.miami.edu) 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.
Organization
The TPTP Tea Party will be organized as follows:
- Discussions, Monday 3rd August, 2:00pm
- We'll start with minor issues, as some important people will
be attending workshops or tutorials.
- The primary topics, "typed first-order problems" and "problems
with integer arithmetic", will be discussed from 3:00pm.
- Refreshments, as soon as discussions are productive.
Participation is free.
The organizer is
Geoff Sutcliffe,
Confirmed participants are:
Tea Party Pictures
