论文部分内容阅读
信念修正是主体接受一个新的信念并将其加入到已有的信念集合中，且不会引起不协调的一个过程.在哲学、计算机科学，尤其是数据库和人工智能中，都有信念修正的逻辑形式化，对于信念修正的研究，主要有两种思路:一种是去建立信念修正算子所应当满足的一个公设集合，典型的有AGM公设和DP公设;另一种就是去给出一个具体的满足AGM公设的修正算子. 修正演算(R-演算)是由李未院士给出的一种满足AGM公设的一个具体的信念修正算子，给出了针对逻辑连接词与量词的Gentzen-型推导规则.在原始R-演算中，仅考虑了极大协调公式集合的语义修正，使得在修正过程中将不可避免地出现有效信息丢失的现象.因此，希望能够定义新的极小改变，并给出基于这种极小改变的新型R-演算，使得新型R-演算能够在信念修正的过程中，保留原信念集中尽可能多的有效信息，此外，还将一阶逻辑的R-演算收缩到一些可判定的逻辑上，从而可以通过增加左分解规则的方法来去除掉原始R-演算中对于修正集合△必须是原子的要求. 本文的主要贡献有: 建立了描述逻辑ALC中的关于集合包含关系极小改变（(∈)DL-极小改变）的R-演算推导系统，给出了它的可靠性定理和完备性定理的证明，针对增加描述逻辑的数量限制和角色构造子，分别给出了相对应的R-演算推导系统SDLS和SDLR. 提出了伪子概念的定义，并在此基础上，给出了关于伪子概念极小改变（≤DL-极小改变）的定义，以及描述逻辑ALC中的关于伪子概念极小改变的R-演算推导系统.同样的，针对包含角色构造子的ALCR，给出了伪子角色的定义和性质，并基于此给出了相应的R-演算推导系统PDLR. 给出了严格推导极小改变((I-)DL-极小改变)的定义，并说明了它的不可实现性，以及给出了与其性质尽可能接近的(卜)DL≤-极小改变，建立了描述逻辑ALC中的关于推导关系极小改变（(卜)DL≤-极小改变）的R-演算推导系统.针对包含角色构造子的ALCR，给出了R-演算推导系统UDLR.