| Presentation | 2000/9/18 A Tableau-based Reconstruction of Consequence Finding Procedure SOL Koji Iwanuma, Katsumi Inoue, Ken Satoh, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | consequence finding / theorem proving / refutation finding / linear resolution / tableau |
| Paper # | AI2000-34 |
| Date of Issue |
| Conference Information | |
| Committee | AI |
|---|---|
| Conference Date | 2000/9/18(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Tableau-based Reconstruction of Consequence Finding Procedure SOL |
| Sub Title (in English) | |
| Keyword(1) | consequence finding |
| Keyword(2) | theorem proving |
| Keyword(3) | refutation finding |
| Keyword(4) | linear resolution |
| Keyword(5) | tableau |
| 1st Author's Name | Koji Iwanuma |
| 1st Author's Affiliation | Yamanashi University() |
| 2nd Author's Name | Katsumi Inoue |
| 2nd Author's Affiliation | Kobe University |
| 3rd Author's Name | Ken Satoh |
| 3rd Author's Affiliation | Hokkaido University |
| Date | 2000/9/18 |
| Paper # | AI2000-34 |
| Volume (vol) | vol.100 |
| Number (no) | 321 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |