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

关键词: Tableau；定理机器证明；TableauTAP 系统

Abstract: 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

Key words: Tableau; Theory machine proving; TableauTAP system