| 講演名 | 2000/9/18 タブローに基づく論理的帰結発見手続きSOL 岩沼 宏治, 井上 克巳, 佐藤 健, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 論理的帰結式の発見問題は反駁発見問題の一般化問題である。SOL導出法はスキップ規則を導入してモデル消去法を拡張した証明体系であり、論理的帰結式の導出計算法として極めて重要である。本論文ではまず初めにSOL導出法をコネクションタブロー上に再構築し、次にスキップ正規性の条件を導入し、体系の効率化と精密化を図る。更に種々の枝刈り規則を導入して、その完全性を証明する。特にスキップ規則それ自体が有効な枝刈りメカニズムとして働くことを示す。 |
| 抄録(英) | The consequence finding problem is a generalization of the refutation finding problem. The SOL-resolution which is a Model-Elimination-like calculus with Skip operation, is one of the most significant calculi for the consequence finding problem. The concept"completeness"of consequence-finding calculi differs from the one of refutation finding calculi, hence the pruning methods that are complete for refutation finding tasks may not be complete for consequence finding problems. In this paper, we first reformulate SOL-resolution within connection tableaux and properly strengthen a structural condition, called the skip-regularity, which reduces a great amount of the redundancies in the search space. Next we investigate various types of pruning methods, such as order-preserving reduction, lemma matching, merge, unit subsumption, etc, and show the completeness theorems of each pruning method for consequence finding. Finally we show Skip operation itself has a significantly important feature as a new local failure pruning method in consequence finding. |
| キーワード(和) | 論理的帰結式 / 定理証明 / 反駁 / 線形導出 / タブロ |
| キーワード(英) | consequence finding / theorem proving / refutation finding / linear resolution / tableau |
| 資料番号 | AI2000-34 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2000/9/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | タブローに基づく論理的帰結発見手続きSOL |
| サブタイトル（和） | |
| タイトル（英） | A Tableau-based Reconstruction of Consequence Finding Procedure SOL |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 論理的帰結式 / consequence finding |
| キーワード(2)（和/英） | 定理証明 / theorem proving |
| キーワード(3)（和/英） | 反駁 / refutation finding |
| キーワード(4)（和/英） | 線形導出 / linear resolution |
| キーワード(5)（和/英） | タブロ / tableau |
| 第 1 著者 氏名（和/英） | 岩沼 宏治 / Koji Iwanuma |
| 第 1 著者 所属（和/英） | 山梨大学 Yamanashi University |
| 第 2 著者 氏名（和/英） | 井上 克巳 / Katsumi Inoue |
| 第 2 著者 所属（和/英） | 神戸大学 Kobe University |
| 第 3 著者 氏名（和/英） | 佐藤 健 / Ken Satoh |
| 第 3 著者 所属（和/英） | 北海道大学 Hokkaido University |
| 発表年月日 | 2000/9/18 |
| 資料番号 | AI2000-34 |
| 巻番号（vol） | vol.100 |
| 号番号（no） | 321 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |