Herbrand定理 王珏 张文生 中国科学院自动化研究所.

Presentation on theme: "Herbrand定理 王珏 张文生 中国科学院自动化研究所."— Presentation transcript:

1 Herbrand定理 王珏 张文生 中国科学院自动化研究所

2 内容 Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作

3 复习 定义(定理) 定理 如果G是公式F1, F2,… Fn的逻辑结论, 则公式 (F1∧F2∧…∧Fn)→G 称为定理.
给定公式F1, F2,… Fn和G, G是公式F1, F2,… Fn的逻辑结论, 当且仅当公式 F1∧F2∧…∧Fn∧~G 不相容 (是永假式)。

4 化公式为Skolem范式的步骤 公式化为前束范式。 母式化为合取范式。

5 Skolem函数 消去存在量词; 令公式H是一个前束范式，并且母式M是合取范式
(Q1x1)…(Qnxn)(M) 对前缀从左到右遇到的第一个存在量词Qr(1rn), 存在两种情况: (1) 如果Qr的左边(前边)没有全称量词, 则M中的xr 用常数a代替; (2) 如果Qr的左边(前边)有全称量词xs1,…, xsk, 且1s1…skr, 则M中的xr 用函数f(xs1,…, xsk)代替; 从前缀中删除(Qr xr);

6 Skolem函数的意义 化公式为Skolem范式与原来公式在不相容意义下保持等价(=).
定理: 令G是一个前束合取范式，G=(Q1x1)…(Qnxn)M[x1,…,xn]， Qr为G中从左向右遇到的第一个存在量词。令 G1=(Q1x1)…(Qr-1xr-1)(Qr+1xr+1)(Qnxn) M[x1,…,xr-1, f(x1,…,xr-1),xr+1,…,xn] 其中：f(x1,…,xr-1)是xr的Skolem函数. 则有： G不相容 G1不相容

7 注意 Skolem范式和原式在不相容意义下保持等价, 而非等价(=)。 例子: 如果G不相容, 那么按照定理G=G1。
如果G是相容的，一般情况下，G不等价于G1，即：GG1。 例子: G =(x)P(x) G1=P(a) 在解释I下不相等: D={1,2} a=1, P(1)=F, P(2)=T. G在I下为真, G1在I下为假.

8 子句集 Skolem化以后, 将公式表示为子句集合. (x)(y)((P(x)Q(y))  (Q(x)~S(f(y))))
定义(子句, clause): 一个包含若干文字的析取式称为子句。例如： P  ~S  R P(x)  Q(y, z)  ~R(y, y) 说明：一个子句中没有文字则称空子句(, nil, 永假)； 一个子句中有n个文字则称n文字子句。 定义（子句集合）: 子句内部的关系是析取; 子句间的关系是合取; 所有子句受全程量词约束;

9 总结 定理（公式不相容基本定理） 说明： 设S是公式G的子句集, G不相容  S不相容
S不相容: 对任一个解释, S中至少有一个子句为假; S相容: 存在一个解释, 使S中所有子句为真;

10 推论： 如果G=G1…Gn, Si是Gi的子句集, i=1,…,n. 令S’=S1…Sn. G不相容  S’不相容

11 公式不相容基本定理的应用 ——定理证明思路 证明定理G; 证明~G不相容; 证明~G的Skolem范式G1不相容; 证明G1的子句集不相容。

12 Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作

13 我们试图找到：一个比较简单的、特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的?
一阶逻辑下验证定理是困难的原因: 个体变量论域D的任意性. D中元素的任意性. 解释的个数的无限性. 我们试图找到：一个比较简单的、特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的? ——Herbrand域(简称H域)就具有这样的性质。

14 Herbrand域 令H0是子句集S中出现的常量的集合。若S中没有常量出现, 则H0由单个常量a组成(即H0={a})； 对于i=1,2,…
Hi=Hi-1∪{所有形如f(t1,...,tn)的项的集合} 其中：f(t1,...,tn)是出现于S中的任一函数符号t1,...,tnHi-1。 规定H∞为S的Herbrand域（Herbrand universe of S, 简称H域）。

