|
2.3 Herbrand 定理
对一个所谓词公式来说，不可满足性的证明是困难的。这是由于个体变量论域D的任意性，以及解释的个数的无限性。如果对一个具体的谓词公式能找到一个比较简单的特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的，这将是十分有益的。所要建立的 Herbrand 域(简称H域)就具有这样的性质。
2.3.1 H域
设G是已给的公式，定义在论域D上，令H0是G中所出现的常量的集合。若G中没有常量出现，就任取常量a∈D，而规定H0={a}。
Hi= Hi-1∪{所有形如f(t1,…,tn)的元素}
其中f(t1,…,tn)是出现于G中的任一函数符号，而t1,…,tn 是Hi-1的元素，i=1,2,…。
规定H∞为G的H域(或说是相应的子句集S的H域)。
不难看出，H域是直接依赖于G的最多只有可数个元素。
 |
例1: |
| S={P(a),～P(x)∨P(f(x))} 依定义有 H0={a} H1={a}∪{f(a)}={a,f(a)} H2={a,f(a)}∪{f(a),f(f(a))}={a,f(a),f(f(a))} … H∞={a,f(a),f(f(a)),…} |
|
|
例2: |
| S={～P(z),P(x)∨～Q(y)} 依定义有 H0={a} a是论域D中一常量。 H1= H0 H2= H1 … H∞={a} |
|
|
例3: |
| S={P(f(x),a,g(y),b)} 依定义有 H0={a,b} H1={a,b,f(a),g(a),f(b),g(b)} H2=(a,b,f(a),g(a),f(b),g(b),f(f(a)), f(g(a)),f(f(b)),f(g(b)),g(f(a)),g(g(a)),g(f(b)),g(g(b))} … H∞=H0∪H1∪H2 … |
,
)的形式，这时若H0={a,b},则H1中除有f(a,a),f(b,a)外，还出现f(a,b),f(b,b)。为了研究子句集S的不可满足性，除引入个体域H外，还需讨论H域上S中各谓词的真值。令集合
A={所有形如P(t1,…,tn)的元素}
称作子句集S(或公式G)的原子集。
其中P(
,…,
)是出现于S中的任一谓词符号，而t1,…,tn是
S的H域的任意元素。就上述例1、例2、例3来说，相应的S的原子集分别是
A={P(a),P(f(a)),P(f(f(a))),…}
A={P(a),Q(a)}
和 A={P(a,a,a,a),P(a,a,a,b)…P(f(a),a,a,a)…}
|
例4: |
| S={P(x)∨Q(x),R(f(y))} 依定义有 H={a,f(a),f(f(a)),…} A={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),P(f(f(a))), Q(f(f(a))),R(f(a))),…} 由于S中谓词个数是有限的，而H是可数集，必然有A也是可数集。 |
下面介绍几个术语。对原子、文字、子句和子句集均已定义，进而将没有变量出现的原子、文字、子句和子句集，分别称作基原子、基文字、基子句和基子句集。它们在讨论子句集S的不可满足性时占有重要位置。
特别当将S中的某子句C中所有变量符号均以S的H域的元素代入时，所得的基子句C′称作C的一个基例。
|
例: |
| S={P(x),Q(f(y))∨R(y)} 有H={a,f(a),f(f(a)),…} 对任一b∈D子句P(b),Q(f(b))∨R(b)都叫基子句。 而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)的基例。 |