Typed First-order Form

The TFF Language

• Syntactically conservative extension of FOF language (Prolog-like)
• Defined types $i, $o, $tType
• Ad-hoc polymorphic equality
• Explicit and default typing of all symbols
• Example

  tff(taught_by_type,type,(
      taughtby: ( student * professor ) > $o )).
  
  tff(coordinator_of_type,type,(
      coordinatorof: course > professor )).
  
  tff(student_enrolled_axiom,axiom,(
      ! [X: student] :
      ? [Y: course] : enrolled(X,Y) )).

• Translation to FOF in TPTP2X

Adding Arithmetic

• Defined types (unbounded, infinite precision):
  $int, $rat, $real
• Numeric constants:
  1234, -4321, 123/456, -321/654, 123.456, -321.654, 123.456E78, -321.654e-87
• Defined functions (ad hoc polymorphic over the types):
  $uminus, $sum, $difference, $product, $quotient, $quotient_?, $remainder_? (? = e, t, f)
  $floor, $ceiling, $truncate, $round $to_int, $to_rat, $to_real
• Defined predicates (ad hoc polymorphic over the types):
  $less, $lesseq, $greater, $greatereq,
  $is_int, $is_rat
• Example

  tff(recursive_fib_sort,axiom,(
      ! [X: $int,Y: $int,Z: $int,R: list] :
        ( ( $less(X,Y)
          & $greatereq(Z,$sum(X,Y))
          & fib_sorted(mycons(Y,mycons(Z,R))) )
       => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )).
  
  tff(check_list,conjecture,(
      fib_sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) )).

TPTP Problems

• First release: TPTP v5.0.0 - September 2010
• Non-arithmetic problems: COM, GEO, KRS, PUZ
• Arithmetic problems: ARI, DAT, GEG, HWV, MSC, NUM, PUZ, SET, SWV, SYN