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

计算机科学 ›› 2006, Vol. 33 ›› Issue (1): 216-219.

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

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
本课题得到国家自然科学基金（60073039,60273080,60473003）资助.

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

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

关键词: 等式合一不等式析取等价类 tableau方法求解算法扩展规则搜索空间完备性可靠性

Abstract: A new method of tableau with equality based on the additional tableau expansion is proposed and its sound and complete is proved. We adopt the idea of separating the tableau expansion into two stages in the method. The equality handle is independent. It r

Key words: Equality unification, Disiunctions of inequality, Equivalence classes

. 一种求解tableau等式合一问题的算法[J]. 计算机科学, 2006, 33(1): 216-219. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed