Design of a parallel theorem prover for first order logic

Wen Tsuen Chen; Tzren Ru Chou; Kuen Rong Hsieh; Huai Jen Liu

doi:10.1109/CMPSAC.1991.170189

Design of a parallel theorem prover for first order logic

Wen Tsuen Chen, Tzren Ru Chou, Kuen Rong Hsieh, Huai Jen Liu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991
Publisher	IEEE Computer Society
Pages	275-280
Number of pages	6
ISBN (Electronic)	0818621524
DOIs	https://doi.org/10.1109/CMPSAC.1991.170189
Publication status	Published - 1991
Externally published	Yes
Event	15th Annual International Computer Software and Applications Conference, CMPSAC 1991 - Tokyo, Japan Duration: 1991 Sept 11 → 1991 Sept 13

Publication series

Name	Proceedings - International Computer Software and Applications Conference
ISSN (Print)	0730-3157

Conference

Conference	15th Annual International Computer Software and Applications Conference, CMPSAC 1991
Country/Territory	Japan
City	Tokyo
Period	1991/09/11 → 1991/09/13

ASJC Scopus subject areas

Software
Computer Science Applications

Access to Document

10.1109/CMPSAC.1991.170189

Cite this

Chen, W. T., Chou, T. R., Hsieh, K. R., & Liu, H. J. (1991). Design of a parallel theorem prover for first order logic. In Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991 (pp. 275-280). Article 170189 (Proceedings - International Computer Software and Applications Conference). IEEE Computer Society. https://doi.org/10.1109/CMPSAC.1991.170189

Design of a parallel theorem prover for first order logic. / Chen, Wen Tsuen; Chou, Tzren Ru; Hsieh, Kuen Rong et al.
Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991. IEEE Computer Society, 1991. p. 275-280 170189 (Proceedings - International Computer Software and Applications Conference).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Chen, WT, Chou, TR, Hsieh, KR & Liu, HJ 1991, Design of a parallel theorem prover for first order logic. in Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991., 170189, Proceedings - International Computer Software and Applications Conference, IEEE Computer Society, pp. 275-280, 15th Annual International Computer Software and Applications Conference, CMPSAC 1991, Tokyo, Japan, 1991/09/11. https://doi.org/10.1109/CMPSAC.1991.170189

@inproceedings{df75677528414b05a85025553d592b63,

title = "Design of a parallel theorem prover for first order logic",

abstract = "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.",

author = "Chen, {Wen Tsuen} and Chou, {Tzren Ru} and Hsieh, {Kuen Rong} and Liu, {Huai Jen}",

note = "Publisher Copyright: {\textcopyright} 1991 IEEE.; 15th Annual International Computer Software and Applications Conference, CMPSAC 1991 ; Conference date: 11-09-1991 Through 13-09-1991",

year = "1991",

doi = "10.1109/CMPSAC.1991.170189",

language = "English",

series = "Proceedings - International Computer Software and Applications Conference",

publisher = "IEEE Computer Society",

pages = "275--280",

booktitle = "Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991",

}

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

Y1 - 1991

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 -

Design of a parallel theorem prover for first order logic

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this