含等词的超表演算

冯莎莎　孙吉贵　吴　瑕

摘要：将处理等词问题的Superposition方法引入超表演算中，使超表演算能处理含等词的一阶逻辑问题，这种新的表演算不但具有完备性，而且无需回溯，是用表演算完成含等词的一阶逻辑定理机器证明的一种尝试。

关键词：超表演算；Superposition方法；等词

中图分类号：TP31

文献标识码：A

文章编号：1671-5489(2005)04—0455—06