Lemma matching for a PTTP-based Top-down theorem prover

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].