摘要: 本文为广义归结原理提供了一种方法,该方法能将要证明的定理写成一阶逻辑中较为自然的Skolem标准形式。