The Use of Data-Mining for the Automatic Formation of Tactics

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

  author =       "Hazel Duncan",
  title =        "The Use of Data-Mining for the Automatic Formation of
  school =       "School of Informatics, University of Edinburgh",
  year =         "2007",
  address =      "UK",
  keywords =     "genetic algorithms, genetic programming",
  URL =          "",
  URL =          "",
  size =         "151 pages",
  abstract =     "As functions which further the state of a proof in
                 automated theorem proving, tactics are an important
                 development in automated deduction. This thesis
                 describes a method to tackle the problem of tactic
                 formation. Tactics must currently be developed by hand,
                 which can be a complicated and time-consuming process.
                 A method is presented for the automatic production of
                 useful tactics.

                 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