Design of a parallel theorem prover for first order logic

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

研究成果: 書貢獻/報告類型會議貢獻

摘要

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.

原文英語
主出版物標題Proceedings of the15th Annual International Computer Software and Applications Conference, CMPSAC 1991
發行者IEEE Computer Society
頁面275-280
頁數6
ISBN(電子)0818621524
DOIs
出版狀態已發佈 - 1991 一月 1
對外發佈Yes
事件15th Annual International Computer Software and Applications Conference, CMPSAC 1991 - Tokyo, 日本
持續時間: 1991 九月 111991 九月 13

出版系列

名字Proceedings - International Computer Software and Applications Conference
ISSN(列印)0730-3157

會議

會議15th Annual International Computer Software and Applications Conference, CMPSAC 1991
國家日本
城市Tokyo
期間1991/09/111991/09/13

ASJC Scopus subject areas

  • Software
  • Computer Science Applications

指紋 深入研究「Design of a parallel theorem prover for first order logic」主題。共同形成了獨特的指紋。

引用此