Typed Higher-order Logic (THF)

New logic features

• Functions and predicates conflated
• Variable functions and predicates
• Lambda functions with λ (lambda)
• Partial application

Problem

• Axioms
  • Coffee is a beverage.
  • A heated beverage is a beverage.
  • A mixture of a beverage with a syrup is a beverage.
  • A heated mix is the application of heat to the mixture of a beverage with a syrup.
  • A heated mixture is hot!
  • A heated mixture of coffee and any syrup is still coffee.
• Conjecture
  • There is something that when mixed with any syrup results in hot coffee.

In logic

• Type information
  • beverage is a type
  • syrup is a type
  • coffee is a beverage
  • mix takes a beverage and a syrup argument and returns a beverage
  • heat takes a beverage argument and returns a beverage
  • heated_mix takes a beverage and a syrup argument and returns a beverage
  • hot takes a beverage argument and returns boolean
• Axioms
  • heated_mix = λ B:beverage,S:syrup (heat (mix B S))
  • ∀ B:beverage ∀ S:syrup (hot (heated_mix B S))
  • ∀ S:syrup (heated_mix coffee S) = coffee
• Conjecture
  • ∃ M:syrup > beverage ∀ S:syrup (M S) = coffee ∧ (hot (M S))

In TPTP format

• %------------------------------------------------------------------------------
  thf(beverage_decl,type,beverage: $tType).
  thf(syrup_decl,type,syrup: $tType).
  thf(coffee_decl,type,coffee: beverage).
  thf(mix_decl,type,mix: beverage > syrup > beverage).
  thf(heat_decl,type,heat: beverage > beverage ).
  thf(heated_mix_decl,type,heated_mix: beverage > syrup > beverage).
  thf(hot_decl,type,hot: beverage > $o).
  
  thf(heated_mix,axiom,
      heated_mix = ( ^ [B: beverage,S :syrup] : ( heat @ ( mix @ B @ S ))) ).
  
  thf(hot_mixture,axiom,
      ! [B: beverage,S: syrup] : ( hot @ ( heated_mix @ B @ S ) ) ).
  
  thf(heated_coffee_mix,axiom,
      ! [S: syrup] : ( ( heated_mix @ coffee @ S ) = coffee ) ).
  
  thf(hot_coffee,conjecture,
      ? [Mixture: syrup > beverage] :
      ! [S: syrup] :
          ( ( ( Mixture @ S ) = coffee )
          & ( hot @ ( Mixture @ S ) ) ) ).
  %------------------------------------------------------------------------------
  

  Note how the signatures of symbols whose arity is greater than 1 are provided in curried form, which allows for partial application.

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

Challenge problem