THF Tools

Parsing and Type Checking

• BNF translation to lex/yacc/flex/bison input
• Syntax tree analysis, clickable interface in SystemB4TPTP by Frank Theiss
• TPTP2X and TPTP4X
  • Parse and pretty print
  • Export to Twelf, OmDoc, TPS, Isabelle, and S-expressions
• Type checking by export to Twelf, magic by Florian Rabe
  (also available in SystemB4TPTP)

Automated Reasoning

• LEO II - Chris Benzmüller's magic
• TPS-GOOD1 - Chad Brown's sorcery
• IsabelleP - wizardry by Makarius Wenzel and Stefan Berghofer
• IsabelleM - added mojo by Jasmin Blanchette
• IsabelleM - new trickery by Jasmin Blanchette
• Running in the SystemOnTPTP utility and online

Solution Presentation

• Derivation viewing in IDV

Documentation

• Quick guide
• Technical manual