将蕴涵符号化为析取和否定符号

(2)減少否定符号的辖域

每个否定符号最多只用到一个谓词符号上并反复应用狄·摩根定律

对哑元改名以保证每个量词有其自己唯一的哑元

引入Skolem函数，消去存在量词

如果要消去的存在量词不在任何一个全称量词的辖域内那么我们就用不含变量的Skolem 函数即常量。

把所有全称量词迻到公式的左边并使每个量词的辖域包括这个量词后面公式的整个部分。前束形= (前缀) (母式)

(6)把母式化为合取范式

反复应用分配律将母式寫成许多合取项的合取的形式，而每一个合取项是一些谓词公式和(或)谓词公式的否定的析取

消去前缀即消去明显出现的全称量词

(8)消去连詞符号(合取)

用{合取项1,合取项2}替换明显出现的合取符号

更换变量符号的名称，使一个变量符号不出现在一个以上的子句中

3-4 如何通过消解反演求取问题的***?

给出一个公式集S和目标公式L通过反证或反演来求证目标公式L，其证明步骤如下：

(1)否定L得～L；

(2)把～L添加到S中去；

(3)把新产苼的集合｛～L，S｝化成子句集；

(4)应用消解原理力图推导出一个表示矛盾的空子句NIL。

3-5 什么叫合适公式?合适公式有哪些等价关系?

合式公式的遞归定义为：

(1) 原子谓词公式是合式公式

(2) 若A为合式公式则A的否定也是合式公式

感谢你的反馈我们会做得更好！