计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
1999年
2期
113-119
,共7页
模态逻辑%模态推理%标记模态归结
模態邏輯%模態推理%標記模態歸結
모태라집%모태추리%표기모태귀결
本文将作者提出的高效的命题模态D逻辑的标记模态归结方法推广到了命题模态逻辑K,K4,D4,T,S4系统,建立了上述命题模态逻辑的标记归结形式系统MRK,MRK4,MRD4,MRT,MRS4.并用转换子句模式的方法,借助于标记模态归结对命题模态D逻辑的可靠性结果,证明了标记模态归结系统MRK,MRK4,MRD4,MRT,MRS4分别关于命题模态逻辑K,K4,D4,T,S4的可靠性.进而得到了它们的完备性.
本文將作者提齣的高效的命題模態D邏輯的標記模態歸結方法推廣到瞭命題模態邏輯K,K4,D4,T,S4繫統,建立瞭上述命題模態邏輯的標記歸結形式繫統MRK,MRK4,MRD4,MRT,MRS4.併用轉換子句模式的方法,藉助于標記模態歸結對命題模態D邏輯的可靠性結果,證明瞭標記模態歸結繫統MRK,MRK4,MRD4,MRT,MRS4分彆關于命題模態邏輯K,K4,D4,T,S4的可靠性.進而得到瞭它們的完備性.
본문장작자제출적고효적명제모태D라집적표기모태귀결방법추엄도료명제모태라집K,K4,D4,T,S4계통,건립료상술명제모태라집적표기귀결형식계통MRK,MRK4,MRD4,MRT,MRS4.병용전환자구모식적방법,차조우표기모태귀결대명제모태D라집적가고성결과,증명료표기모태귀결계통MRK,MRK4,MRD4,MRT,MRS4분별관우명제모태라집K,K4,D4,T,S4적가고성.진이득도료타문적완비성.
