| 中介模态逻辑MS4的表推演系统 |
| |
| 引用本文： | 宫宁生,张东摩.中介模态逻辑MS4的表推演系统[J].南京航空航天大学学报,1995,27(5):668-673. |
| |
| 作者姓名： | 宫宁生 张东摩 |
| |
| 作者单位： | 南京航空航天大学计算机科学与工程系 |
| |
| 基金项目： | 国家高技术研究发展计划资助 |
| |
| 摘 要： | 中介逻辑是一个新的逻辑系统，该系统的创立有明显的哲学背景，自创立后得到了很大的发展。在数理逻辑以及计算机科学领域已发展了中介模态逻辑以及ＭＩＬＬ等中介程序计设 语言，但对作为程序计设语言之逻辑基础之一的中介模态逻辑的自动推理理论与实现的研究还很不够。本文系统地讨论中介模态逻辑ＭＳ４的自动定理证明理论，构造了中介模态逻辑ＭＳ４的表推演系统，由于该系统采用“与或树”的表达方法，因而不产生“遗忘问题”；
|
| 关 键 词： | 数理逻辑 模态逻辑 人工智能 表推演 定理证明器 |
Tableau-Based Proving System for Medium Modal Logic MS_4 |
| |
| Gong Ningsheng, Zhang Dongmo, Zhu Wujia.Tableau-Based Proving System for Medium Modal Logic MS_4[J].Journal of Nanjing University of Aeronautics & Astronautics,1995,27(5):668-673. |
| |
| Authors: | Gong Ningsheng Zhang Dongmo Zhu Wujia |
| |
| Abstract: | |
| |
| Keywords: | mathematical logic modal logics artificial intelligence tableau theorem prover |
| 本文献已被 CNKI 维普 等数据库收录！ |
