发布网友 发布时间:2022-05-06 16:12
共1个回答
热心网友 时间:2023-10-11 10:49
Skolem标准形的定义: 前束范式中消去所有的存在量词,则称这种形式的谓词公式为Skolem标准形,任何一个谓词公式都可以化为与之对应的Skolem标准形。但是,Skolem标准形不唯一。 前束范式:A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。 Skolem标准形的转化过程为,依据约束变量换名规则,首先把公式变型为前束范式,然后依照量词消去原则消去或者略去所有量词。具体步骤如下: 将谓词公式G转换成为前束范式 前束范式的形式为: (Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn) 即: 把所有的量词都提到前面去。 注意:由于所有的量词的辖域都延伸到公式的末端,即,最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。 约束变量换名规则: (Qx ) M(x) (Qy ) M(y) (Qx ) M(x,z) (Qy ) M(y,z) 量词否定等值式: ~(x ) M(x) (y ) ~ M(y) ~(x ) M(x) (y ) ~ M(y) 量词分配等值式: (x )( P(x) ∧Q(x)) (x ) P(x) ∧ (x ) Q(x) (x )( P(x) ∨ Q(x)) (x ) P(x) ∨ (x ) Q(x) 消去量词等值式:设个体域为有穷集合(a1, a2, …an) (x ) P(x) P(a1) ∧ P(a2) ∧ …∧ P(an) (x ) P(x) P(a1) ∨ P(a2) ∨ … ∨ P(an) 量词辖域收缩与扩张等值式: ( x )( P(x) ∨ Q) ( x ) P(x) ∨ Q (x )( P(x) ∧ Q) ( x ) P(x) ∧ Q (x )( P(x) → Q) (x ) P(x) → Q (x )( Q → P(x) ) Q → (x ) P(x) (x )( P(x) ∨ Q) (x ) P(x) ∨ Q (x )( P(x) ∧ Q) (x ) P(x) ∧ Q (x )( P(x) → Q) (x ) P(x) → Q (x )( Q → P(x) ) Q → (x ) P(x)热心网友 时间:2023-10-11 10:49
Skolem标准形的定义: 前束范式中消去所有的存在量词,则称这种形式的谓词公式为Skolem标准形,任何一个谓词公式都可以化为与之对应的Skolem标准形。但是,Skolem标准形不唯一。 前束范式:A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。 Skolem标准形的转化过程为,依据约束变量换名规则,首先把公式变型为前束范式,然后依照量词消去原则消去或者略去所有量词。具体步骤如下: 将谓词公式G转换成为前束范式 前束范式的形式为: (Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn) 即: 把所有的量词都提到前面去。 注意:由于所有的量词的辖域都延伸到公式的末端,即,最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。 约束变量换名规则: (Qx ) M(x) (Qy ) M(y) (Qx ) M(x,z) (Qy ) M(y,z) 量词否定等值式: ~(x ) M(x) (y ) ~ M(y) ~(x ) M(x) (y ) ~ M(y) 量词分配等值式: (x )( P(x) ∧Q(x)) (x ) P(x) ∧ (x ) Q(x) (x )( P(x) ∨ Q(x)) (x ) P(x) ∨ (x ) Q(x) 消去量词等值式:设个体域为有穷集合(a1, a2, …an) (x ) P(x) P(a1) ∧ P(a2) ∧ …∧ P(an) (x ) P(x) P(a1) ∨ P(a2) ∨ … ∨ P(an) 量词辖域收缩与扩张等值式: ( x )( P(x) ∨ Q) ( x ) P(x) ∨ Q (x )( P(x) ∧ Q) ( x ) P(x) ∧ Q (x )( P(x) → Q) (x ) P(x) → Q (x )( Q → P(x) ) Q → (x ) P(x) (x )( P(x) ∨ Q) (x ) P(x) ∨ Q (x )( P(x) ∧ Q) (x ) P(x) ∧ Q (x )( P(x) → Q) (x ) P(x) → Q (x )( Q → P(x) ) Q → (x ) P(x)