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.
Published Date: May 1999
Registration: ISBN 978-1-57735-080-4
Copyright: Published by The AAAI Press, Menlo Park, California.