Generating Lemmas for Tableau-based Proof Search Using Genetic Programming

Created by W.Langdon from gp-bibliography.bib Revision:1.8129

@InProceedings{fuchs:1999:GLTPSUGP,

• author = "Marc Fuchs and Dirk Fuchs and Matthias Fuchs",
• title = "Generating Lemmas for Tableau-based Proof Search Using Genetic Programming",
• booktitle = "Proceedings of the Genetic and Evolutionary Computation Conference",
• year = "1999",
• editor = "Wolfgang Banzhaf and Jason Daida and Agoston E. Eiben and Max H. Garzon and Vasant Honavar and Mark Jakiela and Robert E. Smith",
• volume = "2",
• pages = "1027--1032",
• address = "Orlando, Florida, USA",
• publisher_address = "San Francisco, CA 94104, USA",
• month = "13-17 " # jul,
• publisher = "Morgan Kaufmann",
• keywords = "genetic algorithms, genetic programming, ATP, CTC, TPTP, SETHEO/SAT",
• ISBN = "1-55860-611-4",
• URL = "http://gpbib.cs.ucl.ac.uk/gecco1999/GP-400.pdf",
• URL = "http://gpbib.cs.ucl.ac.uk/gecco1999/GP-400.ps",
• size = "6 pages",
• abstract = "Top-down or analytical provers based on the connection tableau calculus are rather powerful, yet have notable short comings 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 topdown goal decomposition and bottom-up lemma generation. Experimental studies show that our method compares very favourably with existing methods, improving on run time and on the number of solvable problems",
• notes = "GECCO-99 A joint meeting of the eighth international conference on genetic algorithms (ICGA-99) and the fourth annual genetic programming conference (GP-99)",

}

Genetic Programming entries for Marc Fuchs Dirk Fuchs Matthias Fuchs

Citations