Typed First-order Logic with Arithmetic (TFA)

New logic features

• $int, $rat, $real types
• Arithmetic functions and predicates
• Arithmetic variables

Problem

• Axioms
  • Jon is not the owner of Hercules.
  • Hercules bit Jon twice!
  • If a dog bites a person more than once, and (s)he is not the owner of the dog, then (s)he hates the owner of the dog.
  • If a dog bites a person at least once then the person chases the dog.
• Conjecture
  • There exists a dog that Jon chases and another person that Jon hates.

In logic

• Type information
  • 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
• Axioms
• Conjecture

In TPTP format

• 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)
        & hates(jon,P) ) ).
  

• Check the syntax in SystemB4TPTP using TPTP4X.
• Check the axioms are consistent with FEST in SystemOnTPTP.
• Try prove it using Vampire in SystemOnTPTP.
• View the derivation using IDV in SystemOnTSTP.
• Verify the derivation using GDV in SystemOnTSTP.

Challenge problem