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

摘要

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