Proving Hard Theorems in Rich Theories

Introduction

• What is ATP?
• What are "Rich Theories"?
• Approaches to Proving Hard Theorems

Brute Force and Ignorance

• A Motivating Example
• Axiom Reduction
• Implementation and Results
• Conclusion

Subtlety and Intelligence

• Relevancy Measures
• Binary Search