Title :
Design of a parallel theorem prover for first order logic
Author :
Chen, Wen-Tsuen ; Chou, Tuen-Ru ; Hsieh, Kuen-Rong ; Liu, Huai-Jen
Author_Institution :
Dept. of Comput. Sci., Nat. Tsing Hua Univ., Hsinchu, Taiwan
Abstract :
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
Keywords :
formal logic; logic programming; parallel algorithms; theorem proving; Herbrand universe; divide-and-conquer strategy; first order logic; parallel theorem algorithm; parallel theorem prover; restricted substitution; Computer science; Logic design; Parallel processing; Terminology; Testing;
Conference_Titel :
Computer Software and Applications Conference, 1991. COMPSAC '91., Proceedings of the Fifteenth Annual International
Conference_Location :
Tokyo
Print_ISBN :
0-8186-2152-4
DOI :
10.1109/CMPSAC.1991.170189
