posts - 9,  comments - 11,  trackbacks - 0

参考自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 阅读(3674) 评论(1)  编辑 收藏 引用

FeedBack:
# re: 一阶谓词逻辑归结推理系统(2)--Skolem化步骤
2009-09-25 15:04 | 飞机
.。。。。来了。。。好失望。。  回复  更多评论
  

只有注册用户登录后才能发表评论。
网站导航: 博客园   IT新闻   BlogJava   知识库   博问   管理


<2009年9月>
303112345
6789101112
13141516171819
20212223242526
27282930123
45678910

留言簿(5)

随笔档案

文章档案

搜索

  •  

最新评论

阅读排行榜

评论排行榜