该文主要探讨基于逻辑的自动推理方法,提出了扩展规则,在此基础上建立了一种基于扩展规则的定理证明方法和一种基于扩展规则的知识编译方法.基于归结的定理证明方法一直是定理证明应用最广的方法之一.该文提出了一种新的定理证明方法,它的主要思想是沿着归结的逆向作定理证明并且用包含排斥原理解决这样做带来的空间复杂性问题.我们证明了这种方法的正确性和完备性,同时还引入了"互补因子"的概念来估计它的复杂性.这种方法有时从效率上要优于基于归结的方法,因此可以看作是和归结互补的一种定理证明方法.在此基础上,我们又提出了一种新的知识编译方法.它以EPCCL理论作为编译的目标语言.这种新方法与已有的知识编译方法的不同之处在于:无论是在线推理过程还是离线推理过程都是基于扩展规则的.对于用我们的方法编译后的理论的任何询问都能在线性时间内给出回答.而且对于某些问题用我们的方法编译效率很高,编译后的子句集规模较小.此外,该文还作了一些诊断方面的研究,引入了借助其它系统进行辅助诊断的思想,在此基础上提出了一种针对模型不完备条件下的诊断方法,使得经典的诊断方法对于模型的依赖程度有所降低.