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

An Algorithm for Two Separate Tableau with Equality

作　　者：刘全[1] 孙吉贵[1] 张永刚[1] 

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

出　　处：《计算机工程》2003年第8期44-46,142,共4页Computer Engineering

基　　金：国家自然科学基金资助项目(60073039); 吉林省自然科学基金资助项目(2000540)

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

关 键 词：等词 分阶段tableau 不等式析取 等价类 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]