OR-PARALLEL THEOREM-PROVING WITH RANDOM COMPETITION

With random competition we propose a method for parallelizing arbitrary theorem provers. We can prove high efficiency (compared with other parallel theorem provers) of random competition on highly parallel architectures with thousands of processors. This method is suited for all kinds of distributed memory architectures, particularly for large networks of high performance workstations since no communication between the processors is necessary during run-time. On a set of examples we show the performance of random competition applied to the model elimination theorem prover SETHEO. Besides the speedup results for random competition our theoretical analysis gives fruitful insight in the interrelation between search-tree structure, run-time distribution and parallel performance of OR-parallel search in general.