维护的证明论系统  

A PROOF THEORY FOR BELIEF REVISION

作　　者：张玉平[1] 李未[1] 

机构地区：[1]北京航空航天大学计算机系

出　　处：《软件学报》1995年第9期513-524,共12页Journal of Software

基　　金：863高技术;国家自然科学基金

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

关 键 词：证明论系统 维护 命题逻辑 计算机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]