斯科伦范式是数理逻辑中的一类合式公式。
斯科伦范式是数理逻辑中的一类合式公式。
一前束范式是斯科伦范式,如果其中的存在量词都在全称量词的左方出现。
定义
设G是一个公式,G1x1…GnxnM是与G等价的前束范式,其中M为合取范式形式。若Qr是存在量词,并且它左边没有全称量词,则取异于出现在M中所有常量符号的常量符号c,并用c代替M中所有xr,然后在首标中删除Qrxr.
若Qsi,…,Qsm是所有出现在Qrxr左边的全称量词(m≥1,1≤s1
对首标中的所有存在两次做上述处理后,得到一个在首标中没有存在量词的前束范式,这个前束范式成为公式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))