Analysis of Distributed-Search Contraction-Based Strategies
Maria Paola Bonacina4 
| (4) |
Dept. of Computer Science, University of Iowa, Iowa City, IA 52242-1419, USA |
Abstract
We present a model of parallel search in theorem proving for forward-reasoning strategies, with contraction and distributed
search. We extend to parallel search the bounded-search-spaces approach to the measurement of infinite search spaces, capturing
both the advantages of parallelization, e.g., the subdivision of work, and its disadvantages, e.g., the cost of communication,
in terms of search space. These tools are applied to compare the search space of a distributed-search contraction-based strategy
with that of the corresponding sequential strategy.
Supported in part by NSF grants CCR-94-08667 and CCR-97-01508.
References secured to subscribers.