期刊名称：International Journal of Computer Science and Network Security
印刷版ISSN：1738-7906
出版年度：2006
卷号：6
期号：1A
页码：190-195
出版社：International Journal of Computer Science and Network Security
摘要：Method based on extension rule is a new method for theorem proving. It is, in a sense, potentially a complementary method to resolution based method. ER is the basic extension rule algorithm. In order to increase its efficiency, this paper improves it by some reduction rules. And then the soundness and completeness of the improved algorithm is proved. The experiment results show the improved algorithm not only increase the efficiency but also keep the characteristic of the extension rule method, namely it is still potentially complementary methods to resolution based methods. In order to enhance the reasoning speed by making the best of the respective characteristic of extension rule method and resolution method, this paper proposes a combined algorithm with reduction rules, which combines the extension rule and resolution. It is also sound and complete.
