Strategy Parallelism and Lemma Evaluation

Automated Deduction offers no unique strategy which is uniformly successful on all problems. Hence a parallel combination of several different strategies increases the chances of success. The efficiency of this approach can be increased even more by the exchange of suitable intermediate results. The paper offers a cooperative solution approach to this task. As a special kind of cooperation we present here the selection of suitable lemmata together with a model of a cooperative parallel theorem prover which combines different lemma selection techniques within a strategy parallel prover environment. We give a short assessment of the results of first experiments and an outline of the future work.