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

An Algorithm to Solve Tableau with Equality Unification Question

作　　者：刘全[1] 孙吉贵[2] 窦全胜[2] 

机构地区：[1]苏州大学计算机科学与技术学院,苏州215006 [2]吉林大学计算机科学与技术学院,长春130012

出　　处：《计算机科学》2006年第1期216-219,共4页Computer Science

基　　金：本课题得到国家自然科学基金(60073039;60273080;60473003)资助。

摘　　要：在增添扩展规则的 tableau 方法的基础上提出了一种新的含等词 tableau 方法——等式合一方法,并证明了它的可靠性和完备性。在该方法中,将 tableau 分成两个阶段,等词单独处理,通过提取等式合一问题并求解解替换封闭 tableau,进一步限制了 tableau 的搜索空间,提高了 tableau 的推理效率。同时,为了研究等式合一方法的有效性,在解替换求解方面,提出了提取不等式析取,并在启发式的帮助下计算等价类的方法。通过实例分析,结果表明,等式合一方法优于其它方法。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 restricts the tableau search space and raises the inference efficiency by extracting the e quality unification problems and solving the substitution to close tableau. At the same time, to verify the validity of the algorithm, we give a method based on the transformation into disjunctions of inequalities and the calculation of equivalence classes with the help of heuristics. Though the instance analysis and implememation of the EU-Tableau system, it shows that equality unification is superior to other methods.

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

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程] TP312[自动化与计算机技术—控制科学与工程]