摘要
语义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.
出处
《科技视界》
2015年第9期9-11,共3页
Science & Technology Vision
