Suppose a program P is written to accept a set of inputs I. If we are only interested in a nonempty subset $I^ * $ of I, we usually can simplify P to another program $P^ * $ such that $P^ * $ runs faster on $I^ * $ than P does. The problem of specialization is to find such $P^ * $. In this paper, the program P and the input $I^ * $ will be specified by axioms. Using these axioms, we can obtain $P^ * $ from P through theorem-proving techniques.