| Presentation | 1998/11/30 Speed Up Automated Theroem Prover by Using Lemma Generalization Kenichi Kishino, Koji Iwanuma, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, we discuss lemma generalization on automated theorem proving based on Model Elimination. Lemma is used to avoid recomptation of same goal which is a problem top-down theorem proving basically held. On lemma matching stage, more general lemma-there is more variables in its arguments-is more useful, becouse chance to match these lemmas is more bigger. So we try to generalize lemmas when they are stored in order to increase the chance to match with them and to eliminate the search space. We implemented lemma generalization on PTTP-based theorem prover and evaluate its performance. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | lemma generalization / theorem provign / automated deduction / model elimination |
| Paper # | AI98-41 |
| Date of Issue |
| Conference Information | |
| Committee | AI |
|---|---|
| Conference Date | 1998/11/30(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 | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Speed Up Automated Theroem Prover by Using Lemma Generalization |
| Sub Title (in English) | |
| Keyword(1) | lemma generalization |
| Keyword(2) | theorem provign |
| Keyword(3) | automated deduction |
| Keyword(4) | model elimination |
| 1st Author's Name | Kenichi Kishino |
| 1st Author's Affiliation | Dept.of Computer Science and Media Engineering, Yamanashi University() |
| 2nd Author's Name | Koji Iwanuma |
| 2nd Author's Affiliation | Dept.of Computer Science and Media Engineering, Yamanashi University |
| Date | 1998/11/30 |
| Paper # | AI98-41 |
| Volume (vol) | vol.98 |
| Number (no) | 436 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |