参考自http://www.ycrc.com.cn/qinghua/18/text/chapter4/section1/1.htm
标准式的化简步骤
如果一个合适公式的所有量词均非否定的出现在公式的前部,而且所有的量词的
约束范围均是整个公式,则称这样的合适公式为前束范式。任何一个合适公式,
都可以等价地转化为一个前束范式。消去前束范式中所有的存在量词后得到的
合适公式,称为S范式,这一过程称作skolem化。S范式与它的原式不一定等价,
但在不可满足性方面,二者是等价的。也就是说,如果原式是不可满足的,
则其对应的S范式也一定是不可满足的。反之亦成立。
(1)消蕴涵符
(2)移动否定符
如果公式中的否定符"~"不只是作用于原子公式,则要利用摩根定律对公式进行变换,
使得否定符只作用于原子公式。
如果否定作用于量词的话,可以用量词转换律将量词提到否定的作用域之外。
(3)变量换名
(4)量词左移
将所有的量词移到公式的左边,但不改变原来各量词的排列顺序。
这也是为什么在第三步要进行变量改名的原因,否则就不能进行这种移动。
(5)消去存在量词(skolem化)
按照这样的原则将公式中的存在量词消去:设E是前束范式中的一个存在量词,
如果在它的前面没有出现全称量词,则所约束的变量x,全部用一个新的常量
(未在公式中出现过)代替;如果E前面有全称量词,则所约束的变量x,
全部用一个新的(未在公式出现过的)函数(称为skolem函数)代替,该函数的
变量是哪些在前面的全称量词所约束的变量。然后将存在量词E消去。
(6)化为合取范式
利用结合律、分配律等,可以把S范式的母式转化为合取范式。
A(x)∨(B(x)∧C(x)) ≡ (A(x)∨B(x))∧(A(x)∨C(x))
(7)隐去全称量词
经过前6步变换以后,所有的变量都是受全称量词约束,所以可以将全称量词隐去,
默认所有的变量是受全称量词约束的。
(8)表示为子句集
在隐去全称量词以后,用","号代替公式中的"∧",并用"{"和"}"括起来,就得到了
原合适公式的子句集。
(9)变量换名
对子句集中的变量再次进行换名替换,使得不同的子句中的变量使用不同的名字。
最简单的方法是采用加下标的方法。注意:在有些书中并不要求对子句集中的变量
进行换名替换,如果是这样的话,你必须很清楚,不同子句中的变量,即便是同名的,
也可以代表不同的变量。在后边将要介绍的归结法中,你会发现,如果不进行换名,
很容易出现错误。因此建议大家对变量进行换名。由于每一个子句都对应一个不同的
合取元,变量都由全称量词量化,因而实质上两个子句的变量之间不存在任何关系,
这里的变量换名不影响公式的真值。
---------------------------------------------------
Skolem化并不影响原合适公式的永假特性
---------------------------------------------------
posted on 2009-08-05 09:56
lingol 阅读(3785)
评论(1) 编辑 收藏 引用