User: Guest  Login
Document type:
Technical Report 
Author(s):
Marc Fuchs 
Title:
Similarity-Based Lemma Generation with Lemma-Delaying Tableaux Enumeration 
Abstract:
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...    »
 
Keywords:
Automated Theorem Proving; Model Elimination; Lemma Generation; Similarity Measures 
Year:
1997 
Year / month:
1997-08-01 00:00:00 
Pages:
31