一种求解tableau等式合一问题的算法

摘要：

在增添扩展规则的tableau方法的基础上提出了一种新的含等词tableau方法--等式合一方法,并证明了它的可靠性和完备性.在该方法中,将tableau分成两个阶段,等词单独处理,通过提取等式合一问题并求解解替换封闭tableau,进一步限制了tableau的搜索空间,提高了tableau的推理效率.同时,为了研究等式合一方法的有效性,在解替换求解方面,提出了提取不等式析取,并在启发式的帮助下计算等价类的方法.通过实例分析,结果表明,等式合一方法优于其它方法.

关键词：等式合一、不等式析取、等价类

所属期刊栏目：33

分类号：TP3(计算技术、计算机技术)

资助基金：中国科学院资助项目60073039;60273080;60473033

在线出版日期：2006-03-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：216-219