While various approaches to parallel theorem proving have been proposed, their usefulness is evaluated only empirically. This research is a contribution towards the goal of machinedindependent analysis of theoremdproving strategies. This paper considers clausal contractiondbased strategies and their parallelization by distributed search, with subdivision of the search space and propagation of clauses by messagedpassing (e.g., a la ClausedDiffusion). A model for the representation of the parallel searches produced by such strategies is presented, and the boundeddsearchdspaces approach to the measurement of search complexity in infinite search spaces is extended to distributed search. This involves capturing both its advantages, e.g., the subdivision of work, and disadvantages, e.g., the cost of communication, in terms of search space. These tools are applied to compare the evolution of the search space of a contractiondbased strategy with that of its parallelization in the above sense.
['Maria Paola Bonacina']
A model and a first analysis of distributed-search contraction-based strategies