The goal of this document is to:
tff(food_type,type,
food: $tType ).
tff(fruit_type,type,
fruit: $tType ).
tff(list_type,type,
list: $tType ).
Declaration of atomic types is not required, i.e., atomic types can be
introduced on the fly.
TPTP problems will have all atomic types declared, so as to provide a
typo check.
tff(cons_type,type,
cons: (fruit * list) > list ).
tff(is_empty_type,type,
isEmpty: list > $o ).
The range type of a function must be an atomic type, and cannot be
$o.
The range type of a predicate must be $o.
Note that symbols of arity greater than one use the * for
a cross-product type.
Currying is not possible, i.e., the first example above cannot be
written
tff(cons_type,type,
cons: fruit > list > list ).
If a symbol's type is declared more than once, and the types are not the same, that's an error.
tff(list_not_empty,axiom,
! [X: fruit,Xs: list] : ~isEmpty(cons(X,Xs)) ).
tff(one_type_decl,type,
one_type: $tType ).
produces the axiom:
fof(one_type_inhabited,axiom,
? [X] : one_type(X) ).
It is unnecessary to produce axioms that say the terms with
different atomic types are unequal (reflecting the fact that
atomic type domains are disjoint) because it is impossible to
claim they are equal in a well-typed formula.
tff(f_type,type,
f: (t1 * ... * tn) > tf ).
is translated into:
fof(f_type,axiom,
! [X1,...,Xn] : tf(f(X1,...,Xn)) ).
It is unnecessary to have an implication with the antecedent
checking the types of the arguments X1,...,Xn because
it is impossible to use incorrectly typed arguments in a
well-typed formula.
! [X1: t1,...,Xn: tn] : p(X1,...,Xn)is translated into:
! [X1,...,Xn] :
( ( t1(X1)
& ...
& tn(Xn) )
=> p(X1,...,Xn) )
Geoff thinks that for problems that do not contain equality it is
unnecessary to have an implication with the antecedent checking the
types of the arguments X1,...,Xn because they could never
become instantiated to a term of the wrong type in a wel-typed
problem.
If equality is present the check is necessary because of
paramodulation, either into those variables (most ATP systems won't
do that), or paramodulation from a variable of another type.
The latter is a case that needs to be checked in a system that deals
with TFF natively.
? [X1: t1,...,Xn: tn] : p(X1,...,Xn)is translated into:
? [X1,...,Xn] :
( t1(X1)
& ...
& tn(Xn)
& p(X1,...,Xn) )
| The next section is a developmental idea that should be ignored except by Geoff and other TPTP developers. |
tff(one_type_decl,type,
one_type: $tType ).
produces the axiom:
fof(one_type_inhabited,axiom,
? [X] : one_type(X) ).
tff(one_type_decl,type,
one_type: $tType ).
tff(another_type_decl,type,
another_type: $tType ).
produce the axiom:
fof(one_type_not_another_type,axiom,
! [X,Y] :
( one_type(X)
=> ~ another_type(X) ) ).
tff(f_type,type,
f: (t1 * ... * tn) > tf ).
is translated into:
fof(f_type,axiom,
! [X1,...,Xn] :
( ( t1(X1)
& ...
& t2(Xn) )
<=> tf(f(X1,...,Xn)) ) ).
tff(p_type,type,
p: (t1 * ... * tn) > $o )..
is translated into:
fof(p_type,axiom,
! [X1,...,Xn] :
( ( t1(X1)
& ...
& t2(Xn) )
<= p(X1,...,Xn) ) ).
! [X1: t1,...,Xn: tn] : p(X1,...,Xn)is translated into:
! [X1,...,Xn] :
( ( t1(X1)
& ...
& tn(Xn) )
=> p(X1,...,Xn) )
? [X1: t1,...,Xn: tn] : p(X1,...,Xn)is translated into:
? [X1,...,Xn] :
( t1(X1)
& ...
& tn(Xn)
& p(X1,...,Xn) )
%----Type declarations tff(australian,type, australian: $tType ). tff(russian,type, russian: $tType ). tff(vodka,type, vodka: $tType ). tff(geoff,type, geoff: australian ). tff(andrei,type, andrei: russian ). tff(smirnoff,type, smirnoff: vodka ). tff(rotgut,type, rotgut: vodka ). tff(drink_of,type, drink_of: russian > vodka ). tff(tasty,type, tasty: vodka > $o ). tff(trueblue,type, trueblue: australian > $o ). %----Ill-typed conjectures tff(geoff_vodka,conjecture, vodka(drink_of(geoff)) ). tff(tasty_australian,conjecture, ? [X: australian] : tasty(X) ). tff(tasty_geoff,conjecture, tasty(geoff) ). tff(tasty_drink_of_geoff,conjecture, tasty(drink_of(geoff)) ). tff(geoff_rotgut,conjecture, drink_of(geoff) = rotgut ). tff(trueblue_andrei,conjecture, trueblue(andrei) ). tff(geoff_andrei,conjecture, geoff = andrei ). tff(drink_of_andrei_russian,conjecture, drink_of(andrei) = geoff ).In the weak translation the first conjecture can be proved, and none of the others can be disproved (their negations proved) ...
fof(australian,axiom, ? [X] : australian(X) ). fof(russian,axiom, ? [X] : russian(X) ). fof(vodka,axiom, ? [X] : vodka(X) ). fof(geoff_australian,axiom, australian(geoff) ). fof(andrei_russian,axiom, russian(andrei) ). fof(smirnoff_vodka,axiom, vodka(smirnoff) ). fof(rotgut_vodka,axiom, vodka(rotgut) ). fof(drink_of_russian,axiom, ! [X] : vodka(drink_of(X)) ). %----Can prove this weird thing fof(geoff_vodka,conjecture, vodka(drink_of(geoff)) ). %----Cannot prove (they are CSA) these negated weird things (but also cannot %----prove their unnegated form, like the one above). fof(tasty_australian,conjecture, ~ ? [X] : ( australian(X) & tasty(X) )). fof(tasty_geoff,conjecture, ~ tasty(geoff) ). fof(tasty_drink_of_geoff,conjecture, ~ tasty(drink_of(geoff)) ). fof(geoff_rotgut,conjecture, drink_of(geoff) != rotgut ). fof(trueblue_andrei,conjecture, ~ trueblue(andrei) ). fof(geoff_andrei,conjecture, geoff != andrei ). fof(drink_of_andrei_russian,conjecture, drink_of(andrei) != geoff ).In the strong translation all of the conjectures can be disproved (their negations can be proved) ...
fof(australian,axiom, ? [X] : australian(X) ). fof(russian,axiom, ? [X] : russian(X) ). fof(australian_not_russian,axiom, ! [X] : ( australian(X) => ~ russian(X) ) ). fof(vodka,axiom, ? [X] : vodka(X) ). fof(australian_not_vodka,axiom, ! [X] : ( australian(X) => ~ vodka(X) ) ). fof(russian_not_vodka,axiom, ! [X] : ( russian(X) => ~ vodka(X) ) ). fof(geoff_australian,axiom, australian(geoff) ). fof(andrei_russian,axiom, russian(andrei) ). fof(smirnoff_vodka,axiom, vodka(smirnoff) ). fof(rotgut_vodka,axiom, vodka(rotgut) ). fof(drink_of_russian,axiom, ! [X] : ( russian(X) <=> vodka(drink_of(X)) ) ). fof(vodka_tasty,axiom, ! [X] : ( tasty(X) => vodka(X) ) ). fof(australian_trueblue,axiom, ! [X] : ( trueblue(X) => australian(X) ) ). %----These can all be proved - they are the negations of ill-typed TFF fof(geoff_vodka,conjecture, ~ vodka(drink_of(geoff)) ). fof(tasty_australian,conjecture, ~ ? [X] : ( australian(X) & tasty(X) ) ). fof(tasty_geoff,conjecture, ~ tasty(geoff) ). fof(tasty_drink_of_geoff,conjecture, ~ tasty(drink_of(geoff)) ). fof(geoff_rotgut,conjecture, drink_of(geoff) != rotgut ). fof(trueblue_andrei,conjecture, ~ trueblue(andrei) ). fof(geoff_andrei,conjecture, geoff != andrei ). fof(drink_of_andrei_russian,conjecture, drink_of(andrei) != geoff ).A theorem to be proved:
Yikes, here's a FOF conjecture that can be proved in the strong translation, cannot be proved in the weak translation, and cannot be expressed in TFF.
fof(non_russian,conjecture, ? [X] : ~ russian(X)).
| The following sections summarize relatively well-known features and
options of type systems that we considered when putting this proposal together. |
tff(a_type,type,a: animal).
tff(b_type,type,b: integer).
tff(has_4_legs_type,type,has_4_legs: animal > $o).
tff(some_integer_animal,axiom,a = b).
tff(a_has_4_legs,axiom,has_4_legs(a)).
tff(b_has_4_legs,plain,has_4_legs(b),inferred(paramodulation ...
To overcome this problem would require either multiple equality symbols
or polymorphic equality (see below).
If equations are permitted only between terms of the same type then
a formula has a model with non-disjoint type domains iff it has a model
with disjoint type domains. So, you can consider only models with
disjoint type domains if you want. It makes no difference. (Thanks
to Cesare Tinelli)
a: $i; f: fruit; ifun: $i -> $i; fruitfun: fruit -> fruit; a = f ifun(f) fruitfun(a)
Theorem provers: TODO. Reference: SPASS and soft typing.
Model finders have an easier task to find typed models, as long as the domains of the separate types are as most as large as the domain of the untyped version of the problem. This is the case for the first proposal, but definitely not for the second.