Dependent Types

TPTP Language for Dependent Types

• Cezary will write this part

Problems

• The problems provided by Daniel and Cezary have been separated into three groups:
  • Test problems designed to test particular aspects of reasoning with dependent types
  • Application problems, divided into:
    • Monomorphic problems
    • Polymorphic problems
  The monomorphic and polymorphic problems have each been split into:
  • Complete problems
  • Lemmas that can be used to help solving complete problems
• Browse the problems.
• Download a .tgz of all the problems.
• Results from DLash and DT2H2X as a .csv

ATP Systems and Tools

• DLash 1.11
  • As an ATP system
  • As a DTF type checker
  • Available in SystemOnTPTP
• DT2H2X 1.8.4
  • As an ATP system
  • As a DTF type checker
  • Available in SystemOnTPTP
• TPTP Utils (by Alex Steen)
  • As a translator to plain THF (still to have Daniel's modifications merged)