15 基本概念 定义（基础，ground)： 没有变量的项，称为基础项(ground term).
f(a,b) 没有变量的原子，称为基础原子(ground atom). P(a,f(b)) 没有变量的文字，称为基础文字(ground literal). P(a,f(b)), ~P(a,f(b)) 没有变量的子句，称为基础子句(ground clause). P(b,f(b))  ~Q(f(f(b)))

16 原子集 其中：P(t1,...,tn)是出现在S中的任一谓词符号, 而t1,...,tn
定义：令S是一个子句集合，形如P(t1,...,tn)的基础原子集合，称为S的原子集，或Herbrand基，记为A。 其中：P(t1,...,tn)是出现在S中的任一谓词符号, 而t1,...,tn 是S的H域的任意元素。

17 例子 S={P(z), P(x)∨Q(y)} S={P(a), P(x)∨P(f(x))} S={P(f(x), a, g(y), b)}
H∞={a} A={P(a), Q(a)} S={P(a), P(x)∨P(f(x))} H∞={a, f(a), f(f(a)),...} A={P(a), P(f(a)), P(f(f(a))),…， P(a) ∨ P(f(a))，…} S={P(f(x), a, g(y), b)} H∞={a, b, f(a), g(a), f(b), g(b),…} A={P(a,a,a,a), P(a,a,a,b), P(a,a,b,b),...}

18 基础实例 定义：当S中的某子句C中所有变量符号均以S的H域的元素代入时，所得的基子句C’称作C的一个基础实例(基例， a ground instance of a clause C)。 例 S={P(x), Q(f(y))∨R(y), Z(f(y))} H={a,f(a),f(f(a)),...} P(a), P(f(a))都称作子句C=P(x)的基例。 同样, Q(f(a))∨R(a), Q(f(f(a)))∨R(f(a))都是Q(f(y))∨R(y)的基例。 对于任一b∈D,子句P(b), Q(f(b))∨R(b)都叫基子句。 但是，Q(a)∨R(a)不是Q(f(y))∨R(y)的基础实例。

19 注意 原子集和基础实例不同： 原子集考虑单个原子，基础实例考虑子句。 原子集是将某个谓词中的项改为H域中的元素，而基例是改变量。
Q(f(a))∨R(a)是基例，但不属于S的原子集。 原子集是将某个谓词中的项改为H域中的元素，而基例是改变量。 H={a,f(a),f(f(a)),...}. Q(a)不是Q(f(y))的基例, 但是属于S的原子集。 Q(f(a))既是Q(f(y))的基例, 又属于S的原子集。 一个基础实例是由原子集中的原子或原子的非析取而成。 A={P(a), Q(a), R(a), Z(a), P(f(a)), Q(f(a)),...} 基础实例: Q(f(a))∨R(a)

20 H解释 起因 由子句集S建立H域，进而容易得到原子集A； 一般论域D上对S的解释I  H域上的解释I*; S在D上为真  S在H上为真;

21 H解释的表示 令A={A1,…,An ,…}是S的原子集, 一个H解释可被表示为: I={m1,…,mn ,…}
其中：mj或者是Aj，或者是~Aj。 如果mj是Aj, 则Aj为真, 否则, Aj为假。

22 H解释的性质 引理 定理 如果在论域D上的一个解释I满足S，则任一个对应于I的H解释I*，也满足S。
子句集S是不可满足的，当且仅当S的所有的H解释使S为假。

23 结论： 如果S为不满足的，则存在一个特殊域，当S被证明在这个域上的所有解释为F。 即证明了对所有域上的所有解释为F，也就证明了S为不相容的。

24 几个性质 性质1: 一个子句C的基础实例C’被解释I满足, iff存在一个C’的基础文字L’在I下为真, 即C’ I。
C: ~P(x)  Q(f(x)) H: {a, f(a), f(f(a)),…} C’:~P(a)  Q(f(a)) I1: {~P(a), ~Q(a), ~P(f(a)), ~Q(f(a)), …} 性质2: 一个子句C在解释I下为真，iff 这个子句C的每个基础实例被I所满足。 I2: {P(a), Q(a), P(f(a)), Q(f(a)), …}

