The use of lemmas is very promising for improving top-down oriented proof procedures for first-order logic based on model elimination or the connection tableau calculus.
In the past several methods for the generation of lemmas for a given set of clauses have been developed and quite successfully integrated into existing proof systems. But, when trying to generate harder lemmas, the bottom-up lemma generation procedures fall into the well-known problems of saturating theorem proving. They suffer from a rather unintelligent control which neglects the goal to be proven and the costs to handle an ever growing mass of clauses.
Therefore, we propose a lemma generation procedure based on genetic programming which improves on the procedures currently used. We obtain an appropriate control of the generation process by the integration of top-down and bottom-up proof search. Further, the probabilistic techniques allow for the use of constant memory by simultaneously providing the probability that each interesting lemma can eventually be generated.