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

An Algorithm to Solve Tableau with Equality Unification Question

在增添扩展规则的 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.