The 8th TPTP Tea Party will be held in room 243 in the Jupiter building at 1:30pm on Friday 11th August 2017 at the 26th International Conference on Automated Deduction 6-11th August 2017

• The TPTP problem library
• The TSTP solution library
• The TPTP syntax
• The TPTPWorld software package
• etc

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 organizers are Geoff Sutcliffe, Stephan Schulz. People who have confirmed that they will attend are: Simon Cruanes, Pascal Fontaine, Mario Frank, Evgeny Kotelnikov, Stephan Schulz, Geoff Sutcliffe.

The topics for this year are (so far - please email me if you have more):

---

1. The TCF language.
   Typed first-order Clausal Form is TF0 in which the formulae are in CNF. It was requested by Giles and Kostya, and they are happy.

   ---

2. Tuples.
   Tuples have been floating around in the TPTP languages, unused, for a while. Tuples are now back, and two forms are used:
   • Tuples in []s. These are used in THF for tuples of terms of which at least one is of type $o (i.e., "statements").
   • Tuples in {}s. These are used in THF and TFF (and potentially FOF) for tuples of terms of any type other than $o (i.e., "objects").

   ---

3. The TFO/TFX language.
   Evgeny's FOOL logic is an extension of TFF that allows terms of type $o, e.g., ...

       tff(a_type,type,a: $i).
       tff(f_type,type,f: $o > $i).
       tff(p_type,type,p: ($i * $o) > $o).
       tff(an,axiom,! [X:$o] : p(f(X),! [Y:$i] : p(a,Y))).
   

   He has a translator to plain FOF. Currently we are coping with this in the THF context, but there are some flaws with that approach, e.g., the type declaration p_type would declare p to take one argument that is a product type, and also the whole construction relies on the TPTP syntax that allows applications to be written in first-order style (e.g., p(a,Y) rather than p @ a @ Y). I propose introducing a new TPTP language fragment called TFO (Typed First-order with bOolean terms) or TFX (Typed First-order eXtended), that allows terms of type $o, but type declarations in the TFF idiom (no product types). This will also be useful for modal logic, as discussed below.

   I will probably need to split up the BNF file to make this work, due to conflicts between THF, TFX, and FOF.

   ---

4. $let, $ite, $let_tf, $let_ff, $let_ft, $let_tt, $ite_f, and $ite_t.
   The status of these two constructs has been unclear in the TPTP. At present $let and $ite are part of THF, and the '_xx' variants part of TFF.
   • In order to simplify things, I suggest we get rid of the '_xx' variants, and have plain $let and $ite in the TFO/TFX language. (It would be possible to also leave the '_xx' variants in plain TFF.)
   • The type of the defined symbol in $let currently has to be inferred. I propose we extend the syntax to include a new first argument that explicitly provides the type.
   • In order to bring THF $let into line with most functional programming languages, lambda terms will be used. OK?
   • Example

     THF: $let(FF: $int > $int > $i,
               FF := ^[X:$int,Y:$int]: ( f @ X @ X @ Y @ Y) ),
               FF @ a @ b)
     
     TFX: $let(ff: ($int * $int) > $i,
               ! [X:$int,Y:$int] : ( ff(X,Y) := f(X,X,Y,Y) ),
               ff(a,b) )
     

   • []s are used to do a parallel let, e.g.,

     TF0: $let([ff: ($int * $int) > $i, gg: ($int > $int)],
               [! [X:$int,Y:$int] : ( ff(X,Y) := f(X,X,Y,Y) ),! [X:$int] : ( gg(X) := X)],
               ff(gg(a),b) )
     

     Is this really useful? Should it be let*? How can we leverage tuples for this?

   ---

5. Modal logic (and beyond)
   Christoph Benzmueller, Tobias Gleißner, and I have been working on TPTP language extensions for modal (and other non-classical) logic. Currently the work has been in the higher-order context, and is written up here. In order to use these ideas at the first order level, I propose we use the TFO/TFX language (see above). This will allow the use of @ to apply symbols of type $o > $o (specifically modal operators). So this would be legal ...

       tfo(q_type,type,q: $i > $o).
       tfo(an,axiom,$box @ ! [X:$i] : q(X)).
   

   TFO/TFX is actually too strong, because it allows all terms to be of type $o, while modal logic requires only that the modal operators be allowed to take arguments of type $o. But it's not out of hand. For typed higher-order modal logic, THF is just fine.

   ---

6. CASC LTB division - Quo vadis?
   

   ---