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