计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2008年
6期
896-909
,共14页
常亮%史忠植%邱莉榕%林芬
常亮%史忠植%邱莉榕%林芬
상량%사충식%구리용%림분
动态描述逻辑%动作理论%可满足性问题%Tableau算法%可判定性
動態描述邏輯%動作理論%可滿足性問題%Tableau算法%可判定性
동태묘술라집%동작이론%가만족성문제%Tableau산법%가판정성
动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.
動態描述邏輯在描述邏輯的基礎上引入瞭動態維,用于描述和推理動態領域的知識,但目前缺少有效的判定算法作為支撐.文中以描述邏輯ALCO的動態擴展為例,構建齣動態描述邏輯D-ALCO.以D-ALCO的構建過程為基礎,將ALCO的Tableau算法、命題動態邏輯的Tableau算法以及對可能模型途徑的處理有機地結閤起來,給齣瞭D-ALCO的Tableau判定算法,證明瞭算法的可終止性、可靠性和完備性.應用該算法,可以在採用開世界假設的情況下對D-ALCO中公式的可滿足性進行判定.對于D-ALCQO、D-ALCQIO等具有更彊描述能力的動態描述邏輯,可以對該算法擴展後得到相應的Tableau判定算法.
동태묘술라집재묘술라집적기출상인입료동태유,용우묘술화추리동태영역적지식,단목전결소유효적판정산법작위지탱.문중이묘술라집ALCO적동태확전위례,구건출동태묘술라집D-ALCO.이D-ALCO적구건과정위기출,장ALCO적Tableau산법、명제동태라집적Tableau산법이급대가능모형도경적처리유궤지결합기래,급출료D-ALCO적Tableau판정산법,증명료산법적가종지성、가고성화완비성.응용해산법,가이재채용개세계가설적정황하대D-ALCO중공식적가만족성진행판정.대우D-ALCQO、D-ALCQIO등구유경강묘술능력적동태묘술라집,가이대해산법확전후득도상응적Tableau판정산법.
