摘要
本文将Ｐ．Ｅｎｊａｌｂｅｒｔ和Ｌ．ＦａｒｉｎａｓｄｅｌＣｅｒｒｏ提出的模态归结推理方法推广到命题模态逻辑Ｋ４和Ｄ４系统，建立了Ｋ４逻辑的归结推理ＲＫ４；Ｄ４逻辑的归结推理ＲＤ４，分别证明了ＲＫ４和ＲＤ４关于Ｋ４和Ｄ４的可靠性与完备性．
In this paper, the modal resolution method presented by P. Enjalbert and L.Farinas del Cerro is extended to modal systems K. and D.. Then, the soundness and completeness of RK4 relative to K4 is proved, and also for RD4 relative to D4.
出处
《软件学报》
EI
CSCD
北大核心
1995年第12期742-750,共9页
Journal of Software
基金
国家自然科学基金
863计划
国家攀登计划资助
