李龙,刘全,南冬辉

• 1:大庆石油学院计算机科学与工程学院

• 2:大庆油田有限责任公司采油工程研究院

• 3:大庆油田有限责任公司信息中心 黑龙江大庆163318

• 4:黑龙江大庆163453

摘要(Abstract)：

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

关键词(KeyWords)：等词;分阶段tableau;不等式析取;等价类

Abstract:

Keywords:

基金项目(Foundation):

作者(Author):李龙,刘全,南冬辉

Email:

参考文献(References)：

• [1] 刘叙华,安 直.使用等式替换策略的广义归结[J].科学通报,1985,3(21):1601～1603.

• [2] 孙吉贵,刘叙华.NC线性对称调解[J].计算机学报,1985,12(7):18～20.

• [3] FittingM .FirstOrderLogicandAutomatedTheoremProving[M].NewYork:SpringerVerlag,1996.30～33.

• [4] FittingM .TypesandTableau[M].NewYork:SpringerVerlag,2000.101～104.