Cooperation between Top-Down and Bottom-Up Theorem Provers
  Top-down and bottom-up theorem proving approaches each have specific
advantages and disadvantages. Bottom-up provers profit from strong redundancy
control but suffer from the lack of goal-orientation, whereas top-down provers
are goal-oriented but often have weak calculi when their proof lengths are
considered. In order to integrate both approaches, we try to achieve
cooperation between a top-down and a bottom-up prover in two different ways:
The first technique aims at supporting a bottom-up with a top-down prover. A
top-down prover generates subgoal clauses, they are then processed by a
bottom-up prover. The second technique deals with the use of bottom-up
generated lemmas in a top-down prover. We apply our concept to the areas of
model elimination and superposition. We discuss the ability of our techniques
to shorten proofs as well as to reorder the search space in an appropriate
manner. Furthermore, in order to identify subgoal clauses and lemmas which are
actually relevant for the proof task, we develop methods for a relevancy-based
filtering. Experiments with the provers SETHEO and SPASS performed in the
problem library TPTP reveal the high potential of our cooperation approaches.
