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

Implement a Semantic Tableau Theorem Prover Using Prolog

作　　者：高华[1] 江建国[1] 苏贺靓 

机构地区：[1]辽宁师范大学数学学院,辽宁大连116029

出　　处：《科技视界》2015年第9期9-11,共3页Science & Technology Vision

摘　　要：语义Tableau是一种具有较强通用性和适用性的推理方法。基于Prolog语言,并利用语义Tableau方法,在M.C.Fitting提出的一阶逻辑自动定理证明器的基础上提出了一些改进,给出了改进后相应的算法,并且对算法的可终止性和正确性进行了证明。实验结果表明,优化后的语义Tableau定理证明器,大大提高推理效率。Semantic Tableau is a strong versatility and applicability of the method of reasoning. Basing on the Prolog language, and the use of Semantic Tableau method, it made some improvements which based on the first-order logic automated theorem proposed by M.C.Fitting, and gave the corresponding algorithm. In addition, it gives the proofs of its terminability and correctness. Experimental results shows that the optimized Semantic Tableau theorem prover makes the Tableau close early and improves greatly in time efficiency of deduction.

关 键 词：语义Tableau 定理证明器 PROLOG 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]