Automated Theorem Proving
for
Hard Theorems in Rich Theories

Introduction

• What is ATP?, What is it Good For?
• What are "Rich Theories"?
• Overview of the Projects

Selecting Axioms

• Brute Force and Ignorance (RedAx)
• Measuring Relevance (Prophet)
  • Background
  • Direct Relevance
  • Transitive Relevance
• Using Relevance (YuCS)

Adding Lemmas

• Using Lemmas (YiLT and YuLM)
• Generating Interesting Lemmas and Theorems (AGInT)

Combining ATP Systems

• Proving (more) Easy Theorems (SSCPA)
• Proving Hard Theorems (CSSCPA)

Derivation Verification and Presentation

• Semantic Verification (DVDV)
• Presentation (YuTV)