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)