Generating lemmas for tableau-based proof search using genetic programming
M. Fuchs, D. Fuchs, Matthias Fuchs · 1999
Top-down or analytical provers based on the connection tableau calculus are rather powerful, yet have notable shortcomings regarding redundancy control. A well-known and successful technique for alleviating these shortcomings is the use of lemmas. We propose to use genetic programming to evolve useful lemmas through an interleaved process of top-down goal decomposition and bottomup lemma generation. Experimental studies show that our method compares very favorably with existing methods, improving on run time and on the number of solvable problems. 1