循環証明体系におけるカット除去定理とカット規則の制限

今年度は、不動点演算子を含む各種の命題論理と、分離論理に対する循環証明体系に関して、以下の成果を得た。1. 証明木の各無限枝が有限種類のシーケントしか含まないような無限証明（このような無限証明を，擬有限性を満たす無限証明，と呼ぶ）は循環証明に変換できることを示した。不動点演算子を含む各種の命題論理（古典命題論理、時相論理、様相論理）の無限証明が常にこの擬有限性を満たすことにより、これらの論理については、常に無限証明から有限証明への変換が可能であることが分かる。とくに、この変換においてはカット規則が導入されることはないことから、無限証明体系と循環証明体系の証明能力が等しいこと、および、循環証明体系のカットなし完全性であることを証明した。2. 有理数権限値をもつ並行分離論理のエンテイルメント（含意命題）判定のために、分離論理の証明体系が利用できることを示し、このエンテイルメント判定が決定可能であることを示した。より詳細には、Brotherstonらによって提案された、メモリアクセスの権限を有利数値で表現した並行分離論理体系に対し、論理式をシンボリック・ヒープに制限した体系を提案した。この体系におけるエンテイルメント判定問題を、権限値なしの分離論理のエンテイルメント判定問題に帰着し、これを循環証明体系における証明探索によって解くアルゴリズムを示すことにより、エンテイルメント判定問題の決定可能性を証明した。

今年度は、不動点演算子を含む各種の命題論理と、分離論理に対する循環証明体系に関して、以下の成果を得た。1. 証明木の各無限枝が有限種類のシーケントしか含まないような無限証明（このような無限証明を，擬有限性を満たす無限証明，と呼ぶ）は循環証明に変換できることを示した。不動点演算子を含む各種の命題論理（古典命題論理、時相論理、様相論理）の無限証明が常にこの擬有限性を満たすことにより、これらの論理については、常に無限証明から有限証明への変換が可能であることが分かる。とくに、この変換においてはカット規則が導入されることはないことから、無限証明体系と循環証明体系の証明能力が等しいこと、および、循環証明体系のカットなし完全性であることを証明した。2. 有理数権限値をもつ並行分離論理のエンテイルメント（含意命題）判定のために、分離論理の証明体系が利用できることを示し、このエンテイルメント判定が決定可能であることを示した。より詳細には、Brotherstonらによって提案された、メモリアクセスの権限を有利数値で表現した並行分離論理体系に対し、論理式をシンボリック・ヒープに制限した体系を提案した。この体系におけるエンテイルメント判定問題を、権限値なしの分離論理のエンテイルメント判定問題に帰着し、これを循環証明体系における証明探索によって解くアルゴリズムを示すことにより、エンテイルメント判定問題の決定可能性を証明した。