- author = "Hazel Duncan",
- title = "The Use of Data-Mining for the Automatic Formation of Tactics",
- school = "School of Informatics, University of Edinburgh",
- year = "2007",
- address = "UK",
- keywords = "genetic algorithms, genetic programming",
-
URL = "
http://hdl.handle.net/1842/1768",
-
URL = "
https://www.era.lib.ed.ac.uk/bitstream/handle/1842/1768/hazelthesis.pdf",
- 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.",
- notes = "Supervisors: Alan Bundy and Amos Storkey and John Levine",
