Benutzer: Gast  Login
Titel:

Similarity-Based Lemma Generation with Lemma-Delaying Tableaux Enumeration

Dokumenttyp:
Technical Report
Autor(en):
Marc Fuchs
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...     »
Stichworte:
Automated Theorem Proving; Model Elimination; Lemma Generation; Similarity Measures
Jahr:
1997
Jahr / Monat:
1997-08-01 00:00:00
Seiten/Umfang:
31
 BibTeX