The Integration and Interaction of Multiple Mathematical Reasoning Processes.

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics

Abstract

The proposed platform grant will be used to provide essential infrastructure and exploratory activities that will support a portfolio of projects within the overall aims described below.The research aims of the Mathematical Reasoning Group are the automation of mathematical reasoning processes, including their analysis, development and interaction. These processes willinclude: concept formation; theory formation; conjecture making; proof and counterexample finding; the learning of new proof methods and critics; the presentation of proofs and proof search; and the refinement, revision and maintenance of conjectures, representations and theories. A major focus will continue to be on mechanisms for guiding proof search, especially the further development of proof planning, and it will include both formal and `informal' reasoning, for instance diagrammatic reasoning, schematic proof and the use of analogy, abstraction, reflection, symmetry and multi-agent search control. We expect to find applications of this work in formal methods of system design, system biology, commonsense reasoning, and the provision of computational aids for mathematicians. Our work is a unique blend of the techniques of artificial intelligence and theoretical computer science.

Publications

10 25 50
publication icon
Alan Bundy (Author) (2008) Classification results in quasigroup and loop theory via a combination of automated reasoning tools in Commentationes Mathematicae Universitatis Carolinae

publication icon
Alan Bundy (Author) (2007) Automated Discovery of Inductive Theorems in Studies in Logic, Grammar and Rhetoric

publication icon
Dixon L (2009) Graphical reasoning in compact closed categories for quantum computation in Annals of Mathematics and Artificial Intelligence

publication icon
Dixon L (2010) Open Graphs and Computational Reasoning in Electronic Proceedings in Theoretical Computer Science

publication icon
Dixon L (2009) Plans, Actions and Dialogues Using Linear Logic in Journal of Logic, Language and Information

publication icon
Dixon, L (2009) Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic in Workshop on Verification and Validation of Planning and Scheduling Systems: ICALP 2009

publication icon
Gudmund, G. (2010) The AI4FM approach for proof automation within formal methods in UKCRC Grand Challenges in Computing Research (GCCR'10)

publication icon
Ireland A (2013) Reasoned modelling critics: Turning failed proofs into modelling guidance in Science of Computer Programming

 
Description Synopsis: The aim of the project was the automation of mathematical reasoning processes, including their analysis, development and interaction. These processes included: concept formation; theory formation; conjecture making; proof and counterexample finding; the learning of new proof methods and critics; the presentation of proofs and proof search; and the refinement, revision and maintenance of conjectures, representations and theories. In particular, the Platform provided the opportunity to:
- Develop, document and maintain our research platforms, e.g., IsaPlanner.
- To explore new mechanisms for mathematical reasoning, their integration and interaction.
- To explore diverse applications of mathematical reasoning.
- To use the flexibility it provided significantly to improve the productivity and effectiveness of our research via support for students, etc.

Results: The Platform Grant pump primed a large number of activities within the area of interacting mathematical reasoning processes. It enabled us to explore new directions and establish new projects that were adventurous, but on which we could demonstrate solid initial progress. During the project period, five new research grants can be directly attributed to pump-priming by the Platform Grant. It has also enabled us to maintain and develop the generic software that underpins much of our work, especially IsaPlanner, our proof planning system that guides and repairs proofs by mathematical induction.
Exploitation Route The Platform Grant enabled to pump prime a number of new research projects via our 'flexibility fund', which funded RAs and PhDs for periods of 1-6 months to explore new directions. Many of these projects led to successful research grant applications. Our exceptional funding success rate can be explained in large part to the fact that we were able to combine adventurous proposals with a proof of feasibility arising from these exploratory projects: a rare combination.
Sectors Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Other

URL https://sites.google.com/site/dreamplatformgrant/
 
Description We pump-primed several new research directions in: • Graphical reasoning about quantum mechanics using the Quantomatic system. This was developed in collaboration with Abramsky's quantum information processing group and Oxford and built on our hiproofs graphical language for proof planning. This tool increases productivity and accuracy in quantum reasoning. • Automatic theory exploration. Three different approaches were explored. These have led to tools for automated support for mathematicians and for increasing the automation in formal methods. • Automated synthesis of loop invariants. In software verification this is usually thought to require human intervention, so automation increases productivity and accuracy. • Use of concept generation in the computer games industry. We have collaborated with the following companies: Praxis, QinetiQ, BAE Systems, nCipher, CESG and Lemma One. Our PhD students have been employed by the first three of these companies, which has assisted technology transfer. We also spun out two companies, which have licenced software we have developed: • TheoryMine, which sells naming rights to automatically conjectured and proved novel theorems. • Contemplate, which specialises in static analysis of software in the finance sector.
First Year Of Impact 2015
Sector Digital/Communication/Information Technologies (including Software)
 
Description EPSRC
Amount £23,194 (GBP)
Funding ID EP/H023852/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 05/2010 
End 05/2014
 
Description EPSRC
Amount £1,140,286 (GBP)
Funding ID EP/J001058/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 08/2011 
End 07/2015
 
Description EPSRC
Amount £513,669 (GBP)
Funding ID EP/H024204/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 04/2010 
End 03/2014