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