Name
Abstract | ||
|---|---|---|
In this paper, we study the efficiency and limitation of various forms of lemma matching, which is intended to speed up top-down theorem proving. In general, top-down theorem proving involves a huge amount of redundancy, which are caused by recomputation of identical goals and/or by irrelevant computation to a targeted goal, and so on. Lemma matching has the ability of preventing some of these redundant computations. Lemma matching rules are mandatory in the sense that all other alternative rules can be discarded as soon as the lemma matching is successfully applied. Thus lemma matching rules have stable efficiency for speeding up top-down proof search. Moreover almost all lemma matching rules are in rather simple forms, thus they are quite easy to implement. We have implemented them in a top-down theorem prover based on PTTP [19, 20]. We report good experimental results, and compare them with the results by OTTER [15] and SETHEO [8]. |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1007/3-540-63104-6_16 | CADE |
Keywords | Field | DocType |
pttp-based top-down theorem prover,lemma matching,theorem proving,theorem prover,top down | Model elimination,Discrete mathematics,Valiant–Vazirani theorem,Computer science,Automated theorem proving,Algorithm,Redundancy (engineering),Rule of inference,Lemma (mathematics),Computation,Speedup | Conference |
Volume | ISBN | Citations |
1249 | 3-540-63104-6 | 9 |
PageRank | References | Authors |
0.72 | 16 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Koji Iwanuma | 1 | 138 | 17.65 |