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

Algorithm for two separate tableau with equality

在自动推理方面的研究中 ,由于等词的增加 ,导致证明的搜索空间膨胀 ,简单的定理证明变得复杂 ,甚至得不到证明 .在增添新的扩展规则的tableau方法的基础上提出一种新的含等词tableau算法———分阶段tableau .在该算法中 ,将tableau算法分成两个阶段 ,先对等词单独处理 ,然后利用提取不等式析取并在启发式的帮助下计算等价类 ,从而限制了tableau的搜索空间 ,提高了tableau的推理效率 .为了研究分阶段tableau的有效性 ,做了实例分析 ,并与Fitting和Jef frey方法进行了比较 ,结果表明 ,分阶段tableau方法优于其它方法 .

One of the main goals of automated deduction is to efficiently handle logic with equality. Just adding the equality axioms to the database leads to a huge search space; even very simple theorems cannot be proven. In this paper, based on adding new tableau expansion rules, a new tableau algorithm with equality, called 'two separate tableau', is proposed. In this algorithm, we adopted the idea of separating the tableau expansion into two stages. 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 taken to analyze and compare its performance with Fitting's approach and Jeffrey's approach. The results show the two separate tableau is superior to that of other algorithms.