自动定理证明一直是人工智能领域中最重要的问题之一。定理证明中通常的想法是通过推出空子句的方法来判定子句集的可满足性。本文在传统的基于归结的方法之上引入了目前流行的扩展规则理论,对其工作原理进行详细阐述,并在此之上提出一种新的知识编译的目标语言——EKCCCL(Each“K”clausesContains Complementary Literal)。知识编译部分的工作以扩展规则为基础,本文提出了一类新的推理问题可以在多项式时间内判定的理论:EKCCCL理论。新的知识编译的方法以EKCCCL理论作为目标语言(target language),简单地说,这种知识编译的过程就是寻找等价的EKCCCL理论的过程,因此是一种新的知识编译方法。本文涉及到的都是对命题逻辑的知识编译,实际上现在对一阶逻辑编译的研究还基本处于空白,主要原因是:不同于命题逻辑的可判定性,一阶逻辑是半可判定的。一阶逻辑的半可判定性导致基于本原蕴含式(prime implicate)的知识编译方法的终止性不能得到保证。