| 講演名 | 2008-05-29 プレスブルガー文付き項書換え系における書換え帰納法について 坂田 翼, 西田 直樹, 坂部 俊樹, 酒井 正彦, 草刈 圭一朗, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 手続き型プログラムを等価な制約付き項書換え系に変換してプログラム等価性を検証する手法の研究において,潜在帰納法と呼ばれる手法が制約付き項書換え系に対応するように拡張されている.しかし,潜在帰納法と同じく帰納的定理を証明する手法である書換え帰納法は制約付き項書換え系に対応するように拡張されていない.本論文では,制約付き項書換え系に対応するように書換え帰納法を拡張し,それに基づいた帰納的定理の定理自動証明法を提案する.また,制約をプレスブルガー文に限定した場合に,潜在帰納法よりも簡潔に証明できる例を紹介する. |
| 抄録(英) | A method for verifying equivalence between procedural programs has been proposed, where the implicit induction is extended to deal with constrained term rewriting systems. However, the rewriting induction, which is used for proving inductive theorems, has not been adapted to constrained systems yet. In this paper, we extend the rewriting induction for constrained term rewriting systems, and propose a procedure based on the method for proving constrained inductive theorems. In the case that constraints are Presburger formulas, we show an example of inductive theorems of which the proof by the procedure is simpler than by the method based on implicit induction. |
| キーワード(和) | 制約付き項書換え系 / 帰納的定理 / プログラム検証 |
| キーワード(英) | constrained TRS / rewriting induction / program verification |
| 資料番号 | SS2008-1,KBSE2008-1 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2008/5/22(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | プレスブルガー文付き項書換え系における書換え帰納法について |
| サブタイトル（和） | |
| タイトル（英） | On Rewriting Induction for Presburger-Constrained Term Rewriting Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 制約付き項書換え系 / constrained TRS |
| キーワード(2)（和/英） | 帰納的定理 / rewriting induction |
| キーワード(3)（和/英） | プログラム検証 / program verification |
| 第 1 著者 氏名（和/英） | 坂田 翼 / Tsubasa SAKATA |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya Univercity |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki NISHIDA |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya Univercity |
| 第 3 著者 氏名（和/英） | 坂部 俊樹 / Toshiki SAKABE |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya Univercity |
| 第 4 著者 氏名（和/英） | 酒井 正彦 / Masahiko SAKAI |
| 第 4 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya Univercity |
| 第 5 著者 氏名（和/英） | 草刈 圭一朗 / Keiichirou KUSAKARI |
| 第 5 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya Univercity |
| 発表年月日 | 2008-05-29 |
| 資料番号 | SS2008-1,KBSE2008-1 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | 64 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |