A theoretical framework and algorithms are presented that provide a basis for the study of induction of definite (Horn) clauses. These hinge on a natural extension of θ-subsumption that forms a strong model of generalization. The model allows properties of inductive search spaces to be considered in detail. A useful by-product of the model is a simple but powerful model of redundancy. Both induction and redundancy control are central tasks in a learning system, and, more broadly, in a knowledge acquisition system. The results also demonstrate interaction between induction, redundancy, and change in a system's current knowledge-with subsumption playing a key role.