语义Tableau定理证明器的Prolog实现     

高华  江建国  苏贺靓 《环球赛鸽科技》2015,(9)

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

质点几何定理证明的机器实现     

苏贺靓  江建国  高华 《环球赛鸽科技》2015,(15)

本文针对质点法生成的目标关系式的过程不简明,缺少明显几何意义的问题,提出了一种具有较高可读性算法的几何定理证明器MMP.首先,直接从消点公式推导目标关系式,该方法不再使用质点坐标而直接对质点进行运算;其次,利用三个模块架构证明器,彤成了具有完全性的消点过程;最后,利用待定系数法判定结论语句.由于可以对点直接进行运算,该证明器的消点过程比原有质点法具有明显的几何意义和较高运算效率.  相似文献