Show simple item record

dc.contributor.authorDuncan, Hazel
dc.date.accessioned2007-06-20T08:44:44Z
dc.date.available2007-06-20T08:44:44Z
dc.date.issued2007
dc.identifier.urihttp://hdl.handle.net/1842/1768
dc.descriptionCentre for Intelligent Systems and their Applications
dc.descriptiongrant GR/S76328/01en
dc.description.abstractAs 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 evalutation. 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.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.format.extent871654 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoenen
dc.subjectTacticsen
dc.subjectTheorem Provingen
dc.titleThe Use of Data-Mining for the Automatic Formation of Tacticsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record