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

• 作者: 江建国 苏贺靓 高华
• 来源期刊: 科技视界
• 关键词: 语义Tableau 定理证明器 Prolog
• 年，卷（期）: 2015,（9）
• 所属期刊栏目: 本刊视点
• 页码范围: 9-11
• 页数: 3页
• 字数: 3794字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	高华	辽宁师范大学数学学院	3	2	1.0	1.0
2	江建国	辽宁师范大学数学学院	17	88	4.0	9.0
3	苏贺靓	辽宁师范大学数学学院	2	0	0.0	0.0