论文部分内容阅读
中介逻辑是一个新的逻辑系统，该系统的创立有明显的哲学背景，自创立后得到了很大的发展。在数理逻辑以及计算机科学领域已发展了中介模态逻辑以及ＭＩＬＬ等中介程序计设 语言，但对作为程序计设语言之逻辑基础之一的中介模态逻辑的自动推理理论与实现的研究还很不够。本文系统地讨论中介模态逻辑ＭＳ４的自动定理证明理论，构造了中介模态逻辑ＭＳ４的表推演系统，由于该系统采用“与或树”的表达方法，因而不产生“遗忘问题”；