THF Introduction

What is it?

• Many different frameworks, unlike first-order logic
• History ... Frege, Russell, Church, Martin Löf, Girard, Reynolds
• Church's simple type theory is a common basis

What is it Good For?

• Hardware and software verification, e.g., Verisoft
• Knowledge based reasoning, e.g., SUMO, Cyc
• Computer supported mathematics, e.g., Mizar, DeTSeT
• Multimodal and authorization logics

What Systems are Successful?

• Interactive higher-order proof assistants
  • Isabelle, HOL, Coq, ProofPower, Omega, ...
• Automated higher-order theorem provers
  • LEO II, TPS, IsabelleP and IsabelleM, ... erm ...

TPTP Infrastructure

• Not as advanced as that of first-order
• Islands of activity with large syntax gaps
• The THFTPTP project (thanks to the EU)