确定性知识推理：谓词知识点_化子句集 例题

1.重要的谓词公式

P∨(Q∧R) ⇔ (P∨Q)∧(P∨R)

转换:

P→Q ⇔﹁ P∨Q
P↔Q ⇔ (P∧Q)∨(﹁P∧﹁Q)

双重否定定律

﹁(﹁P) ⇔ P

摩根定律

﹁(P∧Q) ⇔﹁P∨﹁Q
﹁(P∨Q) ⇔﹁P∧﹁Q

量词转换律

﹁ (∀x)P(x) ⇔ (∃x) ﹁P(x)
﹁ (∃x)P(x) ⇔ (∀x)￢P(x)

2.谓词公式化为子句集

例 请将下述谓词公式化为子句集：
(∀x)((∀y)P(x,y)→﹁ (∀y)(Q(x,y)→R(x,y)))
解
(∀x)(﹁(∀y)P(x,y)∨﹁ (∀y)(﹁Q(x,y)∨R(x,y)))----------(1) 消去连接词“→”和“↔”
(∀x)((∃y)﹁P(x，y)∨(∃y)( Q(x，y) ∧﹁R(x，y)))------------(2) 将否定符号“﹁”移到最紧靠谓词的位置
(∀x)((∃y)﹁P(x，y)∨(∃z)( Q(x，z) ∧﹁R(x，z)))------------(3) 对变元标准化
(∀x)(∃y) (∃z)(﹁P(x，y)∨( Q(x，z) ∧﹁R(x，z)))-----------(4) 化为前束范式
(∀x)(﹁P(x,f(x))∨ (Q(x,g(x))∧﹁ R(x,g(x)) ) )-------------(5) 消去存在量词
(∀x)((﹁P(x,f(x))∨Q(x,g(x))∧(﹁P(x,f(x))∨﹁R(x,g(x))))----------(6) 化为Skolem标准形
(﹁P(x,f(x))∨Q(x,g(x)) ∧(﹁P(x,f(x))∨﹁R(x,g(x)))-----------(7) 消去全称量词
(﹁P(x,f(x))∨Q(x,g(x)) ∧(﹁P(y,f(y))∨﹁R(y,g(y)))------------(8) 消去合取词 (9) 更换变量名称
消去合取词后，上式就变为下述子句集：
{ ﹁P(x, f (x))∨Q(x, g (x))
﹁P(y, f (y))∨R(y, g (y)) }

原文传送门：https://www.jianshu.com/p/4e7f9e48c86b