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 proceedingConference 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 languageEnglish
Title of host publicationProceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991
PublisherIEEE Computer Society
Pages275-280
Number of pages6
ISBN (Electronic)0818621524
DOIs
Publication statusPublished - 1991 Jan 1
Externally publishedYes
Event15th Annual International Computer Software and Applications Conference, CMPSAC 1991 - Tokyo, Japan
Duration: 1991 Sep 111991 Sep 13

Publication series

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

Conference

Conference15th Annual International Computer Software and Applications Conference, CMPSAC 1991
CountryJapan
CityTokyo
Period91/9/1191/9/13

    Fingerprint

ASJC Scopus subject areas

  • Software
  • Computer Science Applications

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). [170189] (Proceedings - International Computer Software and Applications Conference). IEEE Computer Society. https://doi.org/10.1109/CMPSAC.1991.170189