A novel asynchronous parallelism scheme for first-order logic

Abstract

We present a new parallelization technique designed to speed the solution of first-order inference problems by detecting and pruning unnecessary search. Our technique, called nagging, is naturally fault tolerant and relatively robust in the presence of high communication latency. As a result, it is well suited to execution on a network of loosely-coupled processors. Our implementation has been tested on as many as 100 workstations and exhibits encouraging scaling properties. In this paper, we introduce nagging in the context of existing work on parallel search for logical inference, present an informal analysis of its operation, and present some empirical results for our PTTP-style prototype.