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

An Automated Reasoning Expanded Method Based on Set Signs

在多值逻辑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.