离散数学：第四章 第二节 范式 [兼容模式].pdfVIP

2011-11-16 第四章归结法原理 §4.2 前束范式与斯科伦范式 §4.1 命题逻辑的归结法 在命题逻辑中，为了用归结法判断一个公式是否是 §4.2 前束范式与斯科伦范式 另一些公式的逻辑推论，首先需要将公式化为标准 §4.3 谓词逻辑的归结法 形式—合取范式。 作业 在谓词逻辑中，为了用归结法判断一个语句是否是 另一些语句的逻辑推论，首先需要将语句化为标准 形式—斯科伦范式。 定义4.5 形式为 Q y … Q y B 的公式称为前束范 可以通过等值演算将一个公式化为前束范式。 1 1 n n 式，其中n 为非负整数，每个 Qi 是 ∀或 ∃，B 是 例 通过等值演算将公式 开公式，y , …, y 是不同变元。称 Q y …Q y 为 1 n 1 1 n n Q(x) ∧(∃xP(x) →∀xR(x)) 该前束范式的前束词，称B 为它的母式。 化为前束范式。 开公式是前束范式，这时 n = 0 ，前束词是空串。 Q(x) ∧(∃xP(x) →∀xR(x)) 当一个前束范式不是开公式时当一个前束范式不是开公式时，它的所有量词都出它的所有量词都出 ⇔Q(x) ∧∀x(P(x) →∀xR(x)) 现在最前面，并且它们的辖域都一直管到底。 因为x 是公式P(x) 中的自由变元，所以 前束范式： ∀x∃y ∃z(P(x , y ) →Q(u, v)) ，P(x , y ) P(x) →∀xR(x) ⇔∀x(P(x) →R(x)) 非前束范式： ∀xP(x) ∧Q(y ) ，因为 ∀x 的辖域是 不成立。需要将约束变元换名。 P(x) ，而不是P(x) ∧Q(y ) 。 Q(x) ∧∀x(P(x) →∀xR(x)) 与公式A 等值的前束范式称为A 的前束范式。 ⇔Q(x) ∧∀x(P(x) →∀yR (y )) 例4.8 通过等值演算求公式 ∀xP(x) ↔¬∃yQ (x , y ) ⇔Q(x) ∧∀x∀y (P(x) →R(y )) 的前束范式。 因为x 是公式 Q(x) 中的自由变元，所以 解 ∀xP(x) ↔¬∃yQ (x , y ) Q(x) ∧∀x∀y (P(x) →R(y )) ⇔(∀xP(x) →¬∃yQ (x , y )) ∧(¬∃yQ (x , y ) →∀xP(x))