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.
Keywords: first order logic, automatic theorem proving, divide and conquer, parallel algorithm, pipelining
Received May 16, 1990; revised July 20. 1991.
Communicated by Lin-Shan Lee.
*A preliminary version of this paper has been presented in the 15-th Annual International Computer Software and Applications Conference (IEEE COMSAC'91), Kogakuin University, Tokyo, Japan, September 11-13, 1991.