25 性质3: 一个子句C在解释I下为假，iff 至少存在一个C的基础实例C’，使得C’不被I所满足。
C: ~P(x)  Q(f(x)) H: {a, f(a), f(f(a)),…} C’:~P(a)  Q(f(a)) I3: {P(a), ~Q(a), P(f(a)), ~Q(f(a)), …} 性质4: 子句集S是不可满足的, iff 对每个解释I下，至少有S的某个子句的某个基例不被I所满足。

26 Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作

27 语义树(Semantic tree) 例1 G = P  Q  R S = {P, Q, R} A = {P, Q, R} P ~P Q

28 例2 S={~P(x)Q(x), P(f(y)), ~Q(f(y))} H={a, f(a), f(f(a)), ...}
A={P(a), Q(a), P(f(a)), Q(f(a)), ...} P(a) ~P(a) Q(a) ~Q(a) P(f(a)) ~ P(f(a)) …… …… …… ……

29 注意 颠倒原子的顺序是可以的. 例如Q(a)为第一个顶点. 如果原子集是无限的，则对应的语义树必定是无限的.
从任一个叶节点向根节点看, 代表S的一个解释. 从任一个中间节点向根节点看, 代表S的一个部分解释.

30 一些概念 定义(complementary pair, 互补对) 包含互补对的子句是永真的.
如果A 是一个原子, 那么两个文字A 和~A 成为互补对, 并且 {A, ~A} 称为互补对。 包含互补对的子句是永真的. P  Q  ~Q

31 定义 (semantic tree, 语义树) 给定一个子句集S，令A是一个S的原子集合，一个对S来说的语义树是一个向下的树结构T, 在它的每一条联线上均附加了一个有限的在A中的原子或原子非的集合: 对于每一个节点N, 仅有有限个直接联线 L1,…Ln ，令Qi 是附加在Li（ i=1,…,n）的所有文字的合取，则 Q1 …Qn 是一个永真的命题（基础）. 对于每一个节点N, 令I(N) 是从根节点到N节点的一个分支上的所有附加在个联线上文字集合的并集（包含N），则I(N)不包含任何互补对。 注意： I(N)不是一个解释，它仅是一个解释的一部分。

32 完备语义树（complete semantic tree）
定义: 假设 A={A1, A2, …, Ak,…} 是子句集S的原子集合，一个对S来说的语义树是完备的，iff 对这个语义树的每一个端节点 N ，I(N) 包括Ai 或 ~Ai, 对i=1,2,…都成立.

33 例1 G = P  Q  R S = {P, Q, R} A = {P, Q, R} P ~P Q ~Q R ~R

34 反例 P ~P Q ~Q R ~R P ~P Q ~Q Q ~Q R ~R R ~R

35 完备语义树的性质 一个完备的语义树是对一个公式的全部解释 (全部) 当原子集 A 无限时, 任何完备语义树S 兼时无限的 (无限)
如果S是不可满足的, 那么从某一个节点N以后我们可以停止扩展. (终止)

36 封闭语义树(Closed semantic tree)
定义(failure node, 失败节点, 假节点) 如果I(N)使S中的某个字句的基础实例为假，但是， I(N’)不能使S中的任何子句为假，N’为N的父亲节点，则称N为假节点。

37 例 S={P, QR, ~P~Q, ~P~R} P ~P Q ~Q R ~R

38 定义(Closed semantic tree, 封闭语义树)
一个语义树T是封闭的，iff T的每一个分支终止在假节点。 S={P, QR, ~P~Q, ~P~R} P ~P Q ~Q R ~R

39 例 S={P(x), ~P(x)Q(f(x)), ~Q(f(a))} A={P(a), Q(a), P(f(a)), Q(f(a)),…}

40 推理节点 定义(inference node, 推理节点)
如果在一个封闭的语义树中，节点 N 的直接子孙均为假节点，则这个节点N为推理节点. S={P(x), ~P(x)Q(f(x)), ~Q(f(a))} A={P(a), Q(a), P(f(a)), Q(f(a)),…} P(a) Q(f(a)) ~P(a) ~Q(f(a))

