Distributed resolution-based theorem proving systems
James K. Roberge · 1988
Existing distributed resolution-based theorem proving systems use strategies which are generalizations of the classic uniprocessor theorem proving model. While these distributed strategies yield fruitful results when the number of processors is kept small, they fall prey to a host of difficulties as the number of processors is increased. These difficulties arise as a result of the volume of information which must be routed between processors in order to support these strategies. We propose using a different style of theorem proving as the basis of a distributed theorem proving system. Our approach is based upon the decomposition of a clause set containing both Horn and non-Horn clauses into a set of Horn clause sets. Refutations for the resulting Horn clause sets can be found in parallel and these refutations combined to form a refutation for the original clause set. We show that this approach yields an intuitively appealing style of theorem proving based upon problem decomposition and case reasoning. Equally important, we show that this approach requires the routing of far less information between processors than do existing techniques.