在谓词逻辑中，有下述定义：
原子（atom）谓词公式是一个不能再分解的命题。
原子谓词公式及其否定，统称为文字（literal）。
P
P
P称为正文字，
¬
P
\neg P
¬P称为负文字。
P
P
P与
¬
P
\neg P
¬P为互补文字。
任何文字的析取式称为子句（clause）。任何文字本身也是子句。
由子句构成的集合称为子句集。
不包含任何文字的子句称为空子句，表示为NIL。
由于空子句不含有文字，它不能被任何解释满足，所以，空子句是永假的、不可满足的。
在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集，从而能够比较容易地判定谓词公式的不可满足性。下面结合一个具体的例子，说明把谓词公式化为子句集的步骤。
[例] 将下列谓词公式化为子句集：
(
∀
x
)
{
(
∀
y
)
P
(
x
,
y
)
→
¬
(
∀
y
)
[
Q
(
x
,
y
)
→
R
(
x
,
y
)
]
}
\mathbf{(\forall x)\{(\forall y)P(x,y) \rightarrow \neg(\forall y)[Q(x,y) \rightarrow R(x,y)]\}}
(∀x){(∀y)P(x,y)→¬(∀y)[Q(x,y)→R(x,y)]}
(1) 消去谓词公式中的
“
→
”
“\rightarrow”
“→”和
“
↔
”
“\leftrightarrow”
“↔”
利用谓词公式的等价关系：
P
→
Q
⟺
¬
P
∨
Q
P
⟷
Q
⟺
(
P
∨
Q
)
∨
(
¬
P
∨
¬
Q
)
\mathbf{P \rightarrow Q \Longleftrightarrow \neg P \lor Q} \\ \mathbf{P\longleftrightarrow Q \Longleftrightarrow(P \lor Q) \lor (\neg P \lor \neg Q)}
P→Q⟺¬P∨QP⟷Q⟺(P∨Q)∨(¬P∨¬Q)
上列等式等价变化为：
(
∀
x
)
{
¬
(
∀
y
)
P
(
x
,
y
)
∨
¬
(
∀
y
)
[
¬
Q
(
x
,
y
)
∨
R
(
x
,
y
)
]
}
\mathbf{(\forall x)\{\neg (\forall y)P(x,y)\lor \neg(\forall y)[\neg Q(x,y)\lor R(x,y)]\}}
(∀x){¬(∀y)P(x,y)∨¬(∀y)[¬Q(x,y)∨R(x,y)]}
(2)把否定符号移到紧靠谓词的位置上
利用谓词公式的等价关系：
双重否定律：
¬
(
¬
P
)
⟺
P
\mathbf{\neg(\neg P)\Longleftrightarrow P}
¬(¬P)⟺P
德摩根律：
¬
(
P
∧
Q
)
⟺
¬
P
∨
¬
Q
\mathbf{\neg(P \land Q)\Longleftrightarrow \neg P \lor \neg Q}
¬(P∧Q)⟺¬P∨¬Q
¬
(
P
∨
Q
)
⟺
¬
P
∧
¬
Q
\mathbf{\neg(P \lor Q)\Longleftrightarrow \neg P \land \neg Q}
¬(P∨Q)⟺¬P∧¬Q
量词转换律：
¬
(
∀
x
)
P
⟺
(
∃
x
)
¬
P
\mathbf{\neg(\forall x)P \Longleftrightarrow(\exists x)\neg P}
¬(∀x)P⟺(∃x)¬P
¬
(
∃
x
)
P
⟺
(
∀
x
)
¬
P
\mathbf{\neg(\exists x)P \Longleftrightarrow(\forall x)\neg P}
¬(∃x)P⟺(∀x)¬P
把否定符号移到紧靠谓词的位置上，减少了否定符号的辖域。
上列等式变换为：
(
∀
x
)
{
(
∃
y
)
¬
P
(
x
,
y
)
∨
(
∃
y
)
[
Q
(
x
,
y
)
∨
¬
R
(
x
,
y
)
]
}
\mathbf{(\forall x)\{(\exists y)\neg P(x,y)\lor(\exists y)[Q(x,y)\lor \neg R(x,y)]\}}
(∀x){(∃y)¬P(x,y)∨(∃y)[Q(x,y)∨¬R(x,y)]}
(3)变量标准化
所谓变量标准化就是重新命名变元，使每个量词采用不同的变元，从而使不同量词的约束变元有不同的名字。这是因为在任一量词辖域内，受到该量词约束的变元为一哑元（虚构变量），它可以在该辖域内被另一个没有出现过的任意变元统一代替，而不改变谓词公式的值。
(
∀
x
)
P
(
x
)
≡
(
∀
y
)
P
(
y
)
(
∃
x
)
P
(
x
)
≡
(
∃
y
)
P
(
y
)
\mathbf{(\forall x)P(x)\equiv (\forall y)P(y)}\\ \mathbf{(\exists x)P(x)\equiv (\exists y)P(y)}
(∀x)P(x)≡(∀y)P(y)(∃x)P(x)≡(∃y)P(y)
上面等价变换为：
(
∀
x
)
{
(
∃
y
)
¬
P
(
x
,
y
)
∨
(
∃
z
)
[
Q
(
x
,
z
)
∧
¬
R
(
x
,
z
)
]
}
\mathbf{(\forall x)\{(\exists y)\neg P(x,y)\lor(\exists z)[Q(x,z)\land \neg R(x,z)]\}}
(∀x){(∃y)¬P(x,y)∨(∃z)[Q(x,z)∧¬R(x,z)]}
(4)消去存在量词
分两种情况：
一种情况是存在量词不出现在全称量词的辖域内。此时只要用一个新的个体常量替换受该存在量词约束的变元，就可以消去存在量词。因为如原谓词公式为真，则总能找到一个个体常量，替换后仍然使谓词公式为真。这里的个体常量就是不含变量的
S
k
o
l
e
m
Skolem
Skolem函数。
另一种情况是存在量词出现在一个或者多个全称量词的辖域内。此时要用 S k o l e m Skolem Skolem函数替换受该存在量词约束的变元，从而消去存在量词。这里认为所存在的y依赖于x值，它们的依赖关系由Skolem函数所定义。
对于一般情况：
(
∀
x
1
)
(
∀
x
2
)
.
.
.
(
∀
x
n
)
(
∃
y
)
P
(
x
1
,
x
2
,
.
.
.
,
x
n
,
y
)
\mathbf{(\forall x_1)(\forall x_2)...(\forall x_n)(\exists y)P(x_1,x_2,...,x_n, y)}
(∀x1)(∀x2)...(∀xn)(∃y)P(x1,x2,...,xn,y)
存在量词
y
y
y的
S
k
o
l
e
m
Skolem
Skolem函数记为：
y
=
f
(
x
1
,
x
2
,
.
.
.
,
x
n
)
\mathbf{y=f(x_1,x_2,...,x_n)}
y=f(x1,x2,...,xn)
可见，
S
k
o
l
e
m
Skolem
Skolem函数把每个
x
1
,
x
2
,
.
.
.
,
x
n
x_1,x_2,...,x_n
x1,x2,...,xn值，映射到存在的那个
y
y
y。
用 S k o l e m Skolem Skolem函数代替每个存在量词量化的变量的过程称为 S k o l e m Skolem Skolem化。 S k o l e m Skolem Skolem函数所使用的函数符号必须是新的。
对于上面的例子，存在量词
(
∃
y
)
(\exists y)
(∃y)及
(
∃
z
)
(\exists z)
(∃z)都位于全称量词
(
∀
x
)
(\forall x)
(∀x)的辖域内，所以都需要用
S
k
o
l
e
m
Skolem
Skolem函数代替。设
y
y
y和
z
z
z的
S
k
o
l
e
m
Skolem
Skolem函数分别记为
f
(
x
)
f(x)
f(x)和
g
(
x
)
g(x)
g(x)，则替换后得到
(
∀
x
)
{
¬
P
(
x
,
f
(
x
)
)
∨
[
Q
(
x
,
g
(
x
)
)
∧
¬
R
(
x
,
g
(
x
)
)
]
}
\mathbf{(\forall x)\{\neg P(x, f(x))\lor[Q(x, g(x))\land \neg R(x, g(x))]\}}
(∀x){¬P(x,f(x))∨[Q(x,g(x))∧¬R(x,g(x))]}
(5)化为前束形
所谓前束形，就是把所有的全称量词都移到公式的前面，使每个量词的辖域都包括公式后的整个部分，即：
前束形
=
(
前缀
)
{
母式
}
\pmb{前束形=(前缀)\{母式\}}
前束形=(前缀){母式}
其中，（前缀）是全称量词串，{母式}是不含量词的谓词公式。
对上面的例子，因为只有一个全称量词，而且已经位于公式的最左边，所以，这一步不需要做任何工作。
(6)化为
S
k
o
l
e
m
Skolem
Skolem标准形
S
k
o
l
e
m
Skolem
Skolem标准形的一般形式是：
(
∀
x
1
)
(
∀
x
2
)
.
.
.
(
∀
x
n
)
M
\mathbf{(\forall x_1)(\forall x_2)...(\forall x_n)M}
(∀x1)(∀x2)...(∀xn)M
其中，
M
M
M是子句的合取式，称为
S
k
o
l
e
m
Skolem
Skolem标准形的母式。
一般利用：
P
∨
(
Q
∧
R
)
⇔
(
P
∨
Q
)
∧
(
P
∨
R
)
P
∧
(
Q
∨
R
)
⇔
(
P
∧
Q
)
∨
(
P
∧
R
)
\mathbf{P \lor(Q\land R) \Leftrightarrow(P\lor Q)\land (P\lor R)}\\ \mathbf{P \land(Q\lor R) \Leftrightarrow(P\land Q)\lor (P\land R)}
P∨(Q∧R)⇔(P∨Q)∧(P∨R)P∧(Q∨R)⇔(P∧Q)∨(P∧R)
把谓词公式化为
S
k
o
l
e
m
Skolem
Skolem标准形。
对于上面的例子，有
(
∀
x
)
{
[
¬
P
(
x
,
f
(
x
)
)
∨
Q
(
x
,
g
(
x
)
)
]
∧
[
¬
P
(
x
,
f
(
x
)
)
∨
¬
R
(
x
,
g
(
x
)
)
]
}
\mathbf{(\forall x)\{[\neg P(x, f(x))\lor Q(x, g(x))]\land[\neg P(x,f(x))\lor \neg R(x,g(x))]\}}
(∀x){[¬P(x,f(x))∨Q(x,g(x))]∧[¬P(x,f(x))∨¬R(x,g(x))]}
(7)略去全称量词
由于公式中所有变量都是全称量词量化的变量，因此，可以省略全称量词。母式中的变量仍然认为是全称量词量化的变量。
对于上面的例子，有：
[
¬
P
(
x
,
f
(
x
)
)
∨
Q
(
x
,
g
(
x
)
)
]
∧
[
¬
P
(
x
,
f
(
x
)
)
∨
¬
R
(
x
,
g
(
x
)
)
]
\mathbf{[\neg P(x, f(x))\lor Q(x, g(x))]\land [\neg P(x, f(x))\lor \neg R(x, g(x))]}
[¬P(x,f(x))∨Q(x,g(x))]∧[¬P(x,f(x))∨¬R(x,g(x))]
(8)消去合取词，把母式用子句集表示
对于上面的例子，有：
{
¬
P
(
x
,
f
(
x
)
)
∨
Q
(
x
,
g
(
x
)
)
,
¬
P
(
x
,
f
(
x
)
)
∨
¬
R
(
x
,
g
(
x
)
)
}
\mathbf{\{\neg P(x, f(x))\lor Q(x, g(x)), \neg P(x, f(x))\lor \neg R(x, g(x)) \}}
{¬P(x,f(x))∨Q(x,g(x)),¬P(x,f(x))∨¬R(x,g(x))}
(9)子句变量标准化，即使每个子句中的变量符号不同
谓词公式的性质有：
(
∀
x
)
[
P
(
x
)
∧
Q
(
x
)
]
≡
(
∀
x
)
P
(
x
)
∧
(
∀
y
)
Q
(
y
)
\mathbf{(\forall x)[P(x)\land Q(x)]\equiv (\forall x)P(x)\land(\forall y)Q(y)}
(∀x)[P(x)∧Q(x)]≡(∀x)P(x)∧(∀y)Q(y)
对于上面的例子，有：
{
¬
P
(
x
,
f
(
x
)
)
∨
Q
(
x
,
g
(
x
)
)
,
¬
P
(
y
,
f
(
y
)
)
∨
¬
R
(
y
,
g
(
y
)
)
}
\mathbf{\{\neg P(x, f(x))\lor Q(x, g(x)), \neg P(y, f(y))\lor \neg R(y, g(y)) \}}
{¬P(x,f(x))∨Q(x,g(x)),¬P(y,f(y))∨¬R(y,g(y))}
显然，在子句集中各子句之间是合取关系。
下面举个课本上的例子熟练下：
