定义

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
子句集S中的基础子句的项(常元)构成S的
海伯伦域
(Herbrand域,简称H域,Herbrand Universes),构成方法如下:令F是出现在S中的函数符号的集合,除非F包含的所有函数符号均为0阶(这时公式退化为常量的集合),否则,F是集合,其中表示S中的常元,,D是一个个体域:F是函数构成的表达式的集合,是的映射。S的H域是所有项的集合,。由于F的阶可超穷增加,因此,H域是一个可数超穷集。
例题解析

海伯伦域

海伯伦域

海伯伦域
例1
求的H城,是解释的常元,是变元。
海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
例2
求命题的子句集的H域。
海伯伦域

海伯伦域

海伯伦域
(是常元)

海伯伦域

海伯伦域

海伯伦域

海伯伦域
(最外层的中有n个)

海伯伦域

海伯伦域

海伯伦域
即的H域。
海伯伦化

海伯伦域

海伯伦域
Herbrand化(H化)
子句(或文字A,或原子A)的所有变元均被H域的元素替换,这一过程称为H化,H化的结果称为一个H化基例,也称为H化基子句 (或H化基文字,或H化基原子)。
海伯伦域

海伯伦域
例3
,的H化的若干结果是
海伯伦域

海伯伦域

海伯伦域
现在考虑对子句结构进行进一步的细化分析。

海伯伦域

海伯伦域

海伯伦域
子句集中允许有V连接的子句,如。如果细分它为更简单的形式即两个原子和。

海伯伦域
子句集中的原子A的H域解释
是指子句集的每个原子A进行H化基原子。然后指定(映射到)一个真假值,即A的H域解释是,A是子句集中的H化原子。
海伯伦域
显然,原子A的H化是更“小”的命题结构的H化,也是解释的特例。
海伯伦域
子句或原子的H化是以下所述的一阶公式G的解释的特例,即解释域为域H。
海伯伦域
一阶公式G的一个解释
是指对公式G的变元、函数、原子谓词公式进行如下指定(映射):(1)从非空的项变元取值范围D内为每个项变元指定一个元素,即{公式G的项变元}→D;

海伯伦域
(2)为每个m元函数指定一个D的元素,即;
海伯伦域
(3)为每个n元原子谓词公式指定一个真假值,即。第(1)步称为半解释。后面对其他非空域进行变元的赋值也称为相应域的半解释。
相关概念
定义1
不含有任何连接词的谓词公式叫 原子公式,简称 原子
,而原子或原子的否定统称 文字
。定义2子句
就是由一些文字组成的析取式。
海伯伦域
定义3
不包含任何文字的子句称为 空子句
,记为。定义4
由子句构成的集合称为 子句集
。定义5
设谓词公式G的子句集为S,则按下述方法构造的个体变元域H称为公式G或子句集S的 Herbrand域
,简称 H域
。
海伯伦域

海伯伦域
(1)令H是S中所出现的常量的集合。若S中没有常量出现,就任取一个常量,规定。

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
(2)令{S中所有的形如的元素),其中是出现于G中的任一函数符号,而是中的元素。i=0,1,2,…。
定义6
下列集合称为子句集S的 原子集
:
海伯伦域
A={所有形如的元素}
海伯伦域

海伯伦域
其中,是出现在S中的任一谓词符号,而则是S的H域上的任意元素。
定义7
将没有变元出现的原子、文字、子句和子句集分别称作 基原子
、基文字
、基子句
和 基子句集
。定义8
当子句集S中的某个子句C中的所有变元符号均以其H域中的元素替换时,所得到的基子句称作C的一个 基例
。
海伯伦域

海伯伦域

海伯伦域

海伯伦域
定义9
(可满足性、不可满足性)对于一个变元自由的一阶语言公式G,如果至少存在一个D论域上的一个解释,在此解释下G为真,则称G是 可满足
的,即;反之,如果对于任何解释G均为假,则称G是 不可满足
的,即,或。
海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
对于一个变元自由的一阶语言公式集,即,如果至少存在一个D的解释,在此解释下,的每个以D为论域的公式均为真,则称为可满足的;如果D的所有解释都有假公式,则称是不可满足的。
不可满足意义下的一致性
定理1
设有谓词公式G,而其相应的子句集为S,则G是不可满足的充分必要条件是S是不可满足的。要再次强调:公式G与其子句集S并不等值,只是在不可满足意义下等价。

海伯伦域
的子句集

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
当时,若设P的子句集为,的子句集为,则一般情况下,并不等于,而是要比复杂得多。但是,在不可满足的意义下,子句集与是一致的,即不可满足不可满足。
海伯伦理论
H域上的解释
定义10
如果子句集S的原子集为A,则对A中各元素的真假值的一个具体设定都是S的一个 H解释
。
海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
可以证明,在给定域D上的任一个解释,总能在H域上构造一个解释与之对应,使得如果D域上的解释能满足子句集S,则在H域的解释也能满足S(即若,就有)。

海伯伦域

海伯伦域

海伯伦域

海伯伦域

海伯伦域
定理2
设是子句集S在域D上的一个解释,则存在对应于的H域解释,使得若有,就必有。定理3
子句集S不可满足的充要条件是S对H域上的一切解释都为假。证明:
充分性:若S在一般域D上是不可满足的,必然在H域上是不可满足的,从而对H域上的一切解释都为假。
海伯伦域

海伯伦域

海伯伦域
必要性:若S在任一H解释下均为假,必然会使S在D域上的每一个解释为假。否则,如果存在一个解释使S为真,那么依据定理2可知,一定可以在H域找到相对应的一个解释使S为真。这与S在所有H解释下均为假矛盾。
定理4
子句集S不可满足的充要条件是存在一个有限的不可满足的基例集S’。该常理称为Herbrand定理。