制約付き項書換え系の書換え帰納法における補題等式の自動生成法

• 中林, 直生

• 西田, 直樹

• 草刈, 圭一朗

• 坂部, 俊樹

• 酒井, 正彦

• Nakabayashi, Naoki

• Nishida, Naoki

• Kusakari, Keiichirou

• Sakabe, Toshiki

• Sakai, Masahiko

Bibliographic Information

Other Title

• セイヤク ツキ コウ カキカエ ケイ ノ カキカエ キノウホウ ニ オケル ホ ダイ トウシキ ノ ジドウ セイセイホウ
• Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems

Abstract

近年，帰納的定理の証明原理の一つである書換え帰納法が制約付き項書換え系に対応するように拡張され，命令型プログラムの等価性検証に応用するための枠組みが提案された．帰納的定理の証明のためには適切な補題等式を与える必要がある場合が多いが，これまで研究が進んでいる項書換え系に対する補題生成の手法は制約付き項書換え系に対してはあまり有効ではない．本論文では，書換え規則から項の関係を定式化し，その関係に基づいて等式をより一般的な等式に変換する枠組みを提案する．さらに，制約付き項書換え系の書換え帰納法による証明手続きにその枠組みを利用した補題等式の生成・追加機能を組み込むことで，補題等式を予め記述せずに定理自動証明を試み，その有効性を検証する．

日本ソフトウェア科学会第26回大会講演論文集 (2009年9月16日(水)～9月18日(金), 島根大学)

Journal

• 日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編

  日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編 26 723-736, 2009-09

  日本ソフトウェア科学会

Details

• CRID: 1050852018417778944
• NII Article ID: 40022028623
• NII Article ID: 120006668020
• NII Book ID: AN10158574
• ISSN: 09135391
• HANDLE: 2237/21168
• NDL BIB ID: 029998310
• Web Site: https://nagoya.repo.nii.ac.jp/records/19062
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I029998310
• Text Lang: ja
• Article Type: conference paper
• Data Source:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN