一种基于超连接的一阶逻辑反演推理算法

An Algorithm of Refutational Theorem Proving for First Order Logic

研究一种一阶谓词逻辑公式的反演求证算法，它是应用超连接过程来处理子句集的消解的，该算法具有比Ｒｏｂｉｎｓｏｎ的传统消解方法更高的效率．以一个实例讨论了该算法的应用，结果表明此算法可以保证在预定义的相关边界内。

An algorithm of refutational theorem proving for first order logic is presented with analyzing its time consuming. It uses hyper linking to process clause set, with much more efficiency than Robinson's resolution method. An application of this method is discussed in a practical example. This algorithm grants the termination of first order logic within a pre defined relevance bound.