基于Tableau的定理机器证明系统TableauTAP  

Theorem Proving System Based on Tableau——TableauTAP

作　　者：刘全[1] 孙吉贵[2] 

机构地区：[1]苏州大学计算机科学与技术学院,苏州215006 [2]吉林大学计算机科学与技术学院,长春130012

出　　处：《计算机工程》2006年第7期38-39,45,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60073039;60273080);吉林省科技发展计划基金资助项目(20020306);吉林大学创新基金资助项目

摘　　要：使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP。该系统可以证明不含等词的经典逻辑公式和多值逻辑公式,通过预处理自动生成tableau规则,因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明,实验结果表明,TableauTAP在时间和空间效率上都是比较高的。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.

关 键 词：TABLEAU 定理机器证明 TableauTAP系统 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]