| 講演名 | 1996/5/24 PTTP型定理証明におけるゴールの準最適な並び 藤平 光壮, 岩沼 宏治, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 逐次型探索において, 探索の順序は極めて重要である. PTTP型定理証明においては, ゴールの順序が探索の順序を決定する. ゴールの順序により探索空間の大きさが変わってしまう. 本研究では, 証明を開始する前に各リテラルの探索空間コストをある程度予測し, 探索空間が小さくなるようにリテラルの並び換えを行なう. 並び換えの方法をいくつか提案し, 実装, 性能評価実験, 他の証明器との比較実験を行なった. |
| 抄録(英) | In general, the search order is quite important for sequential theorem Provers to find a proof quickly. As for PTTP-based theorem provers, the order of goals to be solved determines the order of search operations, and thus determines the total size of search space. In this paper, we study the semi-optimal orders of goals for a PTTP-based theorem prover throughout experiments. In preprocessing phase, we reorder goals by a criterion using the result of an estimation of cost for finding a proof of every goal. We propose several criteria for ordering goals, and evaluate them with experimental results. We also compares our results with other famous provers OTTER and SETHEO. |
| キーワード(和) | PTTP / DFID / ME 演繹 / 並べ換え |
| キーワード(英) | PTTP / Depth-first iterative-deepening / model elimination / reordering |
| 資料番号 | AI96-3 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 1996/5/24(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | PTTP型定理証明におけるゴールの準最適な並び |
| サブタイトル（和） | |
| タイトル（英） | Semi-optimal orders of goals in PTTP-type theorem prover |
| サブタイトル（和） | |
| キーワード(1)（和/英） | PTTP / PTTP |
| キーワード(2)（和/英） | DFID / Depth-first iterative-deepening |
| キーワード(3)（和/英） | ME 演繹 / model elimination |
| キーワード(4)（和/英） | 並べ換え / reordering |
| 第 1 著者 氏名（和/英） | 藤平 光壮 / Mitsutake FUJIHIRA |
| 第 1 著者 所属（和/英） | 山梨大学工学部電子情報工学科 Department of Electrical Engineering and Computer Science, Faculty of Engineering, Yamanashi University |
| 第 2 著者 氏名（和/英） | 岩沼 宏治 / Kouji IWANUMA |
| 第 2 著者 所属（和/英） | 山梨大学工学部電子情報工学科 Department of Electrical Engineering and Computer Science, Faculty of Engineering, Yamanashi University |
| 発表年月日 | 1996/5/24 |
| 資料番号 | AI96-3 |
| 巻番号（vol） | vol.96 |
| 号番号（no） | 77 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |