TY - GEN

T1 - Design of a parallel theorem prover for first order logic

AU - Chen, Wen Tsuen

AU - Chou, Tzren Ru

AU - Hsieh, Kuen Rong

AU - Liu, Huai Jen

PY - 1991/1/1

Y1 - 1991/1/1

N2 - In this paper, we describe the design of a parallel theorem prover for first order logic. The parallel theorem algorithm is based on the divide-andconquer strategy. The concept of restricted substitution is used to reduce the number of the 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.

AB - In this paper, we describe the design of a parallel theorem prover for first order logic. The parallel theorem algorithm is based on the divide-andconquer strategy. The concept of restricted substitution is used to reduce the number of the 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.

UR - http://www.scopus.com/inward/record.url?scp=85068044724&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85068044724&partnerID=8YFLogxK

U2 - 10.1109/CMPSAC.1991.170189

DO - 10.1109/CMPSAC.1991.170189

M3 - Conference contribution

AN - SCOPUS:85068044724

T3 - Proceedings - International Computer Software and Applications Conference

SP - 275

EP - 280

BT - Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991

PB - IEEE Computer Society

T2 - 15th Annual International Computer Software and Applications Conference, CMPSAC 1991

Y2 - 11 September 1991 through 13 September 1991

ER -