41 证明一个定理就是寻找一棵封闭语义树. S不可满足  S在所有解释下为假  S在所有H解释下为假; 完备语义树包含所有H解释，并且每一枝是一个H解释; S在I下为假, 则使某个基础实例为假; 对于假节点, 语义树不用再扩展; 所有枝上都有假节点, 则为封闭语义树;

42 Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作

43 Herbrand定理 定理(Version 1) 子句集S是不可满足的，当且仅当 对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树。

44 证明 （=>）设子句集S不可满足. 要证:对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树。 设T是S的完备语义树.
任选T的一个分支B, I(B)是B上所有连线上的文字的集合的并， I(B)是S的一个解释. S不可满足, 则I(B)一定使S中的一个子句C为假; I(B)一定使C的某个基础实例C’为假(性质3); 因为C’的每个原子一定都在原子集A中，并且 C’的文字数目是有限的, 所以在B上一定存在一个假节点. 因为B的任意性, T的每个分支都有假节点. 因此， T是封闭的.

45 T是有限的. T是有限的封闭语义树. （<=）设对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树. 要证: 子句集S不可满足。 完备语义树包含S的所有解释,每一枝对应一个解释; 封闭语义树: 每一枝都终止在假节点上: 每一枝都使S的某个子句的某个基例为假. 根据性质4，子句集S是不可满足的, iff对每个解释I下，至少有S的某个子句的某个基例为假。 因此，子句集S不可满足。

46 定理(Version 2) 子句集S是不可满足的，当且仅当 存在一个有限不可满足的S的基础实例集合S’。 例子:
S={P(x), ~P(a)~P(b), Q(f(x))} H={a, b, f(a), f(b), f(f(a)), f(f(b))…} A={P(a), P(b), Q(a), Q(b),…} S’={P(a), P(b), ~P(a)~P(b)} P(a) P(b) ~P(a) ~P(b)

47 证明 （=>） 设子句集S是不可满足的; 要证: 存在一个有限不可满足的S的基础实例集合S’.
根据Version 1, 有一棵有限的封闭语义树; 每一枝都终止在假节点上， 每一枝都使S的某个子句的某些基例为假， 构成S’. S’不可满足. 有限的封闭语义树 —> 节点有限 —> 假节点有限； 因此， S’有限.

48 （<=）设存在一个有限不可满足的S的基础实例集合S’。
S的任一个解释I都是一个对所有基础实例的解释;它包含一个对S’的解释I’. 因为S’不可满足, 所以I’使S’为假; I’I, 所以I使S’为假; (I使某个子句的某个基础实例为假) 由于解释I的任意性, 因此，S不可满足.

49 说明： S不相容就是对S的每一个解释均使S为假，事实上，就是存在一个有限封闭的语义树，进一步就是存在一个基础实例集。
如何找到一个封闭的语义树或有限的字句的基础实例集元不是件容易的事。 Herbrand定理仅仅是一个存在型定理。

50 例2. S={~ P(x)  Q(f(x),x) ,~P(g(x)), ~ Q(y,z) }
H={a, f(a), g(a), g(f(a)), f(g(a)), …} A= {……} S1={P(g(a)), Q(f(g(a)), g(a)) , P(g(a)), ~ Q(f(g(a)), g(a)) } S不相容

