id: 06448910
dt: j
an: 2015d.00475
au: Pease, Alison
ti: A computational model of Lakatos-style reasoning.
so: Philos. Math. Educ. J. 27, 286 p., electronic only (2013).
py: 2013
pu: Professor Paul Ernest, University of Exeter, Graduate School of Education,
Exeter
la: EN
cc: E20 P20 E50 R40
ut: 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
lemma-incorporation; local counterexamples; global counterexamples;
method of proofs and refutations; testing hypotheses; philosophical
evaluation
ci:
li: http://people.exeter.ac.uk/PErnest/pome27/Pease%20%20A%20Computational%20Model%20of%20Lakatos-style%20Reasoning.pdf
ab: 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 pre-existing 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
ill-specified 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.
rv: