Typed First-order Form

Typed First-order Form (TFF)

• Types, type signatures, typed quantification
• Formulae must be correctly typed
• Makes arithmetic possible

Monomorphic TFF (TF0)

• Types ... $i, $o, $int, $rat, $real, declared types - $tType
• Type signatures ... types, function types, predicate types
• Polymorphic equality and arithmetic
• Default typing ... FOF!
• ATP systems ... cvc5, E, Vampire, etc.
• Example (as a plain file)

  tff(dog_type,type,      dog: $tType ).     tff(human_type,type,    human: $tType ).
  tff(odie_decl,type,     odie: dog ).       tff(jon_decl,type,      jon: human ).
  
  tff(owner_of_decl,type, owner_of: dog > human ).
  tff(bit_decl,type,      bit: (dog * human * $int) > $o ).
  tff(hates_decl,type,    hates: (human * human) > $o ).
  
  tff(jon_owns_odie,axiom,                   tff(odie_bit_jon_twice,axiom,
      jon = owner_of(odie) ).                    bit(odie,jon,2) ).
  
  tff(another_dog_bit_jon_twice,axiom,       tff(hate_the_multi_biter_dog,axiom,
      ? [D: dog] :                               ! [D: dog,H: human,N: $int] :
        ( D != odie                                ( ( H != owner_of(D)
        & jon != owner_of(D)                         & bit(D,H,N)
        & bit(D,jon,2) ) ).                          & $greater(N,1) )
                                                  => hates(H,owner_of(D)) ) ).
  tff(jon_hates_another_human,conjecture,
      ? [H: human] :
        ( H != jon
        & hates(jon,H) ) ).
  

Polymorphic TFF (TF1)

• Types ... TF0, type constructors, type variables
• Type signatures ... TF0, !> polymorphic signatures
• Types provided for uses of polymorphic symbols
• ATP systems ... Alt-Ergo, Leo-III, Vampire, Zipperposition, etc.
• Example (as a plain file)

  tff(dog_type,type,      dog: $tType ).       tff(human_type,type,    human: $tType ).
  tff(biter_type,type,    biter: $tType > $tType ).
  tff(odie_decl,type,     odie: biter(dog) ).  tff(jon_decl,type,      jon: human ).
  
  tff(owner_of_decl,type, owner_of:
      !>[BiterType: $tType]: (biter(BiterType) > human ) ).
  tff(bit_decl,type,      bit:
      !>[BiterType: $tType]: ( (biter(BiterType) * human * $int) > $o ) ).
  tff(hates_decl,type,    hates: (human * human) > $o ).
  
  tff(jon_owns_odie,axiom,                   tff(odie_bit_jon_twice,axiom,
      jon = owner_of(dog,odie) ).                bit(dog,odie,jon,2) ).
  
  tff(another_dog_bit_jon_twice,axiom,       tff(hate_the_multi_biter_any,axiom,
      ? [D: biter(dog)] :                        ! [T: $tType,B: biter(T),
        ( D != odie                                           H: human,N: $int] :
        & jon != owner_of(dog,D)                   ( ( H != owner_of(T,B)
        & bit(dog,D,jon,2) ) ).                      & bit(T,B,H,N)
                                                     & $greater(N,1) )
  tff(jon_hates_another_human,conjecture,         => hates(H,owner_of(T,B)) ) ).
      ? [H: human] :
        ( H != jon
        & hates(jon,H) ) ).