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