文献

J-GLOBAL ID：202002275469365983   整理番号：20A1395372

分離論理の巡回証明におけるカット除去の失敗

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

著者 (4件)： KIMURA Daisuke (Toho University) ,  NAKAZAWA Koji (Nagoya University) ,  TERAUCHI Tachio (Waseda University) ,  UNNO Hiroshi (Tsukuba University)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 37  号： 1  ページ： 1_39-1_52(J-STAGE)  発行年： 2020年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 文献レビュー  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： 本論文は,分離論理のための循環証明システムにおけるカット規則の役割を考察した。循環証明システムは,帰納的定義述語を含む特性を証明するための逐次計算スタイル証明システムである。最近,帰納的定義述語による分離論理で記述された特性を証明するために,循環証明を用いることに多くの関心が寄せられている。特に,プログラム検証のために,分離論理のための循環証明システムにおける機械的証明探索手順に基づくいくつかの定理証明器が提案されている。本論文は,カット除去特性が,いくつかの設定において,分離論理のための循環証明システムにおいて失敗することを示した。本論文では,2つのシステムを,1つは,単一先行詞と単一結論を有するシーケントに対してと,もう1つは,単一先行詞と多重結論を有するシーケントに対して,提示した。カット除去失敗を示すために,システムがカット有りで証明できるが,カット無しでは証明できない,具体的でそれなりに単純な反例を示した。この結果は,カットフリー証明の発見を試みるナイーブな証明探索手続きは証明可能な限界を有することになるため,分離論理に対する循環証明の実際的応用にとって,カットルールが重要であることを示唆する。(翻訳著者抄録)

シソーラス用語： *論理 ,  *プログラム検証 ,  定理証明 ,  自動化 ,  定理 ,  帰納推論
準シソーラス用語： カット除去 ,  シーケント計算 ,  帰納的推論 ,  自動定理証明 ,  *分離論理

分類 (2件)： 論理代数  (JB03000H) ,  計算理論  (JB02000A)

タイトルに関連する用語 (5件)： 分離論理 ,  巡回 ,  証明 ,  カット除去 ,  失敗