DocumentCode
2614339
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
fYear
1991
fDate
11-13 Sep 1991
Firstpage
275
Lastpage
280
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/CMPSAC.1991.170189
Filename
170189
Link To Document