信念修正完全和可操作方法

《信念修正完全和可操作方法》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、1000-9825/2002/13(01)0059-06©2002JournalofSoftware软件学报Vol.13,No.1信念修正的完全和可操作的方法Ã12李未,栾尚敏1(北京航空航天大学计算机科学与工程系,北京100083);2(中国科学院软件研究所,北京100080)E-mail:shangmin_luan@sina.com摘要:给出了命题逻辑上信念修正的两种可操作的完全方法.首先对R-演算的规则进行了修改,使得对任何一个极大协调的子集都通过这组规则得到.然后,给出了求得所有的极小不协调子集的一组规则.最后,

2、给出一个过程,该过程能求得所有的极大协调子集.因为这两种方法都能求得所有的极大协调子集,所以把它们称为完全的.关键词:信念修正;信念集;迭代修正中图法分类号:TP18文献标识码:A[1]在信念修正的研究成果中,比较重要的有真值维护的方法、AGM(Alchourron,Gardenfors和Makinson)的[2][3~5][6~7][1]方法、序列极限的方法和迭代的方法.真值维护方法的思想是,任何一个合理的信念必定有其合理的理由.真值维护的过程就是从对一个信念加入一条理由开始的.若在加入该理由后不会引起矛盾,则直接将该

3、理由插入就可以了;否则,就执行一个回溯的过程,找到引起矛盾的原因,消除矛盾.[2]Alchourron,Gardenfors和Makinson首先给出了信念修正应该满足的公设,然后给出了一些修正方法.若任意选择一个极大协调的子集和要加入的语句得到修正后的信念集,则称为最大一致子集修正;若选择某些极大协调的子集,然后求这些集合的交集,由该交集和要加入的语句得到修正后的信念集,则称为部分交集修正;若由所有的极大协调子集的交集和要加入的语句得到修正后的信念集,则称为全部交集修正.上面两种方法研究的都是进行一次修正的情况,那么对

4、信念集进行多次修正的情况如何呢?人们对这个问题也进行了研究,提出了序列极限的方法和迭代的方法两种方法.文献[3~5]中使用的是序列极限的方法,首先给出R-重构的定义,然后给出求R-重构的转换系统,称为R-演算,同时给出了一个用于产生信念集修正序列的过[6~7]程,并且证明了由该过程所产生的信念集收敛,并讨论了R-演算在Horn子句集上的可实现性.迭代的方法与AGM的方法类似,首先给出迭代修正应满足的公设,然后给出一些满足这些公设的修正方法.需要说明的是,AGM的方法是针对理论闭包的,其实即使对于一个有限集,其理论闭包可能

5、都是无限集,所以很难找到一种可操作的方法来表示信念集.AGM的方法所存在的另一个问题是,没有讨论如何得到所有的极[3~5]大协调子集,也就是说,这些方法都是不可操作的.李未对这些问题给予了研究,首先他用语句集来表示信念集,语句集可以是一个闭包,也可以不是一个闭包,但不保证修正后的信念集是一个闭包.虽然文献[3]也讨论了求R-重构的方法,称为R-演算,但某些极大协调子集不能由R-演算的规则推出.本文给出了信念修正的两种可操作的方法:一种方法是将R-演算的规则进行修改,使得对任意一个极大协调的子集都能用修改后的规则得到,称为

6、基于R-演算的方法;另一种方法是,首先给出一组规则,通过这组规则得到所有的与要插入的语句极小不协调的集合,然后给出一个过程,该过程中的变量是极小不协调集合的集合和原来的语句集,通过该过程得到所有极大协调子集.同时,本文还与上述几种方法进行了比较.本文所讨论的方法的一个重要特点就是其可操作性.Ã收稿日期:1999-03-25;修改日期:2000-08-02基金项目:国家自然科学基金资助项目(60033020;60103020);中国博士后科学基金资助项目作者简介:李未(1943－),男,北京人,教授,中国科学院院士,主要研

7、究领域为并发程序语言,操作语义,类型理论,人工智能中的逻辑基础;栾尚敏(1963－),男,山东莱芜人,博士生,主要研究领域为人机交互技术,算法设计自动化,信念修正,形式化方法.60JournalofSoftware软件学报2002,13(1)1基于R-演算的方法首先用一个例子说明如何用R-演算的规则来求极大协调的子集,通过分析这个例子来讨论如何修改R-演算的规则,使得修改后的规则是完全的,即任意一个极大协调子集都能通过修改后的规则求得.例1:设Γ={A,A⊃B,B⊃C,E⊃F}.假设这时再向Γ中增加公式¬C,则就会导致矛

8、盾,这时就需要求出与¬C协调的Γ的子集.设Γ1={A,A⊃B,E⊃F},显然Γ1是与¬C协调的一个极大协调子集,下面说明如何通过R-演算的规则得到Γ1.根据R-Γ协调性规则和公理分别得到¬C

9、¬B,Γ1⇒¬C

10、Γ1和¬C

11、C,Γ1⇒¬C

12、Γ1.再根据R-⊃规则得到¬C

13、B⊃C,Γ1⇒¬C

14、Γ1.根据极大协调的子集的定