This paper describes an interactive system for proving theorems in the first order predicate calculus. The system utilizes Jeffrey's tree method, a variant of Beth's method of semantic tableaux, which lends it self well to a man-machine interactive type of implementation. The method also permits one to separate clearly the basic problems involved in automatic theorem proving from those of devising suitable heuristics to obtain a proof. The latter can be superimposed on the basic system at a later stage by means of a strategy language. This paper places special emphasis on a detailed description of programs involved. The system is operational on a small computer.