2020 Fiscal Year Annual Research Report
Proof theoretic analysis of cyclic proof systems
| Project/Area Number |
18K11161
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | シーケント計算 / カット除去 / 分離論理 / 帰納的述語 |
|---|
| Outline of Annual Research Achievements |
前年度までに続き，様々な論理体系に対する循環証明体系に関する基本的性質，とくにカット除去可能性に関して調査を行ない、以下の成果が得られた．
1. 前年度の研究において，プログラム検証のための表明論理である分離論理に対する循環証明体系のカット除去可能性に関して，弱い形のカット除去可能性も成立しないことを証明したが，この成果を国際会議FLOPS 2020において発表した．
2. 分離論理のベースとなる論理であるbunched logicについて，その循環証明体系でもカット除去可能性が成立しないことを証明した．bunched logicは分離論理と同様，分離連言（乗法的連言）をもつ体系であるが，同時に直観主義的連言を含むため，その循環証明体系は，構造規則と呼ばれる推論規則を含む．これらの構造規則により，カット除去可能性の反例の証明は，分離論理に対して与えられていたものをそのまま適用することができない．本研究では，証明中の循環を展開することにより，循環のない証明を構成できることを用い，反例となるシーケントの循環証明がカットなしで証明できないことを示した．さらに，この反例は述語として引数を含まないもの（帰納的命題）のみを含むため，述語のアリティの制限してもカット除去可能性は成立しないことの証明にもなっている．
3. 2で与えたbunched logicに対する証明が，分離論理にも適用できることを示した．これにより，分離論理の循環証明体系についても，述語のアリティを制限してもカット除去可能性が成立しないことを示した．
|
