Similarity-Based Lemma Generation with Lemma-Delaying Tableaux Enumeration

The use of bottom-up generated lemmas is an appropriate method for achieving an effective redundancy control mechanism for connection tableau search procedures as well as for reducing proof lengths. An unbounded use of lemmas, however, usually does not lead to improvements of the search process and can even complicate the search. In order to identify lemmas which are actually relevant for the proof task we develop methods for a similarity-based filtering of lemmas. Similarity between a proof goal and a lemma is measured by simulating a costly but complete tableaux enumeration method (the lemma delaying method) which uses all lemmas to prove the goal and estimating based on this simulation which lemmas may be useful. We investigate this method in detail and introduce several similarity measures. Experiments with the prover SETHEO and the lemma generator DELTA underline the effectiveness of the newly developed methods.     «

The use of bottom-up generated lemmas is an appropriate method for achieving an effective redundancy control mechanism for connection tableau search procedures as well as for reducing proof lengths. An unbounded use of lemmas, however, usually does not lead to improvements of the search process and can even complicate the search. In order to identify lemmas which are actually relevant for the proof task we develop methods for a similarity-based filtering of lemmas. Similarity between a proof goa...     »