The Integration and Interaction of Multiple Mathematical Reasoning Processes

Our work in the DReaM group involves a unique blend of the techniques of artificial intelligence and theoretical computer science, enabling us to take a uniquely holistic perspective on automated reasoning and mathematical discovery. The proposed Platform Grant renewal will be used to provide essential infrastructure and to enable exploratory activities that will support a portfolio of projects which focus on the automation of mathematical reasoning processes, including their analysis, development and interaction. We can be broadly classified by our holistic perspective on automated reasoning. Central to this theme is the interplay between representation and reasoning. That is, discovering the right representation can often dramatically simplify the reasoning required in solving a problem, and conversely, meta-level reasoning, and in particular proof-failure analysis, can often provide guidance in evolving the right representations. The renewal of the Platform Grant will enable us to maintain and strengthen the momentum that has been built up around this theme - in terms of basic research as well as applications. The former covers a spectrum of topics, including: cognitive aspects of theory formation; mathematical discovery and automatic theorem generation; ontology creation, repair and evolution; proof procedures; computability; proof planning; AI problem reformulation; quantum computation; computational creativity; and the visualisation of reasoning processes. The latter covers wide ranging applications such as: software verification; formal modelling of software intensive systems; security and privacy analysis and design; graphic design; videogame design; disaster recovery planning; and the modelling of healthcare processes; poetry and art. The positive effective of our current Platform Grant funding can be seen across all aspects of our research - it enables us to: collaborate and exchange ideas with the best researchers in the world; explore and test new ideas; develop adventurous grant proposals and win funding; consolidate the results of our research projects and secure the follow-on funding that enables the impact of our research to be fully realised; and help develop the next generation of research stars and leaders in our field. A renewed Platform Grant would enable us to continue to grow as a research group, in terms of the career development of our researchers, the depth and breadth of our research, and the impact it has on wider aspects of society.