概念引入:

前束范式的概念:

一个公式,如果量词均在全式的开头,它们的作用域延伸到整个公式的末端,则该公式叫做前束范式(Prenex Normal Form)。

前束范式可记为下Q述形式

其中Qi为任意或者存在,xi为个体变元,A是没有量词的谓词公式。

例如,

等都是前束范式,而

等都不是前束范式。

定义 设P是具有形式

的前束范式,若A是合取范式,则称P为前束合取范式;若A是析取范式,则称P为前束析取范式。

利用换名规则、代替规则、量词的否定公式及量词辖域的扩张与收缩公式等,可以将任一谓词公式化成前束范式。 [2]

PS:如果一个公式单独只有A,那么该公式也是前束范式。

求前束范式的方法:

(1)通过利用公式

及 消去渭词公式中的联结词 和 ;

(2)利用量词转换把 否定深入到原子谓词公式前,即利用量词转化公式把否定联结词深入到命题变元和谓词填式的前面;

(3)运用换名规则和代替规则,将公式中所有变元均用不同的符号;

(4)利用量词辖域的扩张收缩律,量词前移,即利用量词辖域的扩张把量词移到前面。

注意:

规范性:(Q1x1)(Q2x2)(A1A2)

在将(Q2x2)前移中,A2也要随之前移,(Q2x2)(Q1x1)(A2A1)

就像队列一样(先进先出,后进后出)