Alison Pease

home research papers phd  hrl

Lakatos-style Reasoning

                   Photo by Hannah Gleg

Project Description

In his book Proofs and Refutations, Lakatos identifies seven methods by which mathematical discovery and justification can occur. These methods suggest ways in which concept definitions, conjectures and proofs gradually evolve via interaction between mathematicians. Different mathematicians may have different interpretations of a conjecture, examples or counterexamples of it, and beliefs regarding its value or theoremhood. Through discussion, concepts are refined and conjectures and proofs modified. For instance, when a counterexample is found, one might look for general properties which make it fail a conjecture, and then modify the conjecture by excluding that type of counterexample (piecemeal exclusion). Alternatively, one might generalise from the positives and then limit the conjecture to examples of that type (strategic withdrawal). Another reaction might be to deny that the object is a counterexample on the grounds that the conjecture refers to objects of a different type (monster barring). Given a faulty proof, a counterexample may be used to highlight areas of weakness in the proof, and to either modify the proof or the conjecture which it purports to prove (lemma incorporation).

Our main aim was to provide a computational reading of Lakatos's theory, by interpreting it as a series of algorithms and implementing these algorithms as a computer program. We hypothesised that this is (a) possible, and (b) useful. In order to test our hypotheses we developed a system within which we implemented his methods: HRL. This is a multi-agent automated theory formation programme in which each agent has a copy of Colton's theory formation system HR, which can form concepts and make conjectures which empirically hold for the objects of interest supplied. The conjectures are communicated to the other agents, who send counterexamples if they have them. Agents then use Lakatos's methods to suggest modifications to conjectures, concept definitions and proofs.


The following people were involved with the project:

Alan Smaill -- supervisor (A.Smaill _AT_
John Lee -- co-supervisor (J.Lee _AT_
Simon Colton -- co-supervisor (sgc _AT_
Alison Pease -- PhD student (A.Pease _AT_


This work was supported by EPSRC grant GR/M45030

We completed the project in June 2007. For further details, see my PhD thesis.