# Lakatos-style Reasoning

### Project Description

In his book * Proofs and Refutations*, Lakatos identifies seven
methods which mathematicians use to develop conjectures, concept
definitions and proofs. These methods are ways of both generating and
reacting to a counterexample to a conjecture. 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).
HRL is a multi-agent automated theory formation programme in which
Lakatos's methods have been implemented. Each agent has a copy of
Colton's theory formation system HR, which it uses to form
conjectures and concepts. The conjectures are communicated to the
other agents, who send counterexamples if they have them. Agents then
react to the counterexamples using Lakatos's methods.

### People

The following people are involved with the project:

Alan
Smaill (A.Smaill _AT_ ed.ac.uk)

John
Lee (J.Lee _AT_ ed.ac.uk)

Simon Colton
(sgc _AT_ doc.ic.ac.uk)

Alison
Pease (A.Pease _AT_ sms.ed.ac.uk)

### Selected Publications

S. Colton and A. Pease "The TM System for Repairing Non-Theorems"
To appear in Proceedings of the IJCAR'04 Disproving Workshop [pdf,
ps.gz]

A. Pease, S. Colton, A. Smaill and J. Lee: "A Model of Lakatos's
Philosophy of Mathematics" To appear in Computing and Philosophy
(ECAP), 2004. [pdf,
ps.gz]

A. Pease and S. Colton "Automatic Conjecture Modification"
Proceedings of the Automated Reasoning Workshop, Leeds, 2004. [pdf,
ps.gz]

A. Pease, S. Colton, A. Smaill and J. Lee: "Semantic Negotiation:
Modelling Ambiguity in Dialogue". Proceedings of Edilog 2002, the 6th
Workshop on the Semantics and Pragmatics of Dialogue, Edinburgh, UK,
2002. [pdf,
ps.gz]

A. Pease, D. Winterstein and S. Colton: "Evaluating Machine
Creativity". Proceedings of the ICCBR'01 Workshop on Creative Systems,
Vancouver, Canada, 2001. [pdf,
ps.gz]

### Funding

This work was supported by EPSRC grant GR/M45030