| 大会名称 |
|---|
| 2009年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2009 |
| 発行日 |
| 2009/8/20 |
| セッション番号 |
| 7A |
| セッション名 |
| プログラミング |
| 講演日 |
| 2009/09/04 |
| 講演場所(会議室等) |
| A会場（9号館1F 911教室） |
| 講演番号 |
| A-032 |
| タイトル |
| 多重Knuth-Bendix完備化における危険対除去手法の導入 |
| 著者名 |
| 道又 淳一, 青戸 等人, 外山 芳人, |
| キーワード |
| 項書き換え系, Knuth-Bendix完備化, 多重Knuth-Bendix完備化, 危険対除去 |
| 抄録 |
| 項書換えシステムは等式論理に基づく計算モデルである。項書換えシステムに基づくKnuth-Bendix完備化（以下,KB完備化）は重要な自動定理証明手法として知られる。近年、多重KB完備化、停止性判定器に基づくKB完備化、それら両方の特徴を組み入れた停止性判定器に基づく多重KB完備化など、特定の簡約順序に基づかないKB完備化が提案されている。従来のKB完備化においては冗長な危険対を取り除く効率化手法が知られているが、多重KB完備化への導入はまだ試みられていない。本論文は多重KB完備化への危険対除去手法の導入を提案する。危険対除去付き多重KB完備化の形式化、実装および実験結果を報告する。 |
| 本文pdf |
| PDF download (88.1KB) |