论文部分内容阅读
语义Tableau是一种具有较强通用性和适用性的推理方法。基于Prolog语言,并利用语义Tableau方法,在M.C.Fitting提出的一阶逻辑自动定理证明器的基础上提出了一些改进,给出了改进后相应的算法,并且对算法的可终止性和正确性进行了证明。实验结果表明,优化后的语义Tableau定理证明器,大大提高推理效率。