论文部分内容阅读
模态逻辑是研究必然、可能及其相关概念的逻辑。模态逻辑是逻辑学最为重要的分支之一，它的理论、思想、技术和方法不仅是逻辑学中占有重要地位，而且在其他领域，如计算机科学、语言学等以及哲学方面有重要应用，成为这些领域相关部分的理论基础。
模态逻辑公式的可满足性问题和证明系统的完备性问题是模态逻辑中的两个经典的问题。可满足性问题研究的是:对于一个给定的模态公式，判定是否存在模型，使得该命题在其中的某个状态是可满足的。对于模态逻辑的可满足性判定问题，比较经典的解决方法是tableau的方法，但是这个方法由于存在分支的选择问题，因此产生了不确定性。
首先，我们提出了一个基于构造模态公式的canonical model来判定可满足性的方法。利用这个方法，对于给定模态公式(φ)，如果(φ)是可满足的，可以得到(φ)的一个canonical model;如果(φ)是不可满足的，还可以得到┑(φ)的证明。另外，我们基于这个方法，还得到了模态逻辑公理系统完备性的一种构造性证明。
其次，我们用coq实现了一个可以判定模态公式(φ)是否是可满足的工具，如果是，那么程序会输出使其可满足的模型。相反的，如果(φ)不是可满足的，则根据完备性定理，我们知道┑(φ)是可证的，所以程序还会同时输出┑(φ)的证明过程。