|
様相部分構造論理の性質を代数的な手法で調べるため，まず部分構造論理の代数的意味論として剰余束（residuated lattices）を考察し，この代数に様相演算子に対応する演算子を追加した代数系の性質を調べた．本研究課題においては，様相演算子としてガロア結合と呼ばれる演算子を追加した代数系の性質を調べ，最終的に，1984年以来未解決であった直観主義的時相論理の決定可能性の問題を肯定的に解決した．
本年度，ガロア結合という２つの演算子の組ではなく，まず一つの演算子を持つ体系の性質を調べ，monadic剰余束の特徴付け定理を証明した．「Modal Operators on Non-commutative Residuated Lattices」の題目で国際会議で発表，その後一般化した形で学術雑誌に「On residuated lattices with universal quantifiers」を発表した．さらに，1984年以来未解決であった直観主義的時相論理の決定可能性の問題を次のように解決した．まず，直観主義的様相論理が決定可能であること（学術雑誌に発表），次に直観主義的時相論理が直観主義的様相論理のfusionであることを示した（学術雑誌に発表）．決定可能な論理のfusionはまた決定可能であることから，直観主義的時相論理が決定可能であることが証明できた．また，様相論理との関係が深い「強ガロア結合」と呼ばれる演算子が存在するための必要十分条件を求め，強ガロア結合をもつ剰余束の特徴付け定理を得た．これに関する他の結果も含め，国際会議で発表し，さらにこの成果をまとめた形で学術雑誌に発表した（表題「Residuated lattices with Galois connections as monadic operators」）．
|
