论文部分内容阅读
该文将广义归结推广到模态逻辑，给出模态广义双标记子句集的概念，提出模态广义双标记归结。可证明，任意命题模态公式集Ｄ不可满足当且仅当存在从它的广义双标记子句集出发，使用模态广义双标记归结推出不可满足常子句的演绎。结合模态逻辑Ｄ系统的化简规则，基于该文提出的广义双标记归结，实现了命题模态逻辑推理系统ＧＲＤ。实例测试结果表明ＧＲＤ是高效的。