
06448910
j
2015d.00475
Pease, Alison
A computational model of Lakatosstyle reasoning.
Philos. Math. Educ. J. 27, 286 p., electronic only (2013).
2013
Professor Paul Ernest, University of Exeter, Graduate School of Education, Exeter
EN
E20
P20
E50
R40
mathematics and philosophy
thesis
computational philosophy of science
Lakatos's theory
automated theory formation system
HR program for theory generation
automated theorem proving
algorithms
multiagent dialogue system
communication
mathematicians
conjectures
concept definitions
research
method of surrender
monster barring
exception barring
theoretical computer science
computational representation of Cauchy's proof
series of Java methods
method of lemmaincorporation
local counterexamples
global counterexamples
method of proofs and refutations
testing hypotheses
philosophical evaluation
http://people.exeter.ac.uk/PErnest/pome27/Pease%20%20A%20Computational%20Model%20of%20Lakatosstyle%20Reasoning.pdf
Summary: Lakatos outlined a theory of mathematical discovery and justification, which suggests ways in which concepts, 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. We hypothesise that (i) it is possible to computationally represent Lakatos's theory, and (ii) it is useful to do so. In order to test our hypotheses we have developed a computational model of his theory. Our model is a multiagent dialogue system. Each agent has a copy of a preexisting theory formation system, which can form concepts and make conjectures which empirically hold for the objects of interest supplied. Distributing the objects of interest between agents means that they form different theories, which they communicate to each other. Agents then find counterexamples and use methods identified by Lakatos to suggest modifications to conjectures, concept definitions and proofs. Our main aim is 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. This is the first systematic automated realisation of Lakatos's theory. We contribute to the computational philosophy of science by interpreting, clarifying and extending his theory. We also contribute by evaluating his theory, using our model to test hypotheses about it, and evaluating our extended computational theory on the basis of criteria proposed by several theorists. A further contribution is to automated theory formation and automated theorem proving. The process of refining conjectures, proofs and concept definitions requires a flexibility which is inherently useful in fields which handle illspecified problems, such as theory formation. Similarly, the ability to automatically modify an open conjecture into one which can be proved, is a valuable contribution to automated theorem proving.