Rich Theories

What is a Rich Theory?

• Many predicate and function symbols
• Many axioms
• Theorems provable from a small subset of axioms
• Examples:
  • Set theory
  • Number theory
  • Geometry
  • Homological algebra

Techniques

• Dieting
• Iterative lemma replacement
• Iterative lemma addition
• Relevance
  • Brute force
  • Intelligence
  • Hierarchies
  • Binary selection

Architecture