重点：掌握基本等值式，(量词否定等值式，量词辖域收缩与扩张等值式，量词分配等值式)的内容。

一、谓词逻辑等值式

　　定义：若 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image003.gif 为逻辑有效式 (其中 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image004.gif 为逻辑公式)，则称 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image005.gif 与 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image006.gif 等值，记 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image007.gif ，称 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image007.gif 为等值式。

　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image008.gif

　　以下，再给出其他一些重要的等值式(证明略去)

1、量词否定等值式。

　　(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image009.gif

　　(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image010.gif

2、量词辖域收缩与扩张等值式。

　　(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image011.gif

　　(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image012.gif

　　(3) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image013.gif

　　(4) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image014.gif

　　(5) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image015.gif

　　(6) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image016.gif

　　(7) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image017.gif

　　(8) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image018.gif

　　在以上各公式中， http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image005.gif 是含 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image019.gif 自由出现的任意的公式，而 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image006.gif 中不含 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image019.gif 的出现。

3、量词分配等值式。

　　(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image020.gif

　　(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image021.gif

注意： http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image022.gif

　　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image023.gif

4、多个量词间的次序排列等值式。

　　(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image024.gif

　　(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image025.gif

二、前束范式

　　命题公式有范式，主范式，同样，谓词逻辑也有规范形式，这就是前束范式。

　　前束范式：若谓词公式 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image005.gif 具有形式 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image026.gif ，则称 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image005.gif 是前束范式，其中每个 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image027.gif 为 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image028.gif 或 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image029.gif ， http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image006.gif 为不含量词的谓词公式。

　　例如： http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image030.gif ， http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image031.gif ， http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image032.gif 等都是前束范式，而 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image033.gif ， http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image034.gif 等都不是前束范式。

　　例1、求下列公式的前束范式。

　　(1) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image035.gif

　　解： http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image036.gif

　　　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image037.gif 量词否定等值式

　　　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image028.gif 对 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image039.gif 的分配

　　(2) http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image040.gif

　　解： http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image040.gif

　　　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image041.gif 量词否定等值式

　　　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image042.gif 换名规则

　　　　 http://cise.sdkd.net.cn/lssx/7stressresolve/cha2/23.files/image043.gif 量词辖域的扩张