| 语义树方法及其可靠性和完备性 |
| |
| 引用本文： | 李舟军,王兵山.语义树方法及其可靠性和完备性[J].国防科技大学学报,1994,16(3):48-53. |
| |
| 作者姓名： | 李舟军 王兵山 |
| |
| 作者单位： | 国防科技大学计算机系 |
| |
| 摘 要： | Ａｎｄｒｅｗｓ在《ＡｎＩｎｔｒｏｄｕｃｔｉｏｎｔｏＭａｔｈｅｍａｔｉｃａｌＬｏｇｉｃａｎｄＴｙｐｅＴｈｅｏｒｙ：ＴｏＴｒｕｔｈＴｈｒｏｕｇｈＰｒｏｏｆ》一书中给出的语义树方法是一种能直接适用于句子集的反驳方法，但其中关于语义树方法的可靠性和完备性定理（３２０１）及其证明是错误的。本文通过例子指出并纠正了这一错误，同时对修正后的可靠性和完备性定理给出了详细的证明。
|
| 关 键 词： | 抽象协调类 语义树 可靠性 完备性 |
| 收稿时间： | 1993/10/15 0:00:00 |
The Semantic Tableaux Method and Its Soundness and Completeness |
| |
| Li Zhoujun and Wang Bingshan.The Semantic Tableaux Method and Its Soundness and Completeness[J].Journal of National University of Defense Technology,1994,16(3):48-53. |
| |
| Authors: | Li Zhoujun and Wang Bingshan |
| |
| Institution: | 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: | ss:abstract consistency class semantic tableaux soundness completeness |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
| 点击此处可从《国防科技大学学报》下载免费的PDF全文 |
