COMPSAC 91 - THE FIFTEENTH ANNUAL INTERNATIONAL COMPUTER SOFTWARE & APPLICATIONS CONFERENCE, PROCEEDINGS, Institute of Electrical and Electronics Engineers, Tokyo, Japan, 11-13 Sep. 1991, Pages 275-280
The design of a parallel theorem prover for first-order logic is described. The parallel theorem algorithm is based on the divide-and-conquer strategy. The concept of restricted substitution is used to reduce the number of ground clauses generated during the operation of this theorem prover. In this manner, the ground clause set generated by the theorem prover will be much smaller than that generated directly by Herbrand universe.