一种含等词的分阶段tableau算法

An Algorithm for Two Separate Tableau with Equality

在增添新的扩展规则的tableau方法的基础上提出了一种新的含等词tableau算法——分阶段tableau 。在该算法中，将tableau分成两个阶段，等词单独处理，利用提取不等式析取并在启发式的帮助下计算等价类的方法，进一步限制了tableau的搜索空间，提高了tableau的推理效率。同时，为了研究分阶段tableau的有效性，进行了实例分析，并与Fitting和Jeffrey方法进行了比较，结果表明，分阶段tableau方法优于其它方法。

In this paper, b ased on adding new tableau expansion rules, a new tableau algorithm with equality, called ?two separate tableau?, is proposed. In this algorithm, the idea of separating the tableau expansion into two stages is adopted. In the first stage the standard rules are applied until the tableau is exhausted. Thus, in the second stage, it is possible to restrict equality applications and to avoid the generation of useless new formulae. It is possible to restrict search space by using the method based on the transformation into disjunctions of inequalities and the calculation of equivalence classes. At the same time, to study the effectiveness of the algorithm, an example is made to analyze and compare its performance to Fitting?s approach and Jeffrey?s approach. The results show the two separate tableau is superior to that of other algorithms.