Yi's Problem Creator

Interactive Problem Creation

• WWW GUI
• Reuse of TPTP
• Access to ATP systems
• Local user state

Automatic Theorem Discovery

• ATPs generate theorems
• Filters extract interesting ones
  • Non-obvious (proof and possible proof)
  • Surprising (relations between concepts)
  • Intense (axioms compressed to theorem)
  • Novel (non-tautologous, non-redundant WRT axioms and other theorems)
  • Comprehensible (limited number of concepts)
  • Useful (non-specific, antecedent true in models of axioms)
• Architecture
  
• Issues
  • Massive data sets
  • Imprecise understanding of interestingness