Gödel模态逻辑两种扩展的简单表推演

本文考虑了两种逻辑。第一种，$\mathbf{K}\mathsf{G}_\mathsf{inv}$，是Gödel模态逻辑$\mathbf{K}\mathsf{G}$的扩展，引入了定义为$v({\sim_\mathsf{i}}\phi,w)=1-v(\phi,w)$的对合否定$\sim_\mathsf{i}$。第二种，$\mathbf{K}\mathsf{G}_\mathsf{bl}$，是$\mathbf{K}\mathsf{G}_\mathsf{inv}$引入双格连接词和模态词的扩展。我们探讨了它们在$[0,1]$值Kripke框架上关于标准语义的语义性质，并定义了一个允许显式反模型构造的统一表推演演算。为此，我们使用了具有有限模型性质的替代语义。利用该表推演演算，我们构造了一个判定算法，并证明了$\mathbf{K}\mathsf{G}_\mathsf{inv}$和$\mathbf{K}\mathsf{G}_\mathsf{bl}$中的可满足性和有效性是PSpace完全的。