| Presentation | 1996/5/24 Semi-optimal orders of goals in PTTP-type theorem prover Mitsutake FUJIHIRA, Kouji IWANUMA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | PTTP / Depth-first iterative-deepening / model elimination / reordering |
| Paper # | AI96-3 |
| Date of Issue |
| Conference Information | |
| Committee | AI |
|---|---|
| Conference Date | 1996/5/24(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) | Semi-optimal orders of goals in PTTP-type theorem prover |
| Sub Title (in English) | |
| Keyword(1) | PTTP |
| Keyword(2) | Depth-first iterative-deepening |
| Keyword(3) | model elimination |
| Keyword(4) | reordering |
| 1st Author's Name | Mitsutake FUJIHIRA |
| 1st Author's Affiliation | Department of Electrical Engineering and Computer Science, Faculty of Engineering, Yamanashi University() |
| 2nd Author's Name | Kouji IWANUMA |
| 2nd Author's Affiliation | Department of Electrical Engineering and Computer Science, Faculty of Engineering, Yamanashi University |
| Date | 1996/5/24 |
| Paper # | AI96-3 |
| Volume (vol) | vol.96 |
| Number (no) | 77 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |