Typed eXtended First-order form

Typed eXtended First-order form (TXF)

• FOOL formulae ... formulae as terms, Boolean variables
• FOOL terms ... tuples, conditionals, let expressions
• Can be translated to TFF/FOF

Monomorphic TXF (TX0)

• ATP systems ... E, Leo-III, Vampire, Zipperposition, 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(feeds_decl,type,    feeds: (human * dog) > $o ).
  tff(chases_decl,type,   chases: (human * dog) > $o ).
  tff(says_decl,type,     says: (human * $o) > $o ).
  
  tff(jon_owns_odie,axiom,                   tff(odie_bit_jon_twice,axiom,
      jon = owner_of(dog,odie) ).                bit(dog,odie,jon,2) ).
  
  tff(hate_the_multi_biter_dog,axiom,        tff(feed_the_non_biter_dog,axiom,
      ! [D: dog,H: human,N: $int] :              ! [D: dog,H: human] :
        ( ( H != owner_of(D)                       $ite(
          & bit(D,H,N)                               ? [N: $int] :
          & $greater(N,1) )                            ( bit(D,H,N) & $greater(N,0) ),
       => hates(H,owner_of(D)) ) ).                  chases(H,D),
                                                     feeds(H,D)) ).
  tff(jon_says_a_dog_bit_him_twice,axiom,
      ? [D: dog] :                           tff(jon_says_truth,axiom,
        ( D != odie                              ! [S: $o] :
        & jon != owner_of(D)                       ( says(jon,S)
        & says(jon,bit(D,jon,2)) ) ).             => S ) ).
  
  tff(jon_chases_and_hates,conjecture,
      ? [D: dog,H: human] :
        ( chases(jon,D)
        & H != jon
        & hates(jon,H) ) ).
  

Polymorphic TXF (TX1)

• ATP systems ... Leo-III, Vampire, 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(feeds_decl,type,    feeds: (human * biter(dog)) > $o ).
  tff(chases_decl,type,   chases: (human * biter(dog)) > $o ).
  tff(says_decl,type,     says: (human * $o) > $o ).
  
  tff(jon_owns_odie,axiom,                   tff(odie_bit_jon_twice,axiom,
      jon = owner_of(dog,odie) ).                bit(dog,odie,jon,2) ).
  
  tff(hate_the_multi_biter_any,axiom,        tff(feed_the_non_biter_dog,axiom,
      ! [T: $tType,B: biter(T),                  ! [D: biter(dog),H: human] :
                   H: human,N: $int] :             $ite(
        ( ( H != owner_of(T,B)                       ? [N: $int] :
          & bit(T,B,H,N)                               ( bit(dog,D,H,N) & $greater(N,0) ),
          & $greater(N,1) )                          chases(H,D),
       => hates(H,owner_of(T,B)) ) ).                feeds(H,D)) ).
  
  tff(jon_says_a_dog_bit_him_twice,axiom,    tff(jon_says_truth,axiom,
      ? [D: biter(dog)] :                        ! [S: $o] :
        ( D != odie                                ( says(jon,S)
        & jon != owner_of(dog,D)                  => S ) ).
        & says(jon,bit(dog,D,jon,2)) ) ).
  
  tff(jon_chases_and_hates,conjecture,
      ? [D: biter(dog),H: human] :
        ( chases(jon,D)
        & H != jon
        & hates(jon,H) ) ).