MRG home page · Research · Publications · Software · People

University
of Edinburgh

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