Created by W.Langdon from gp-bibliography.bib Revision:1.7182
The method presented works on the principle that commonly occurring patterns within proof corpora may have some significance and could therefore be exploited to provide novel tactics. These tactics are discovered using a three step process.
Firstly a suitable corpus is chosen and processed. One example of a suitable corpus is that of the Isabelle theorem prover. A number of possible abstractions are presented for this corpus.
Secondly, machine learning techniques are used to data-mine each corpus and find sequences of commonly occurring proof steps. The specifics of a proof step are defined by the specified abstraction.
The formation of these tactics is completed using evolutionary techniques to combine these patterns into compound tactics.
These new tactics are applied using a naive prover as well as undergoing manual evaluation. The tactics show favourable results across a selection of tests, justifying the claim that this project provides a novel method of automatically producing tactics which are both viable and useful.",
Genetic Programming entries for Hazel Duncan