Automatic Generation of Interesting Theorems

Introduction

• What is ATP?
• Applications and Systems
• Theorems and Logical Consequences
• Generating Theorems

AGInT

• Architecture
• PreProcessor
• RunTime Filter
• Static Ranker
• PostProcessor

Results

• Puzzling Lemmas
• Puzzling Theorems
• Homological Algebra Theorems
• Set Theory Theorems

Conclusion

• Will the Results be Useful?
• Can We Meet the Challenge?