信念更新是刻画知识与信念动态演化规律的一种形式理论,是计算机软件与理论研究的重要内容。信念更新的动机和任务就是消除吸收新信息所带来的矛盾,使整个系统保持协调。1985年由Alchourron、Gardenfors和Makinson共同提出AGM模型是信念更新领域的最核心内容,其中的部分交思想是信念更新研究最重要的思想。局部信念更新是当前信念更新领域研究热点,Parikh、Kourousias和Makinson等人对基于分离的信念更新算子进行了研究。本文在他们工作的基础上继续对公式集的最细分离、基于分离的信念更新进行研究,取得了一些突破,可以概括为以下几方面:●Parikh(1999)为描述有限语言的局部信念更新提出了公式集的(最细)分离概念,Kourousias和Makinson(2007)将公式集的(最细)分离概念推广到无限语言,利用平行插值定理非构造性地证明了每个公式集(信念集)有唯一的最细分离。本文通过删除公式集中冗余公式的方法,首次给出了计算公式集最细分离的构造性方法并进行了复杂性分析,成功地将存在性数学证明转换成构造性的方法,使得计算公式集的最细分离成为可能,将有力推进基于分离的信念更新算子的研究与应用。●Parikh(1999)用公理P刻画局部信念更新,本文给出了它成立的充要条件,获得了公理P的特性并扩充到无限语言。Parikh(1999)验证了基本的AGM部分交更新算子一般不满足相关性公设;Kourousias和Makinson(2007)对信念集作正规化(损失部分信念),所获的正规化信念基(一般不封闭)上的部分交更新算子满足相关性公设。为了不在信念更新之前就损失原有信念,本文不进行信念集的正规化,而是从全体部分交信念更新算子构成的集合中找到满足相关性公设且与Kourousias和Makinson(2007)在正规化信念基上更新算子近似的部分交更新算子的集合。但是这个集合并不包含所有满足相关性公设的更新算子。通过减弱语义,还找出了全体满足相关性公设的部分交更新算子组成的集合,从而获得表示定理,该表示定理刻画了满足相关性公设的部分交信念更新算子的特征。进一步讨论了两个特殊的部分交信念更新算子——极大部分交信念更新算子和全交信念更新算子,得到了两个表示定理和一个计算式。这些结果丰富了相关性公设下信念更新的理论。相关性公设下部分交信念更新的一个基础是本质公式和本质原子,所以本质公式和本质原子的进一步研究将促进相关性公设下的信念更新研究。本文解决了Makinson(2005)提出的关于本质原子的公开问题。●对给定的信念集K和新信念x,利用AGM方法,一般都获得许多部分交更新算子。为方便信念更新的应用,自然希望在AGM的部分交更新算子中引入一些限制,使获得的部分交更新算子更契合实际需求。对确定的信念更新算子,获得该更新算子时受到更新过程影响的局部信念(信念集在每个最细分离的限制)的多少是衡量更新算子的重要指标,根据这个指标定义了信念更新算子的极大不可变原子集,证明了任意信念更新算子的极大不可变原子集是存在且唯一的,同时给出了计算给定的信念更新算子的不可变原子集的方法。根据极大不可变原子集定义了信念集上的极大不可变的信念更新算子,证明了极大不可变信念更新算子都满足相关性公设。将极大不可变信念更新算子应用到多Agent系统,证明了任意的极大不可变信念更新算子是Pareto最优的。进一步讨论了整体极大不可变信念更新算子——可信任信念更新算子。●在AGM方法中,信念之间是平等的。但信念之间往往具有偏好。因此,有必要在信念更新中引入优先关系,信念子集的优先关系表明它们之间相对重要性。Makinson(1997)提出的平滑遮挡信念更新虽然进行了遮挡(与信念集的核心子集矛盾的新信念被遮挡),但获得的结果不能保护该核心子集。本文提出的退格信念更新算子就是尽可能保护(多个)重要子集,即越重要的子集越不易受信念更新过程的影响,除非它必须改变。显然,AGM信念更新是退格信念更新的特例。由于信念集的分离将信念集分成等价且相互无共同原子的公式集,自然将这些公式集认为就是上述的重要子集,即对这些公式集赋优先关系,从而获得基于分离的退格信念更新。将基于最细分离的退格信念更新与极大不可变信念更新进行了联系,得到了相互间的一个等价关系。最后讨论了具有优先性的退格信念更新在多Agent上的应用。