Generating Lemmas for Tableau-based Proof Search Using Genetic Programming

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 favorablywithexisting methods, improvingon run timeand on the numberof solvable problems.

• Type: Conference
• Year: 1999
• Where: GECCO
• Authors: Marc Fuchs, Dirk Fuchs, Matthias Fuchs
• Keywords: Connection Tableau Calculus, GECCO 1999, Optimization, Shortcomings Regarding Redundancy, Top-down Goal Decomposition