The 7th

TPTP Tea Party

will be held 10:00am on Thursday 4th August at the

23rd International Conference on Automated Deduction
July-August 2011

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. TPTP general
    1. 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)).
    2. 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>)
      • Andrei has an opinion
    3. 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.
    4. 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.
    5. Stephan: How to print several statuses in SZS.
  2. TFF/TFA
    1. 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.
    2. 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.
    3. Christoph Weidenbach: SMT-LIB style metasyntax, compatibility with SMT-LIB, supporting (inductive) theories.
    4. Geoff: $kind instead of/as an alternative to $tType.
  3. THF
    1. 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:

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