A cognitive model of axiom formulation and reformulation with application to AI and software engineering
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
Mathematical and scientific theories rest on foundations which areassumed in order to create a paradigm within which to work. Thesefoundations sometimes shift. We want to investigate where foundationscome from, how they change, and how AI researchers can use these ideasto create more flexible systems. For instance, Euclid formulatedgeometric axioms which were thought to describe the physicalworld. These were the foundations on which concepts, theorems andproofs in Euclidean geometry rested. Euclidean geometry was latermodified by rejecting the parallel postulate, and non-Euclideangeometries were formed, along with new sets of concepts andtheorems. Another example of axiomatic change is in Hilbert'sformalisation of geometry: initially his axioms contained hiddenassumptions which were soon discovered and made explicit. Paradoxesfound in Frege's axiomatisation of number theory led to Zermelo andFraenkel modifying some of his axioms in order to prevent problem setsfrom being constructed. On a less celebrated, but equally remarkable,level children are able to formulate mathematical rules about theirenvironment such as transitivity or the commutativity of arithmetic,and to modify these rules if necessary. Recent work in cognitivescience by Lakoff and Nunez and in the philosophy of mathematics byLakatos suggests ways in which this may be done. We intend toconstruct and evaluate a computational theory and model of thisprocess and to explore the application of our model to AI and softwareengineering. This is an ambitious project, with the potential tobring together and deeply influence diverse fields including cognitivescience, automated mathematical reasoning, situated embodied agents,and AI problem solving and software engineering domains which wouldbenefit from a more flexible approach. Developing a set of automatedtechniques which are able to take a problem and change it into adifferent, more interesting problem could have great impact on thesedomains. In particular, we aim to explore the application of ourtheory and model to AI problem reformulation and softwarespecifications requirements. A general theory of how constraints,specifications or goals can be formulated and reformulated could leadto a communal set of powerful new AI techniques.
Organisations
People |
ORCID iD |
Simon Colton (Principal Investigator) |
Publications
Browne C
(2014)
Handbook of Digital Games
Charnley. J
(2008)
Applications of a Global Workspace Framework to Mathematical Discovery
Colton. S
(2011)
Computational Creativity Theory: The FACE and IDEA models
Colton. S
(2008)
;Automated Parameterisation of Finite Algebras
Colton. S
(2009)
Seven Catchy Phrases for Computational Creativity Research
Colton.S
(2008)
Joined-Up Reasoning for Automated Scientific Discovery
Pease A
(2008)
Bridging the Gap Between Argumentation Theory and the Philosophy of Mathematics
in Foundations of Science
Pease A
(2010)
Model-Based Reasoning in Science and Technology
Pease. A
(2009)
Towards a Computational Model of Embodied Mathematical Language
Pease.A
(2009)
Applying Lakatos-style reasoning to AI domains
Ramezani. R
(2010)
Automatic Generation of Dynamic Investigation Problems
Ramezani. R
(2009)
Solving Mutilated Problems
Sorge V
(2007)
Automatic Construction and Verification of Isotopy Invariants
in Journal of Automated Reasoning
Sorge.V
(2008)
Classification Results in Quasigroup and Loop theory via a Combination of Automated Reasoning Tools
in Comment.Math.Univ.Carolin
Torres. P
(2009)
First Order Logic Concept Symmetry for Theory Formation