| 講演名 | 1999/3/5 2 リテラル節補題の利用による定理証明の高速化 岸野 謙一, 岩沼 宏治, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | トップダウン型の定理証明法が本質的に備えている同一解の再計算という問題を解決するため、中間の計算結果を補題化し、生成された補題を参照することでこれらの冗長な再計算を回避する手法が提案され、実際に利用されている。補題をトップダウン型の定理証明器に組み込む場合、実装の容易さから単位節補題がしばしば利用されるが、単位節補題で簡約できる冗長な再計算には限界があり、さらなる探索空間の縮小のためには非単位節補題の導入が必要となる。本研究では限定された形の非単位節補題として、2 リテラル節補題を実装するとともに、複数の 2 リテラル節補題の利用法を提案し、実験によってもっとも効果的な利用法を考察する。 |
| 抄録(英) | In this paper,we discuss 2-literal lemmaizing on automated theorem proving based on Model Elimination. Lemma is used to avoid recomptations of goals, which is a problem top-down theorem proving basically held. When embedding lemmaizing into theorem provers, unit-lemma is often employed because of it's facility to implement. But,ability to eliminate recomptation of goals which unit-lemma has is limited, and non-unit lemma is needed to eliminate more recomptations of goals. So, we implemented 2-literal lemmaizing into PTTP-based theorem prover which is a limited style of non-unit lemma. We also suggest four kind of methods to use 2-literal lemma and compare them by examinations. |
| キーワード(和) | 2 リテラル節補題 / 非単位節補題 / 定理証明 / 自動演鐸 / model elimination |
| キーワード(英) | 2-literal lemma / non-unit lemma / theorem provign / automated deduction / model elimination |
| 資料番号 | AI98-90 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 1999/3/5(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 2 リテラル節補題の利用による定理証明の高速化 |
| サブタイトル（和） | |
| タイトル（英） | Speed Up Automated Theroem Proving by Using 2-Literal Lemma |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 2 リテラル節補題 / 2-literal lemma |
| キーワード(2)（和/英） | 非単位節補題 / non-unit lemma |
| キーワード(3)（和/英） | 定理証明 / theorem provign |
| キーワード(4)（和/英） | 自動演鐸 / automated deduction |
| キーワード(5)（和/英） | model elimination / model elimination |
| 第 1 著者 氏名（和/英） | 岸野 謙一 / Kenichi Kishino |
| 第 1 著者 所属（和/英） | 山梨大学工学部コンピュータメディア工学科 Dept. of Computer Science and Media Engineering, Yamanashi University |
| 第 2 著者 氏名（和/英） | 岩沼 宏治 / Koji Iwanuma |
| 第 2 著者 所属（和/英） | 山梨大学工学部コンピュータメディア工学科 Dept. of Computer Science and Media Engineering, Yamanashi University |
| 発表年月日 | 1999/3/5 |
| 資料番号 | AI98-90 |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 635 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |