動的論理の代数的一般化とその複雑さの理論解析

本年度の前半は、前年度の Kleene 寓圏（推移閉包演算付きポジティブ関係計算）の EXPSPACE 決定可能性の結果の動的論理的な拡張を試みた。しかし、その体系が複雑化したため、いま一度問題の単純化に切り替えて研究をおこない、以下の結果を得た。1. 関係計算と３変数一階述語論理の間の表現力の等価性をポジティブな場合に拡張した。とくに推移閉包付きポジティブ関係計算が、３変数単項推移演算閉包付きポジティブ存在論理と表現力が等価であることがわかった。この結果は、申請者博士論文に記載した。2. 1. の対応関係の基づいて上記の結果を拡張して、（変数制限のない）単項推移閉包演算付きポジティブ存在論理の等式理論の EXPSPACE 決定可能性を示した。本結果については、現在投稿準備中である。3. 決定不能性に関して、１文字制限付き関係計算の決定不能性を示した。既存の（ポジティブでない）一般の関係計算の等式理論の決定不能性の結果を強化して、文字を１種類だけに制限した（結合・和・補のみの演算からなる）関係計算についても決定不能であることを示した。この結果の系として、グラフ上の３変数一階述語論理の決定不能性も明らかにした。この結果は、国際会議 ICLA '19 で発表をおこなった。また、上記と並行して、十数年の間未解決問題であった中間論理に関する問題である「古森-鹿島の問題」に対する反例を与え、数理論理学に関するいくつかの国内会議で発表をおこなった。

本年度の前半は、前年度の Kleene 寓圏（推移閉包演算付きポジティブ関係計算）の EXPSPACE 決定可能性の結果の動的論理的な拡張を試みた。しかし、その体系が複雑化したため、いま一度問題の単純化に切り替えて研究をおこない、以下の結果を得た。1. 関係計算と３変数一階述語論理の間の表現力の等価性をポジティブな場合に拡張した。とくに推移閉包付きポジティブ関係計算が、３変数単項推移演算閉包付きポジティブ存在論理と表現力が等価であることがわかった。この結果は、申請者博士論文に記載した。2. 1. の対応関係の基づいて上記の結果を拡張して、（変数制限のない）単項推移閉包演算付きポジティブ存在論理の等式理論の EXPSPACE 決定可能性を示した。本結果については、現在投稿準備中である。3. 決定不能性に関して、１文字制限付き関係計算の決定不能性を示した。既存の（ポジティブでない）一般の関係計算の等式理論の決定不能性の結果を強化して、文字を１種類だけに制限した（結合・和・補のみの演算からなる）関係計算についても決定不能であることを示した。この結果の系として、グラフ上の３変数一階述語論理の決定不能性も明らかにした。この結果は、国際会議 ICLA '19 で発表をおこなった。また、上記と並行して、十数年の間未解決問題であった中間論理に関する問題である「古森-鹿島の問題」に対する反例を与え、数理論理学に関するいくつかの国内会議で発表をおこなった。