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.
Organisations
Publications
Alan Bundy (Author)
(2007)
Automated Discovery of Inductive Theorems
in Studies in Logic, Grammar and Rhetoric
Sorge V
(2007)
Automatic Construction and Verification of Isotopy Invariants
in Journal of Automated Reasoning
Lin Y
(2019)
Automating Event-B invariant proofs by rippling and proof patching
in Formal Aspects of Computing
Wilson S
(2010)
Automation for Dependently Typed Functional Programming
in Fundamenta Informaticae
Pease A
(2008)
Bridging the Gap Between Argumentation Theory and the Philosophy of Mathematics
in Foundations of Science
Alan Bundy (Author)
(2008)
Classification results in quasigroup and loop theory via a combination of automated reasoning tools
in Commentationes Mathematicae Universitatis Carolinae
Johansson M
(2010)
Conjecture Synthesis for Inductive Theories
in Journal of Automated Reasoning
Chandran K
(2022)
Docking simulation and ADMET prediction based investigation on the phytochemical constituents of Noni (Morinda citrifolia) fruit as a potential anticancer drug.
in In silico pharmacology
Dixon L
(2009)
Graphical reasoning in compact closed categories for quantum computation
in Annals of Mathematics and Artificial Intelligence
Meikle L
(2012)
Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette
in Electronic Notes in Theoretical Computer Science
| 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 | Public |
| 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 | Public |
| 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 | Public |
| Country | United Kingdom |
| Start | 04/2010 |
| End | 03/2014 |