一种基于集合符号的自动推理扩展方法  

An Automated Reasoning Expanded Method Based on Set Signs

作　　者：刘全[1] 伏玉琛[1] 孙吉贵[2] 崔志明[1] 龚声蓉[1] 凌兴宏[1] 

机构地区：[1]苏州大学计算机科学与技术学院 [2]吉林大学符号计算与知识工程教育部重点实验室,长春130012

出　　处：《计算机研究与发展》2007年第8期1317-1323,共7页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60473003;60673092);教育部科学技术研究重点基金项目(207040);中国博士后科研基金项目(20060390919);江苏省高校自然科学基金项目(06KJB520104);江苏省博士后科研基金项目(060211C)

摘　　要：在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.On the basis of the many-valued logics tableau reasoning, an automated reasoning expansion method based on set sign is presented. This approach which treats set signs as truth values can be applied to some methods and techniques of reasoning suited to classical logics, which make reasoning reform from the non-classical logics to the classical logics. Through rewriting set signs and expansion rules, it is very easy to spread to modal logics, intuitionistic logics and so on. The technology can also be further spread to infinitevalued logic and logic with fuzzy quantifiers（such as T-calculus and S-calculus and so on） . The theorem proving system-TSetTAP is implemented by using SWI-PROLOG language in microcomputer. Using method of set signs in the system, rule programming can be generated by only increasing reasoning rules in rule base. System need not be repaired. So some strategies and approaches used in classical logics can easily apply to non-clssical logic. 900 logic questions in TPTP are proved using the system. The result shows TSetTAP makes the tableau close early and improve greatly in time efficiency and space efficiency of reasoning.

关 键 词：集合符号 自动推理 TABLEAU 经典逻辑 非经典逻辑 

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