机构地区: 广西师范大学数学科学学院
出 处: 《软件学报》 2012年第9期2323-2335,共13页
摘 要: 对应物理论(counterpart theory)是一阶逻辑的一种理论.Lewis利用谓词模态逻辑到对应物理论的翻译来研究谓词模态逻辑的性质,但是Lewis的翻译存在把不可满足的公式翻译为可满足公式的情况.针对这个问题,提出了一种扩展语义的谓词模态逻辑,建立了扩展语义后谓词模态逻辑模型与对应物理论模型的一一对应关系,并在此基础上建立了谓词模态逻辑到对应物理论的语义忠实语义满翻译(faithful and full translation),其可确保将谓词模态逻辑的可满足公式和不可满足公式分别翻译为对应物理论的可满足公式和不可满足公式.由对应物理论是可靠的、完备的一阶逻辑的理论且语义忠实语义满翻译保持可靠性和完备性,进一步证明了扩展语义的谓词模态逻辑也是可靠和完备的. The counterpart theory is a theory of first-order logic. Lewis interprets modal claims by using a translation from quantified modal logic into the counterpart theory. However, Lewis's translation does not preserve the unsatisfiability of formulas. In this paper, an extended semantics for quantified modal logic is introduced, and the corresponding connection between models of the quantified modal logic and models of the counterpart theory is given. Based on the semantics, a faithful and full translation from quantified modal logic to the counterpart theory, which preserves the satisfiability and the unsatisfiability of formulas, is also established. Furthermore, since the counterpart theory is sound and complete, and the soundness and the completeness are preserved by the faithful and full translation, the quantified modal logic is also sound and complete.
领 域: [自动化与计算机技术] [自动化与计算机技术]