人工智能原理教案02章归结推理方法26Herbrand定理.docVIP

2.6 Herbrand定理　　Herbrand定理是归结原理的理论基础，归结原理的正确性是通过Herbrand定理来证明的。同时归结原理是Herbrand定理的具体实现，利用Herbrand定理对公式的证明是通过归结法来进行的。本简单地描述了Herbrand定理的基本思想和相关预备知识，最后给出Herbrand定理的一般形式。 　　公式G永真：对于G的所有解释，G都为真。　　公式G永假（矛盾）： 没有一个解释使G为真。2.6.1 Herbrand 定理概述　　问题：一阶逻辑公式的永真性（永假性）的判定是否能在有限步内完成？　　1936年图灵(Turing)和邱吉(Church)互相独立地证明了：　　没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步内判定它是永真（或永假）。对于非永真（或永假）的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。2.6.1.1 Herbrand 定理思想　　要证明一个公式是永假的，采用反证法的思想（归结原理），就是要寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，就没有这样的解释存在，并且算法在有限步内停止。 因为量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无限、不可数的，要找到所有的解释是不可能的。Herbrand 定理的基本思想是简化讨论域，建立一个比较简单、特殊的域，使得只要在这个论域上（此域称为H域），原谓词公式仍是不可满足的，即保证不可满足的性质不变。　　H域和D域关系的如下图表示： 图2－1 H域与D域关系示意图 2.6.1.2 H域　　H域的定义：　　设S为给定公式G的子句集，定义在论域D上，　　H0为S中的常量集。如果S中没有常量，H0由任意单个常量构成，如{a}，　　Hi+1= Hi{fm(t1, t2, …tn)}, i=0, 1, …　　其中，fm为S中出现的所有函数符号的集合，t1, t2, …tn为Hi-1的元素，i＝1，2, …　　则规定H∞称为G的H域（或说是相应的子句集S的H域）。 Hi称为S的i水平常量集。不难看出，H域是直接依赖于G的，而且最多只有可数个元素。 　　例题2-4　　设子句集S = { P(x), Q(y,f(z,b)),R(a)}，求H域　　解：　　H0 ＝ {a, b}为子句集中出现的常量　　H1 ＝ {a, b, f(a,b), f(a,a), f(b,a), f(b,b)}　　H2 ＝ { a, b, f(a,b), f(a,a), f(b,a), f(b,b)，　 　　　　f(a,f(a,b)), f(a,f(a,a)), f(a, f(b,a)), f(a, f(b,b)),　　　　 　f(b,f(a,b)), f(b,f(a,a)), f(b, f(b,a)), f(b, f(b,b)),　　　　 　f(f(a,b),f(a,b)), f(f(a,b),f(a,a)), f(f(a,b), f(b,a)), f(f(a,b), f(b,b)),　　　　 　f(f(a,a),f(a,b)), f(f(a,a),f(a,a)), f(f(a,a), f(b,a)), f(f(a,a), f(b,b)),　　　　 　f(f(b,a),f(a,b)), f(f(b,a),f(a,a)), f(f(b,a), f(b,a)), f(f(b,a), f(b,b)),　　　　 　f(f(b,b),f(a,b)), f(f(b,b),f(a,a)), f(f(b,b), f(b,a)), f(f(b,b), f(b,b))}　　………　　H∞ = H1H2∪H3………　　解毕　　注意：一个函数中含有多个变量时，每个变量都要做到全部的组合。原子集A：　　为研究子句集S中的不可满足性，需要讨论H域上S中各谓词的真值。这里原子集A为公式中出现的谓词套上H域的元素组成的集合。 A = {所有形如 P(t1, t2, …tn)的元素}。这里，P(x1,…, xn)为出现于S中的任一谓词符号，而t1, t2, …tn为S的H域中的任意元素。即把H域中的东西填到S的谓词里去。　　上例题的原子集为：　　A = { P(a), Q(a,a), R(a), P(b), Q(b,a), Q(b,b), Q(b,a), R(b), P(f(a,b)), Q(f(a,b), f(a,b)), R(f(a,b), P(f(a,a)), 　　P(f(b,a)), P(f(b,b)),……) 　　一旦原子集内真值确定好（规定好），则S在H上的真值可确定。不可数问题转化成为了可数问题。S中的谓