本课题受国家自然科学基金和863计划国家攀登计划资助.
本文将P.Enjalbert和L.FarinasdelCerro提出的模态归结推理方法推广到命题模态逻辑K4和D4系统,建立了K4逻辑的归结推理RK4;D4逻辑的归结推理R D4,分别证明了RK4和RD4关于K
In this paper, the modal resolution method presented by P. Enjalbert and L.Farinas del Cerro is extended to modal systems K4 and D4. Then, the soundness and completeness of R K4 relative to K4 is proved, and also for R D4 relative to D4.
孙吉贵,李乔,刘叙华.模态K4、D4系统的归结推理.软件学报,1995,6(12):742-750
京公网安备 11040202500063号