非正规模态逻辑C2的时态扩张

摘要

本文构建了非正规时态逻辑C2t的矢列演算GC2t。运用高野道夫(M.Takana)的语义方法证明了GC2t的子公式性质,进而证明了GC2t的有穷模型性和可判定性。另外,本文还证明了GC2t的插值性质。