TH1 Type Checking

Overview

• Defined for all TPTP languages using LF
• LF provides type checking rules as a Twelf signature
• Two step process
  • Translation from TPTP to Twelf
  • Run Twelf on signature + translated formulae

Translation to Twelf

• Reject formulae not allowed by language
• Translate all formulae to TH1
  • CNF to FOF - quantify the variables
  • FOF to TF0 - add default types
  • TF0 to TF1, TH0 to TH1 - nada
  • TF0 to TH0, TF1 to TH1 - curry

Type Check with Twelf

• Rules for types
• Rules for terms
• Rules for term constructors
• Rules for proofs
• Rules for polymorphic constants

Questions

• Should be emailed to Florian