Parallelization of deduction strategies: an analytical study

In this paper we present a general analysis of the parallelization of deduction strategies. We classify strategies as subgoal-reduction strategies, expansion-oriented strategies and contraction-based strategies. For each class we analyze how and what types of parallelism can be utilized. Since the operational semantics of deduction-based programming languages can be construed as subgoal-reduction strategies, our analysis encompasses, at the abstract level, both strategies for deduction-based programming and those for theorem proving. We distinguish different types of parallel deduction based on the granularity of parallelism. These two criteria -- the classification of strategies and of types of parallelism -- provide us with a framework to treat problems and with a grid to classify approaches to parallel deduction. Within this framework, we analyze many issues, including the dynamicity and size of the data base of clauses during the derivation, the possibility of conflicts between parallel inferences, and duplication versus sharing of clauses. We also suggest the type of architectures that may be suitable for each class of strategies. We substantiate our analysis by describing existing methods, emphasizing parallel expansion-oriented strategies and parallel contraction-based strategies for theorem proving. The most interesting and least explored by existing approaches are the contraction-based strategies. The presence of contraction rules -- rules that delete clauses -- and especially the application of backward contraction, emerges as a key issue for parallelization of these strategies. Backward contraction is the main reason for the impressive experimental success of contraction-based strategies. Our analysis shows that backward contraction makes efficient parallelization much more difficult. In our analysis, coarse-grain parallelism appears to be the best choice for parallelizing contraction-based reasoning. Accordingly, we propose a notion of parallelism at the search level as coarse grain parallelism for deduction.