THF Problems

Problem Sources

• Chris Benzmüller's collections
• Chad Brown's Landau collection
• Deepak Garg's security work
• Chad Brown's encoding of Ramsey number problems
• Export from DeTSeT
• Export from TPS library
• Juttings' AUTOMATH encoding of Landau
• Ted Sider's modal logic problems
• Translation of ILTP problems

Problem Domains

• Logical cacluli (107 problems)
• Set theory (1407 problems)
• Graph theory (93 problems)
• General algebra (80 problems)
• Group theory (1 problem)
• Number theory (212 problems)
• Computing theory (1 problem)
• Software verification (37 problems)
• Puzzles (51 problems)
• Syntactic (738 problems)
• Miscellaneous (2 problems)

Release Schedule

• TPTP v3.6.0 - THF0 alpha - Christmas 2008 (281 problems)
• TPTP v3.7.0 - THF0 beta - March 2009 (1275 problems)
• TPTP v4.0.0 - THF0 public - August 2009 (2729 problems)
• CASC THF division at CADE-22 - August 2009

Browsing available online at www.tptp.org