A Rich Theory is one whose axioms (expressed in 1st order logic) contain a large number of predicates and functors, and whose theorems are often provable from a subset of the axioms. Examples of rich theories are set theory, geometry, and homological algebra. The complexity and scope of rich theories contribute to the difficulty of finding proofs of theorems using Automated Theorem Proving (ATP) systems. This seminar describes techniques that have been developed to improve the performance of ATP systems on theorems in rich theories.