| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2008-05-29 13:30 プレスブルガー文付き項書換え系における書換え帰納法について ○坂田 翼・西田直樹・坂部俊樹・酒井正彦・草刈圭一朗（名大）  SS2008-1 KBSE2008-1 |
|
| 抄録 | （和） | 手続き型プログラムを等価な制約付き項書換え系に変換してプログラム等価性を検証する手法の研究において， 潜在帰納法と呼ばれる手法が制約付き項書換え系に対応するように拡張されている． しかし，潜在帰納法と同じく帰納的定理を証明する手法である書換え帰納法は 制約付き項書換え系に対応するように拡張されていない． 本論文では，制約付き項書換え系に対応するように書換え帰納法を拡張し， それに基づいた帰納的定理の定理自動証明法を提案する． また，制約をプレスブルガー文に限定した場合に，潜在帰納法よりも簡潔に証明できる例を紹介する． |
| （英） | 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 / / / / / | |
| 文献情報 | 信学技報, vol. 108, no. 64, SS2008-1, pp. 1-6, 2008年5月. | |
| 資料番号 | SS2008-1 | |
| 発行日 | 2008-05-22 (SS, KBSE) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2008-1 KBSE2008-1 |
|
| 研究会情報 | |
| 研究会 | KBSE SS |
| 開催期間 | 2008-05-29 - 2008-05-30 |
| 開催地（和） | 宮崎市民プラザ 大会議室 |
| 開催地（英） | Miyazaki Citizens' Plaza |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2008-05-KBSE-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | プレスブルガー文付き項書換え系における書換え帰納法について |
| サブタイトル（和） | |
| タイトル（英） | On Rewriting Induction for Presburger-Constrained Term Rewriting Systems |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 制約付き項書換え系 / constrained TRS |
| キーワード(2)（和/英） | 帰納的定理 / rewriting induction |
| キーワード(3)（和/英） | プログラム検証 / program verification |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 坂田 翼 / Tsubasa Sakata / サカタ ツバサ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2008-05-29 13:30:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2008-1, KBSE2008-1 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | no.64(SS), no.65(KBSE) |
| ページ範囲 | pp.1-6 |
| ページ数 | 6 |
| 発行日 | 2008-05-22 (SS, KBSE) |
[研究会発表申込システムのトップページに戻る]