语义Tableau是一种具有较强直观性和适用性的推理方法.自该方法问世以来,一直吸引着大量人工智能研究者.基于Prolog语言,M.C.Fitting利用语义Tableau方法提出了一种一阶逻辑自动定理证明器.众所周知,系统的实现效率问题一直是人工智能界的一个热点问题.M.C.Fitting给出的定理证明器虽然比较容易理解,但是在具体应用过程中却存在着一定的效率问题,论文便是针对这一问题展开了具体的研究.具体的研究内容如下:1论文首先给出了一阶逻辑语言的项、公式、子句等有关的概念,然后在此基础上研究了一阶逻辑语言理论及其模型系统,并重点探讨了Herbrand模型.2论文介绍语义Tableau方法的理论和实现.首先描述了Tableau方法的概念与其在实际应用过程中的语义Tableau扩展规则,并完成了该方法的可靠性和完备性的证明,重点介绍了在证明完备性过程中所要用到的模型存在定理;其次给出了实现该系统的算法与在Prolog语言下的代码.3通过对M.C.Fitting给出的定理证明器中存在的效率问题进行分析研究,提出了相关的改进,并给出了改进后的算法以及该算法可终止性和正确性的证明.最后进行了相应的对比实验,结果表明:优化后的语义Tableau定理证明器的推理效率得到了显著的提高.