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

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 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.