Exploitation of parallel processing for implementing high-performance deduction systems

We describe a scheme for parallelizing first-order logic deduction systems. This scheme has been successfully used for parallelizing OTTER, which is a sequential deduction system developed at Argonne National Laboratory. This parallel deduction system, called PARRallel OTter-II (PARROT-II) has attained real speedups in excess of 20 over the best results of current sequential deduction systems. We believe that our results are of interest for two distinct reasons: (1) this is (as far as we know) the first case in which a system has successfully exploited parallelism to outperform the best sequential deduction systems on difficult problems, and (2) we believe that our approach generalizes to other deduction paradigms (e.g., term rewriting systems).This paper discusses the motivation for developing the scheme used by PARROT-II and the implementation details of PARROT-II. It also presents timing results for PARROT-II for some benchmark problems.Work submitted as partial fulfillment of the requirements for the doctoral degree at the Graduate College of the University of Illinois at Chicago. This work was supported in part by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.