参考链接： 人工智能的推理规则
文章目录
永真性&永假性可满足性（相容性）谓词公式的范式前束范式Skolem范式
永真性&永假性
如果谓词公式P对非空个体域D上的任一解释都取得真值T（F），则称P在D上是永真（永假）的。
如果P在任何非空个体域上均是永真（永假）的，则称P永真（永假）。
可满足性（相容性）
对于谓词公式P，如果至少存在D上的一个解释，使公式P在此解释下的真值为T，则称公式P在D上是可满足的。
谓词公式的范式
前束范式
设F为一个谓词公式，如果其中所有的两次均非否定的出现在公式的最前面，而它们的辖域为整个公式，则称F为前束范式。一般前束范式可以写成:
(
Q
1
x
1
)
(
Q
2
x
2
)
.
.
.
(
Q
n
x
n
)
M
(
x
1
,
x
2
,
.
.
.
x
n
)
(Q_1x_1)(Q_2x_2)...(Q_nx_n)M(x_1,x_2,...x_n)
(Q1x1)(Q2x2)...(Qnxn)M(x1,x2,...xn)
式中的
Q
i
Q_i
Qi为前缀，它是一个由全称量词或存在量词组成的量词串，
M
(
x
1
,
x
2
,
.
.
.
,
x
n
)
M(x_1,x_2,...,x_n)
M(x1,x2,...,xn)为母式，是一个不含任何量词的谓词公式。
Skolem范式
如果前束范式中所有的存在量词都在全称量词之前，则称这种形式的谓词公式为Skolem范式。
例如，
(
∃
x
)
(
∃
z
)
(
∀
y
)
(
P
(
x
)
∨
Q
(
y
,
z
)
∧
R
(
x
,
z
)
)
(exists x)(exists z)(forall y)(P(x)lor Q(y,z)land R(x,z))
(∃x)(∃z)(∀y)(P(x)∨Q(y,z)∧R(x,z))就是Skolem范式。
