| 基于Tableau的定理机器证明系统TableauTAP |
| |
| 引用本文： | 刘全,孙吉贵.基于Tableau的定理机器证明系统TableauTAP[J].计算机工程,2006,32(7):38-39,45. |
| |
| 作者姓名： | 刘全 孙吉贵 |
| |
| 作者单位： | 1. 苏州大学计算机科学与技术学院,苏州,215006;吉林大学计算机科学与技术学院,长春,130012
2. 吉林大学计算机科学与技术学院,长春,130012 |
| |
| 基金项目： | 中国科学院资助项目;吉林省科技发展计划;吉林大学校科研和教改项目 |
| |
| 摘 要： | 使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TabIeauTAP。该系统可以证明不含等词的经典逻辑公式童耋譬逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明，实验结果表明，TableauTAP在时间和空间效率上都是比较高的。
|
| 关 键 词： | 定理机器证明 TableauTAP系统 |
| 文章编号： | 1000-3428（2006）07-0038-02 |
| 收稿时间： | 2005-05-17 |
| 修稿时间： | 2005-05-17 |
Theorem Proving System Based on Tableau--TableauTAP |
| |
| LIU Quan,SUN Jigui.Theorem Proving System Based on Tableau--TableauTAP[J].Computer Engineering,2006,32(7):38-39,45. |
| |
| Authors: | LIU Quan SUN Jigui |
| |
| Affiliation: | 1. Institute of Computer Science and Technology, Soochow University, Soochow 215006; 2. Institute of Computer Science and Technology, Jilin University, Changchun 130012 |
| |
| Abstract: | Theorem proving system is implemented by using SWI-PROLOG language in microcomputer and proved its sound. This system can prove classical logics and many-valued logics formulae without equality. It is very easy to extend its function due to tableau rules are produced automatically by preprocessing. 400 logic questions in TPTP are proved using the system that. The result shows that TableauTAP makes the tableau close early and improves greatly in time efficiency and space efficiency of deduction. |
| |
| Keywords: | Tableau |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
