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.

Issues of representation and reasoning are fundamental to the digital age, and so our research agenda has potential for wide ranging impact, as follows:

Academia: Our research is published in a wide spectrum of venues: journals, conferences and workshops focusing on topics including software engineering, formal methods, automated reasoning, ontologies, logic and computation, software verification, AI, computational creativity, theoretical computer science, knowledge management and healthcare. We take leading roles in the Scottish Theorem Proving and Programming Languages networks, and the Scottish Informatics & Computer Science Alliance, and we collaborate with over a dozen internationally leading research groups.

Public sector: Modelling healthcare processes is commonplace in the medical world. The integrity of such modelling has a significant impact on the quality and economics of healthcare services. Over the last 3 years, working with healthcare professionals and clinicians in the NHS, we have successfully developed formal computer-based HIV integrated care pathways. Also, a major challenge for local/central government is how to effectively deal with the transparency of public data: large volumes of data need to be made available in linked forms, to make the data intelligible and reusable. Our ontology creation, repair and evolution work has significant potential for data transparency.

Business and industry: A key differentiator in commercial products such as automotive and mobile technologies is embedded software. The dependability of such software remains a major challenge, as there are safety risks from software failure, and whoever can crack the challenge will have a substantial commercial advantage. Our group is well placed to help UK companies address this challenge via the tools and techniques we aim to develop to support automated reasoning and representational change. The knowledge, tools/techniques we are exploring will potentially impact on next-generation design and verification technologies.

Safety: Society's reliance on highly automated systems for daily life continues to accelerate. System failures can have a significant impact on the world economy as well as society. We will use the PG funding to help strengthen existing engineering practices with new mathematical representations and associated reasoning processes that will enable engineers to make better-informed design decisions. This will impact positively on the quality of systems design and increase the ability for engineers to predicate potential accident scenarios during at design time.

Security and privacy: Failing to meet the challenges posed by Cyber Security carries significant risks for economic growth and society in general. Cyber-attacks can bring down real-world infrastructure. A major new strand of our work involves applying reasoning techniques to cyber security. Using the PG flexibility fund to build on previous work, we are developing further ideas in this space to bring new fundamental technologies to cyber security.

Environmental: Our ontology evolution work has significant potential for disaster recovery planning. Disparate agencies without shared ontologies need to be able to cooperate and react dynamically when faced with volatile disaster scenarios and incomplete data. Failures in inter-agency communication is mentioned in all post emergency reports. Hence our ongoing ontology evolution research will be of potential benefit to various emergency response services.

Education: We are influencing educational policy by responding to Government papers on educational reform, and we are named in an EC COST proposal to study mathematical practice and pedagogy. Our work on automated reasoning and theory formation, in particular modelling how people perform mathematical reasoning, has potential to deliver new computer-aided teaching assistants for mathematics, thus greatly enhancing the educational process.