基本介紹
- 中文名：斯科倫範式
- 外文名：Skolem normal form
- 套用學科：離散數學
定義
設G是一個公式，G1x1…GnxnM是與G等價的前束範式，其中M為合取範式形式。若Qr是存在量詞，並且它左邊沒有全稱量詞，則取異於出現在M中所有常量符號的常量符號c，並用c代替M中所有xr，然後在首標中刪除Qrxr.
若Qsi,…,Qsm是所有出現在Qrxr左邊的全稱量詞（m≥1，1≤s1<s2<…<sm<r），則取異於出現在M中所有函式符號的m元函式符號f(xs1,…,xsm),用f(xs1,…,xsm)代替出現在M中所有xr，然後在首標中刪除Qrxr。
對首標中的所有存在兩次做上述處理後，得到一個在首標中沒有存在量詞的前束範式，這個前束範式成為公式G的斯科倫範式，其中用來代替xr的那些常量符號和函式符號成為斯科倫函式。
例：G=∃x∀y∀z∃u∀v∃wP(x,y,z,u,v,w)
用a代替x
用f(y,z)代替u
用g(y,z,v)代替w
得到公式G的斯科倫範式：
∀y∀z∀vP(a,y,z,f(y,z),v,g(y,z,v))
