The 8thTPTP Tea Partywill 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 |
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):
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.
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) )
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?
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.