概念引入:
前束范式的概念:
一个公式,如果
量词均在全式的开头,它们的作用域延伸到整个公式的末端,则该公式叫做前束范式(Prenex Normal Form)。
前束范式可记为下Q述形式
其中Qi为任意或者存在,xi为个体变元,A是没有量词的谓词公式。

利用换名规则、代替规则、量词的否定公式及量词辖域的扩张与收缩公式等,可以将任一
谓词公式化成前束范式。
[2]
PS:如果一个公式单独只有A,那么该公式也是前束范式。
(1)通过利用公式
及
消去渭词公式中的联结词
和
;




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

(3)运用
换名规则和代替规则,将公式中所有变元均用不同的符号;
(4)利用量词辖域的
扩张收缩律,量词前移,即利用量词辖域的扩张把量词移到前面。
注意:
规范性:(Q1x1)(Q2x2)(A1A2)
在将(Q2x2)前移中,A2也要随之前移,(Q2x2)(Q1x1)(A2A1)
就像队列一样(先进先出,后进后出)