| 摘要: |
| 本文将Ｐ．Ｅｎｊａｌｂｅｒｔ和Ｌ．ＦａｒｉｎａｓｄｅｌＣｅｒｒｏ提出的模态归结推理方法推广到命题模态逻辑K4和D4系统，建立了K4逻辑的归结推理ＲK4；D4逻辑的归结推理R D4，分别证明了ＲK4和ＲD4关于K
|
| 关键词: 模态逻辑K4和D4系统，模态归结，自动推理 |
| DOI： |
| 分类号: |
| 基金项目:本课题受国家自然科学基金和863计划国家攀登计划资助. |
|
| MODAL RESOLUTION FOR MODAL SYSTEMS K4 AND D4 |
|
Sun Jigui,Li Qiao,Liu Xuhua
|
| Abstract: |
| 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. |
| Key words: Modal systems K4 and D4, Modal resolution, Automated reasoning. |
