A model and a first analysis of distributed-search contraction-based strategies

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 machine-independent analysis of theorem-proving strategies. This paper considers clausal contraction-based strategies and their parallelization by distributed search, with subdivision of the search space and propagation of clauses by message-passing (e.g., à la Clause-Diffusion). A model for the representation of the parallel searches produced by such strategies is presented, and the bounded-search-spaces 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 contraction-based strategy with that of its parallelization in the above sense.