一种含等词的分阶段tableau算法

• 作者: 刘全 南冬辉 李龙
• 来源期刊: 大庆石油学院学报
• 学科: 工学
• 关键词: 等词 分阶段tableau 不等式析取 等价类
• 年，卷（期）: 2003,（1）
• 所属期刊栏目: 计算机科学
• 页码范围: 46-50
• 页数: 5页
• 分类号: TP181
• 字数: 3603字
• 语种: 中文
• DOI: 10.3969/j.issn.2095-4107.2003.01.015

摘要

在自动推理方面的研究中,由于等词的增加,导致证明的搜索空间膨胀,简单的定理证明变得复杂,甚至得不到证明. 在增添新的扩展规则的tableau方法的基础上提出一种新的含等词tableau算法--分阶段tableau.在该算法中,将tableau算法分成两个阶段,先对等词单独处理,然后利用提取不等式析取并在启发式的帮助下计算等价类,从而限制了tableau的搜索空间,提高了tableau的推理效率. 为了研究分阶段tableau的有效性,做了实例分析,并与Fitting和Jeffrey方法进行了比较,结果表明,分阶段tableau方法优于其它方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李龙	大庆石油学院计算机科学与工程学院	9	32	3.0	5.0
2	刘全	大庆油田有限责任公司采油工程研究院	4	2	1.0	1.0
3	南冬辉	大庆油田有限责任公司信息中心	1	0	0.0	0.0