斯科伦范式维基百科,自由的 encyclopedia 如果一阶逻辑式的前束范式只有全称量词,则称其为是符合Skolem 范式的。一个公式可以被Skolem 化,就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下二阶逻辑的等价应用: ∀ x ∃ y R ( x , y ) ⇔ ∀ x R ( x , f ( x ) ) {\displaystyle \forall x\exists yR(x,y)\Leftrightarrow \forall xR(x,f(x))} Skolem 化的本质是对如下形式的公式的观察 ∀ x 1 … ∀ x n ∃ y R ( x 1 , … , x n , y ) {\displaystyle \forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)} 它在某个模型中是可满足的,在这个模型必定对于所有的 x 1 , … , x n {\displaystyle x_{1},\dots ,x_{n}} 有某些点 y {\displaystyle y} 使得 R ( x 1 , … , x n , y ) {\displaystyle R(x_{1},\dots ,x_{n},y)} 为真,并且必定存在某个函数(选择函数) y = f ( x 1 , … , x n ) {\displaystyle y=f(x_{1},\dots ,x_{n})} 使得公式 ∀ x 1 … ∀ x n R ( x 1 , … , x n , f ( x 1 , … , x n ) ) {\displaystyle \forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))} 为真。函数 f 叫做 Skolem 函数。 举例说明: ∃ x ∀ y R ( x , y ) ⇒ ∀ y R ( a , y ) {\displaystyle \exists x\forall yR(x,y)\Rightarrow \forall yR(a,y)} 其中a为常数 ∀ x ∃ y R ( x , y ) ⇔ ∀ x R ( x , f ( x ) ) {\displaystyle \forall x\exists yR(x,y)\Leftrightarrow \forall xR(x,f(x))} ∀ x ∀ y ∃ z R ( x , y , z ) ⇔ ∀ x ∀ y R ( x , y , f ( x , y ) ) {\displaystyle \forall x\forall y\exists zR(x,y,z)\Leftrightarrow \forall x\forall yR(x,y,f(x,y))}
如果一阶逻辑式的前束范式只有全称量词,则称其为是符合Skolem 范式的。一个公式可以被Skolem 化,就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下二阶逻辑的等价应用: ∀ x ∃ y R ( x , y ) ⇔ ∀ x R ( x , f ( x ) ) {\displaystyle \forall x\exists yR(x,y)\Leftrightarrow \forall xR(x,f(x))} Skolem 化的本质是对如下形式的公式的观察 ∀ x 1 … ∀ x n ∃ y R ( x 1 , … , x n , y ) {\displaystyle \forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)} 它在某个模型中是可满足的,在这个模型必定对于所有的 x 1 , … , x n {\displaystyle x_{1},\dots ,x_{n}} 有某些点 y {\displaystyle y} 使得 R ( x 1 , … , x n , y ) {\displaystyle R(x_{1},\dots ,x_{n},y)} 为真,并且必定存在某个函数(选择函数) y = f ( x 1 , … , x n ) {\displaystyle y=f(x_{1},\dots ,x_{n})} 使得公式 ∀ x 1 … ∀ x n R ( x 1 , … , x n , f ( x 1 , … , x n ) ) {\displaystyle \forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))} 为真。函数 f 叫做 Skolem 函数。 举例说明: ∃ x ∀ y R ( x , y ) ⇒ ∀ y R ( a , y ) {\displaystyle \exists x\forall yR(x,y)\Rightarrow \forall yR(a,y)} 其中a为常数 ∀ x ∃ y R ( x , y ) ⇔ ∀ x R ( x , f ( x ) ) {\displaystyle \forall x\exists yR(x,y)\Leftrightarrow \forall xR(x,f(x))} ∀ x ∀ y ∃ z R ( x , y , z ) ⇔ ∀ x ∀ y R ( x , y , f ( x , y ) ) {\displaystyle \forall x\forall y\exists zR(x,y,z)\Leftrightarrow \forall x\forall yR(x,y,f(x,y))}