English Dictionary

Skolemization

名詞

不可算名詞

(logic) The conversion of a formula of first-order logic which involves the following steps: (1) replace free variables with constants, (2) replace any variable bound by an existential quantifier which lies in the scope of an even number of logical negations with a Skolem function, and (3) replace any variable bound by a universal quantifier which lies in the scope of an odd number of negations with a Skolem function.

日本語の意味

ファーストオーダー論理の式に対して、以下の手順で変換を行う操作。まず自由変数を定数に置換し、その後、論理否定が偶数回適用された範囲内で存在記号に束縛された変数をSkolem関数に、さらに論理否定が奇数回適用された範囲内で普遍記号に束縛された変数をSkolem関数に置換する手続き。

Skolemization makes automated theorem proving more efficient by transforming first-order formulas into a form without existential quantifiers.

スコーレム化とは、一階述語論理の式を (1) 自由変数を定数に置き換え、(2) 偶数回の否定の範囲にある存在量化子に束縛された変数をスコーレム関数に置き換え、(3) 奇数回の否定の範囲にある全称量化子に束縛された変数をスコーレム関数に置き換える、という手順で変換して存在量化子のない形に整え、自動定理証明の効率を高める技法である。

意味（1）

(logic) The conversion of a formula of first-order logic which involves the following steps: (1) replace free variables with constants, (2) replace any variable bound by an existential quantifier which lies in the scope of an even number of logical negations with a Skolem function, and (3) replace any variable bound by a universal quantifier which lies in the scope of an odd number of negations with a Skolem function.