What are "Rich Theories"?

Rich Theories

• Large number of axioms
• Large number of predicates and functors
• Theorems provable from subsets of axioms
• Rich and lean examples
  • NBG Set Theory (Local copy)
  • Wajsberg algebra (Local copy)
• Other rich theories: Set theory, Number theory, Ontologies, Geometry, Homological algebra, Semantic WWW, the Real World

Causes of Richness

• Linked sub-theories
• Hierarchical theories (definitions)
• Existential quantification (when converted to CNF)

The Challenge to ATP

• Large numbers of axioms increase the search space
• Unnecessary axioms (for a given theorem) create search space without solutions

• Richness provides information