51 例2. S={P(x), ~P(f(x))} H={a, f(a), f(f(a)), …}
A= {P(a), P(f(a)), P(f(f(a))} S1={P(f(a)), ~P(f(a))} S不相容

52 寻找封闭语义树的步骤： 求H域 求H基A 构造完备的语义树 求假节点 形成封闭的语义树

53 Gilmore的方法(1960) 子句集S是有限的; 基础实例的数目是可数的; 枚举;

54 Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作

55 Davis-Putnam的工作 Gilmore的方法是指数复杂性的; Davis-Putnam: 提高效率(启发式方法); 预备知识：
空子句永假；（注：空子句是指集合中有一个空子句）； 空集合永真；（空集合是指没有元素的集合）； 重言式子句：包含互补对的子句。 四条规则: 注意：下面规则的应用不改变子句集的不相容性。

56 规则一：重言式规则(tautology rule)
S中的重言式子句，不会为S的不可满足提供任何信息，应该删除。 例如：S={P∨~P，Q，R∨P} S的逻辑含义是（P∨~P）∧Q∧(R∨P)= Q∧(R∨P)，从而删去重言式P∨~P，不影响S的真值。 S’={Q，R∨P}

57 规则二：单文字规则(one-literal rule)
如果在S中存在只有一个文字的基础子句L, 消去在S中带有这个文字L的所有子句得到S’, 如果S’为空, 则S是相容的; 否则, 从S’中删去~L, 得到S’’，则 S’’不可满足当且仅当S不可满足. 单文字: 在S中存在只有一个文字的基础子句L. 例子: S={L，L∨P，~L∨Q，S∨~R} S’ = {~L∨Q，S∨~R} S’’= {Q，S∨~R} S不可满足, 则在所有解释下S都为假; L=F; L=T; ~L=F.

58 规则三：纯文字规则(pure-literal rule)
L是S的纯文字. 从S中删除含L的子句得S’，如果S’为空集，那么S是可满足的; 否则, S’不可满足当且仅当S不可满足. 纯文字: 如果文字L出现于S中，而~L不出现于S中，L称为S的纯文字. 例子: S={A∨B, A∨~B, ~B, B} S’= {~B, B}; S不可满足, 在A为真的情况下不可满足; A=1  A∨B=1, A∨~B=1; S’不可满足, 当然S不可满足;

59 规则四 分裂规则(splitting rule) S=(L∨A1)∧... ∧(L∨Am) ∧(~L∨B1)∧... ∧(~L∨Bn)∧R
其中：Ai, Bi, R中不含L和~L（自由）。 令S’ ={A1∧...∧Am∧R}， S’’={B1∧...∧Bn∧R} 则S不可满足 当且仅当 S’和S’’同时是不可满足， 即：S’ ∨ S’’同时是不可满足。

60 例1. S={PQ~R, P~Q, ~P, R, U} 对U使用纯文字: {PQ~R, P~Q, ~P, R}
对~P使用单文字: {Q~R, ~Q, R} 对~Q使用单文字: {~R, R} 对R 使用单文字: {} S不可满足; 注意：如果~ L是单文字基础子句，当~L从这个子句集合中被删去后，则这个子句为空子句。

61 例2. S={PQ, ~Q, ~PQ~R} 对~Q使用单文字: {P, ~P~R} 对P使用单文字: {~R}

62 例3. S={P∨~Q, ~P∨Q, Q∨~R, ~Q∨~R}
用规则4：S1= {~Q, Q∨~R， ~Q∨~R} S2= {Q, Q∨~R， ~Q∨~R} 在S1中，对~Q使用单文字: {~R} 在S2中，对Q使用单文字: {~R} 则得到： S1 ∨ S2 = {~R} 对~R 使用纯文字: {} S可满足;

63 例4. S={P∨Q, P∨~Q, R∨Q, R∨~Q} 用规则3： {Q∨~R， ~Q∨~R} 用规则3： {} S可满足;

64 注意： 这些规则对于命题逻辑是十分有效的，但是，对于一阶为词逻辑则需要寻找基础实例集。
Davis的工作在理论上是十分重要的，它对于后来的归结原理的证明方法齐了重要的作用。

65 练习 写出下式的H域和原子集. S={P(f(x,a))} S={P(x)∨Q(y), R(f(y))}
前提：每个储蓄钱的人都获得利息。 结论：如果没有利息，那么就没有人去储蓄钱。 令：S（x，y）表示x储蓄y M（x） 表示x是钱 I（x） 表示x是利息 E（x，y） 表示x获得y 用逻辑公式表示前提和结论并化为子句形式; 下述子句集是可满足的还是不可满足的(给出过程)? S={P∨Q, P∨~Q, ~P∨Q, ~P∨~Q}