Automated Generation of Interesting Theorems

Introduction

• What is ATP?
• Background and Aims
• Alternative Approaches

AGInT

• Architecture
• Runtime Filter
  • Preprocessor
  • Obviousness, Weight, Complexity
  • Surprisingness, Intensity, Adaptively, Focus
• Static Ranker
• Postprocessor

Performance

• Testing Environment
• Aunt Agatha
• The Barbers' Club
• Martians and Venusians
• Truthtellers and Liars
• Naive Set Theory

Conclusion