Design of a Parallel Theorem Prover for First Order Logic
Wen-Tsuen Chen, Tzren-Ru Chou, Kuen-Rong Hsieh and Huai-Jen Liu Department of Computer Science National Tsing Hua University Hsinchu, Taiwan 30043, R.O.C.
In this paper, we describe the design of a parallel theorem prover for first order logic. The parallel theorem proving algorithm is based on a divide-and-conquer strategy. The concept of restricted substitution is used to reduce the number of the ground clauses generated during the operation of this theorem prover will be much smaller than that generated directly by the Herbrand universe. Both the ground clause generation procedure and the theorem proving algorithm are parallel; furthermore, they have a full degree of parallelism. The speed up is almost proportional to the number of processors.