Typed First-order Logic with Arithmetic (TFA)

• person is a type
• dog is a type
• jon is a person
• hercules is a dog
• owner_of takes a dog argument and returns a person
• bit takes a dog, a person, and an $int arguments and returns boolean
• hates takes two person arguments and returns boolean
• chases takes a person and a dog arguments and returns boolean

• owner_of(hercules) ≠ jon
• bit(hercules,jon,2)
• ∀ D: dog ∀ P: person ∀ N: integer ( ( bit(D,P,N) ∧ N > 1 ∧ owner_of(D) ≠ P ) → hates(P,owner_of(D)) )
• ∀ D: dog ∀ P: person ∀ N: integer ( ( bit(D,P,N) ∧ N > 0 ) → chases(P,D) )

• ∃ D: dog ∃ P: person ( chases(jon,D) ∧ P ≠ jon ∧ hates(jon,P) )

tff(person_type,type,   person: $tType ).
tff(dog_type,type,      dog: $tType ).
tff(jon_decl,type,      jon: person ).
tff(hercules_decl,type, hercules: dog ).
tff(owner_of_decl,type, owner_of: dog > person ).
tff(bit_decl,type,      bit: ( dog * person * $int ) > $o ).
tff(hates_decl,type,    hates: ( person * person ) > $o ).
tff(chases_decl,type,   chases: ( person * dog ) > $o ).

tff(jon_not_owner_of_hercules,axiom,
    owner_of(hercules) != jon ).

tff(hercules_bit_jon_twice,axiom,
    bit(hercules,jon,2) ).

tff(biters_not_owned,axiom,
    ! [D: dog,P: person,N: $int] :
      ( ( bit(D,P,N)
        & $greater(N,1)
        & ( owner_of(D) != P ) )
     => hates(P,owner_of(D)) ) ).

tff(bites_then_chases,axiom,
    ! [D: dog,P: person,N: $int] :
      ( ( bit(D,P,N)
        & $greater(N,0) )
     => chases(P,D) ) ).

tff(jon_chases_hates,conjecture,
    ? [D: dog,P: person] :
      ( chases(jon,D)
      & P != jon
      & hates(jon,P) ) ).