The Logic and the Implementation A brief description of our theorem-proving system may be found in [6]. The theorem prover and its logic, as of 1979, are described completely in I1]. A slight revision of the logic is presehted in [2], where ales a~ metafunction" facility is described which permits the user to define new proof procedures in the logic, prove them correct mechanically, and have them used efficiently in subsequent proof attempts. During the period 1980-1985 a linear arithmetic decision procedure was integrated into the rule-driven simplifier. The problems of integrating a decision procedure into a heuristic theorem prover for a richer theory are discussed in [8].