| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2008-07-31 17:30 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序 ○西田直樹・坂田 翼・酒井正彦・草刈圭一朗・坂部俊樹（名大）  SS2008-20 |
|
| 抄録 | （和） | 定理自動証明では手続きが停止せずに暴走してしまうことがある．その暴走 を避けるために，制約付き項書換えに対する定理自動証明の手続きが潜在帰 納法と書換え帰納法それぞれに対して提案された．一方，書換えが停止性を 持つにもかかわらず，計算が進むにつれて項に含まれる書換え可能な項の大 きさが増大していく場合がある．このような書換え系での定理自動証明にお いて，書換え系の停止性を保存するように等式を方向付けして追加すること は，経路順序を用いる手法では困難である．本稿では，引数切り落とし法を 導入しながら，制約付き書換え系の停止性を保存する等式の方向付けに適し た簡約化順序の条件を示す．制約付きTRSの潜在帰納法と書換え帰納法におけ る定理証明での等式の方向付けにおいて，その条件を満たす簡約化順序が有 効であることを示す． |
| （英） | In automated theorem proving, we often face cases where the procedure keeps running. To avoid such cases, the theorem proving methods based on implicit and rewriting inductions have been proposed for constrained rewriting systems. On the other hand, in terminating term rewriting, there are some cases where computation is reducing while the size of reducible terms is increasing. In (automated) theorem proving for rewriting systems with such cases, it is very difficult (or near-impossible) to orient equations by path-based reduction orders in order to add the equations into the rewriting systems, preserving termination of the rewriting systems. In this paper, introducing the argument filtering technique, we show a condition of reduction orders that can be used in orienting equations with preserving termination of constrained systems. We also show that reduction orders satisfying the condition are effective for orientation phases in theorem proving methods based on implicit induction or rewriting induction for constrained term rewriting systems. |
|
| キーワード | （和） | 停止性 / 簡約化対 / 引数切り落とし法 / 潜在帰納法 / 書換え帰納法 / / / |
| （英） | termination / reduction pair / argument filtering / implicit induction / rewriting induction / / / | |
| 文献情報 | 信学技報, vol. 108, no. 173, SS2008-20, pp. 43-48, 2008年7月. | |
| 資料番号 | SS2008-20 | |
| 発行日 | 2008-07-24 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2008-20 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2008-07-31 - 2008-08-01 |
| 開催地（和） | 公立はこだて未来大学 |
| 開催地（英） | Future University-Hakodate |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2008-07-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序 |
| サブタイトル（和） | |
| タイトル（英） | A Reduction Order for Orienting Equations in Theorem Proving of Constrained TRSs |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 停止性 / termination |
| キーワード(2)（和/英） | 簡約化対 / reduction pair |
| キーワード(3)（和/英） | 引数切り落とし法 / argument filtering |
| キーワード(4)（和/英） | 潜在帰納法 / implicit induction |
| キーワード(5)（和/英） | 書換え帰納法 / rewriting induction |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 坂田 翼 / Tsubasa Sakata / サカタ ツバサ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2008-07-31 17:30:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2008-20 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | no.173 |
| ページ範囲 | pp.43-48 |
| ページ数 | 6 |
| 発行日 | 2008-07-24 (SS) |
[研究会発表申込システムのトップページに戻る]