• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2020 年度 実績報告書

循環証明体系の証明論的分析

研究課題

研究課題/領域番号 18K11161
研究機関名古屋大学

研究代表者

中澤 巧爾  名古屋大学, 情報学研究科, 准教授 (80362581)

研究分担者 木村 大輔  東邦大学, 理学部, 講師 (90455197)
研究期間 (年度) 2018-04-01 – 2021-03-31
キーワードシーケント計算 / カット除去 / 分離論理 / 帰納的述語
研究実績の概要

前年度までに続き,様々な論理体系に対する循環証明体系に関する基本的性質,とくにカット除去可能性に関して調査を行ない、以下の成果が得られた.
1. 前年度の研究において,プログラム検証のための表明論理である分離論理に対する循環証明体系のカット除去可能性に関して,弱い形のカット除去可能性も成立しないことを証明したが,この成果を国際会議FLOPS 2020において発表した.
2. 分離論理のベースとなる論理であるbunched logicについて,その循環証明体系でもカット除去可能性が成立しないことを証明した.bunched logicは分離論理と同様,分離連言(乗法的連言)をもつ体系であるが,同時に直観主義的連言を含むため,その循環証明体系は,構造規則と呼ばれる推論規則を含む.これらの構造規則により,カット除去可能性の反例の証明は,分離論理に対して与えられていたものをそのまま適用することができない.本研究では,証明中の循環を展開することにより,循環のない証明を構成できることを用い,反例となるシーケントの循環証明がカットなしで証明できないことを示した.さらに,この反例は述語として引数を含まないもの(帰納的命題)のみを含むため,述語のアリティの制限してもカット除去可能性は成立しないことの証明にもなっている.
3. 2で与えたbunched logicに対する証明が,分離論理にも適用できることを示した.これにより,分離論理の循環証明体系についても,述語のアリティを制限してもカット除去可能性が成立しないことを示した.

  • 研究成果

    (1件)

すべて 2020

すべて 雑誌論文 (1件) (うち査読あり 1件)

  • [雑誌論文] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020

    • 著者名/発表者名
      Saotome Kenji、Nakazawa Koji、Kimura Daisuke
    • 雑誌名

      FLOPS 2020, Lecture Notes in Computer Science

      巻: 12073 ページ: 88~105

    • DOI

      10.1007/978-3-030-59025-3_6

    • 査読あり

URL: 

公開日: 2021-12-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi