Cooperation between Top-Down and Bottom-Up Theorem Provers by Subgoal Clause Transfer Dirk Fuchs Fachbereich Informatik, Universitaet Kaiserslautern Postfach 3049, 67653 Kaiserslautern Germany E-mail: dfuchs@informatik.uni-kl.de Abstract Top-down and bottom-up theorem proving approaches have each specific advantages and disadvantages. Bottom-up provers profit from strong redundancy control and suffer from the lack of goal-orientation, whereas top-down provers are goal-oriented but have weak calculi when their proof lengths are considered. In order to integrate both approaches our method is to achieve cooperation between a top-down and a bottom-up prover: The top-down prover generates subgoal clauses, then they are processed by a bottom-up prover. We discuss theoretic aspects of this methodology and we introduce techniques for a relevancy-based filtering of generated subgoal clauses. Experiments with a model elimination and a superposition-based prover reveal the high potential of our cooperation approach. Keywords theorem proving, cooperation, top-down/bottom-up integration