文献

J-GLOBAL ID：202002231970570358   整理番号：20A1230768

分離論理のための循環証明システムにおける空間因数分解

Spatial Factorization in Cyclic-Proof System for Separation Logic

著者 (4件)： NAKAZAWA Koji (Nagoya University) ,  TATSUTA Makoto (National Institute of Informatics, Sokendai) ,  KIMURA Daisuke (Toho University) ,  YAMAMURA Mitsuru (Nagoya Customs)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 37  号： 1  ページ： 1_125-1_144(J-STAGE)  発行年： 2020年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： 本論文では,一般的な帰納的述語を用いた分離論理における含意検査のための新しい証明システムを提案した。提案したシステムは循環証明システムに基づいており,Unfold-Match-Remove証明戦略を用いている。この戦略の困難さの一つは,非折畳みであるべき述語を見出すことである。この問題を解決するために,因子ルールと呼ぶ新しい推論ルールを導入し,それにより,空間式における帰納的述語を因数分解し,そして,Unfold-Match-Remove戦略において展開される述語を見出した。この証明システムは,帰納的述語を線形のものに制限するとき,完全で決定可能である。また,著者らの証明探索手順のプロトタイプ実装によって,いくつかの実験結果を与えた。このシステムは,カット公式やレンマの発見のような発見的機構の助けを借りずに,いくつかの挑戦的な例を証明できた。(翻訳著者抄録)

シソーラス用語： *プログラム理論 ,  *述語論理 ,  帰納推論 ,  プログラム検証 ,  定理証明 ,  因数分解
準シソーラス用語： 帰納的推論 ,  決定可能性 ,  非折畳み ,  分離論理

分類 (1件)： 論理代数  (JB03000H)

タイトルに関連する用語 (4件)： 分離論理 ,  循環 ,  証明 ,  因数分解