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

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 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:
  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.
  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?


7th TPTP Tea Party was in Wroclaw in 2011. The 6th TPTP Tea Party was in Montreal in 2009. The 5th TPTP Tea Party was in Sydney in 2008. The 4th TPTP Tea Party was in London in 2007. The 3rd TPTP Tea Party was in Seattle in 2006. The 2nd TPTP Tea Party was in Tallin in 2005. The 1st TPTP Tea Party was in London in 2004.

Tea Party Pictures