(5)、把全称量词全部移到公式的左边 (6)、把全称量词后面的公式利用等价关系 Av(BAC)分(AVB)∧(AVC)化为子句的合取 式,得到的公式称为 Skolem标准形。 Skolem 标准形的一般形式为Vx1Yx2xnM,其中 M是子句的合取式。 (7)、消去全称量词。 (8)、对变元更名,使子句间无同名变元。（5）、把全称量词全部移到公式的左边。 （6）、把全称量词后面的公式利用等价关系 A(B C)  (AB) (A C)化为子句的合取 式，得到的公式称为Skolem标准形。Skolem 标准形的一般形式为x1 x2 • • •xnM，其中 M是子句的合取式。 （7）、消去全称量词。 （8）、对变元更名，使子句间无同名变元