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

Theorem Proving System Based on Tableau——TableauTAP

使用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.