Sciweavers

Share
GECCO
1999
Springer

Generating Lemmas for Tableau-based Proof Search Using Genetic Programming

9 years 5 months ago
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.
Marc Fuchs, Dirk Fuchs, Matthias Fuchs
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where GECCO
Authors Marc Fuchs, Dirk Fuchs, Matthias Fuchs
Comments (0)
books