| 引用本文: | 李舟军,王兵山.语义树方法及其可靠性和完备性.[J].国防科技大学学报,1994,16(3):48-53.[点击复制] |
| Li Zhoujun,Wang Bingshan.The Semantic Tableaux Method and Its Soundness and Completeness[J].Journal of National University of Defense Technology,1994,16(3):48-53[点击复制] |
|
| |
|
|
| 本文已被：浏览 6027次 下载 6397次 |
| 语义树方法及其可靠性和完备性 |
| 李舟军, 王兵山 |
|
(国防科技大学 计算机系 湖南 长沙 410073)
|
| 摘要: |
| Andrews 在《An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof》一书中给出的语义树方法是一种能直接适用于句子集的反驳方法，但其中关于语义树方法的可靠性和完备性定理 (3201)及其证明是错误的。本文通过例子指出并纠正了这一错误，同时对修正后的可靠性和完备性定理给出了详细的证明。 |
| 关键词: 抽象协调类 语义树 可靠性 完备性 |
| DOI： |
| 投稿日期：1993-10-15 |
| 基金项目: |
|
| The Semantic Tableaux Method and Its Soundness and Completeness |
| Li Zhoujun, Wang Bingshan |
|
(Department of Computer Science)
|
| Abstract: |
| The semantic tableaux given in the book‘An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof’by Andrews is a refutation method which can be directly used for sentence sets. Nevertheless,the soundness and completeness theorem (3201) of the semantic tableaux method and the proving process are incorrect. In this paper, we illustrate and correct the mistake. In addition, we prove the revised theorem of the soundness and completeness. |
| Keywords: abstract consistency class,semantic tableaux,soundness,completeness |
|
|
