维护的证明论系统

A PROOF THEORY FOR BELIEF REVISION

给定一阶语言及该语言的一个理论，假设需要在理论中添加一个与理论不和谐的语句，并要求保持理论的扩张是和谐的，就必须删除理论内的某些语句．删除理论中尽可能少的语句，即保留理论与需要添加语句和谐的一个极大子集，是构造理论扩张的一种方法．本文构造出了针对上述理论扩张的证明论．该证明论的可靠性及完全性刻划了一般形式的理论扩张与典型的理论扩张间的联系．对于命题逻辑，本文还给出了判定理论扩张的一种方法．

A deduction system, called RE--proof system, is constructed for generatingthe revisions of first order belief sets. When a belief set is rejected by a given fact, allmaximal subsets of the belief set consistent with the fact can be deduced from the proofsystem. The soundness and completeness of the RE--proof system are proved, which imply that there exist a resolution method to decide whether a revision retains a maximal subset of a belief set.