The Integration and Interaction of Multiple Mathematical Reasoning Processes

Lead Research Organisation: Heriot-Watt University
Department Name: S of Mathematical and Computer Sciences

Abstract

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.

Planned Impact

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.

Publications

10 25 50
 
Description The DReaM group has an outstanding international track-record in automated reasoning research, both basic and applied. A distinctive feature of our group is the breadth of research we undertake, from computational creativity, i.e. theory formation, evolution and learning, through to proof engineering, i.e. proof structuring, development, navigation and maintenance. Our applications are also wide ranging, and currently include: ontology management, emergency response, healthcare workflows, industrial-scale embedded formal methods, security and privacy, games, A unique feature of our research is the idea that representation is fluid, i.e. by seeking a deep understanding of the subtle interplay between problem representation and reasoning we are able to develop highly robust and flexible automated reasoning tools and techniques. The breadth of our activities means that we benefit from synergies that arise through the cross-fertilization of ideas and challenges across all three sites. Central to the Platform Grant is what we call the Flexibility Fund (FF), which has given us a real strategic advantage - this Platform Grant has funded 38 FF projects, typically ranging from 2-months through to 6-months. To give a flavour of the diversity of activities, the current Platform Grant has assisted Dr Komendantskaya in securing funding in the emerging area of Verifiable and Explainable AI (i.e. within the context of Neural Networks). In contrast, and building upon work started in our previous Platform Grant, Dr Fleuriot has secured continued funding to further develop and deploy WorkflowFM - a graphical modelling tool that supports the automatic verification of workflows. Through this Platform Grant we have funded thirteen summer Interns - this has been highly effective both in terms of research contributions as well as giving students a taster of what it is like to work within a research group. A significant number of our Interns have gone on to study for a PhD. The end of Platform Grant funding ends continuous infrastructure funding for the DReaM group that dates back to 1982 - first Rolling Funding (SRC/EPSRC) then Platform Grant Funding (EPSRC). This unique source of funding has played vital role in training and nurturing young researchers through the decades.
First Year Of Impact 2015
Sector Aerospace, Defence and Marine,Education,Healthcare
Impact Types Societal

 
Description A Query Answering Framework Using Functional Inferences Over Heterogeneous Data.
Amount £336,402 (GBP)
Funding ID HO2017050001B8 (RB0576) 
Organisation Huawei Technologies Research and Development UK Ltd 
Sector Private
Country United Kingdom
Start 02/2018 
End 01/2021
 
Description AISEC: AI Secure and Explainable by Construction
Amount £2,200,000 (GBP)
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 09/2020 
End 08/2023
 
Description Carnegie Trust Research Internship
Amount £1,400 (GBP)
Organisation Carnegie Trust 
Sector Charity/Non Profit
Country United Kingdom
Start 06/2015 
End 08/2015
 
Description Communication and Trust in Emergencies
Amount £383,425 (GBP)
Funding ID N62909-17-1-2237 
Organisation US Navy 
Department US Office of Naval Research Global
Sector Academic/University
Country United States
Start 04/2017 
End 04/2020
 
Description Continuous Verification of Neural Networks
Amount £90,848 (GBP)
Organisation Defence Science & Technology Laboratory (DSTL) 
Sector Public
Country United Kingdom
Start 04/2020 
End 03/2021
 
Description Digitizing Industrial Workflows: Monitoring and Optimization
Amount € 390,422 (EUR)
Funding ID 18243 
Organisation European Institute of Innovation and Technology (EIT) 
Sector Public
Country Hungary
Start 01/2018 
End 12/2018
 
Description Digitizing Industrial Workflows: Monitoring and Optimization
Amount € 471,023 (EUR)
Funding ID 18243-19 
Organisation European Institute of Innovation and Technology (EIT) 
Sector Public
Country Hungary
Start 01/2019 
End 12/2019
 
Description SICSA Distinguished Visiting Fellow: P.Johann
Amount £1,400 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 08/2015 
End 08/2015
 
Description SICSA PEER grant, 2017
Amount £395 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 09/2017 
End 09/2017
 
Description SICSA Workshop funding: Practical Types Summer School
Amount £6,750 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 07/2015 
End 07/2015
 
Description SICSA Workshop funding: Type Inference and Automated proving
Amount £300 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 05/2015 
End 05/2015
 
Description SICSA workshop funding: STP'15
Amount £400 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 10/2015 
End 10/2015
 
Description SecCon-NN: Neural Networks with Security Contracts - towards lightweight, modular security for neural networks
Amount £30,000 (GBP)
Organisation National Cyber Security Centre 
Sector Public
Country United Kingdom
Start 11/2019 
End 03/2020
 
Title COALP: coalgebraic logic programming interpreter 
Description An interpreter for a prover -- COALP -- that combined proof search and coinductive methods. 
Type Of Material Improvements to research infrastructure 
Year Produced 2016 
Provided To Others? Yes  
Impact Collaborations started. 
URL http://www.macs.hw.ac.uk/~ek19/CoALP/
 
Title ML4PG: Machine Learning for Proof General 
Description Software Supporting Interactive proof development in Coq 
Type Of Material Improvements to research infrastructure 
Year Produced 2017 
Provided To Others? Yes  
Impact Impact on researchers in Interactive Theorem Proving Community 
URL https://github.com/ML4PG/ML4PG
 
Title Tinker 
Description The Tinker tool enables graphical development of proof strategies. It is theorem-prover indepedent and has been connected to 3 theorem provers. 
Type Of Material Improvements to research infrastructure 
Provided To Others? No  
Impact We are working with an industrial collaborator in developing and using the tool in an industrial setting. 
URL http://ggrov.github.io/tinker/
 
Title WorkflowFM 
Description WorkflowFM is a workflow modelling and deployment framework. It offers a domain-agnostic approach and technology based on a correct-by-construction approach. It enables the development of high-level process models and workflows that can be faithfully deployed as software through automatic code-generation. The workflows can be integrated with data, e.g. coming from IoT devices, and monitored through our custom-built dashboard. WorkflowFM has been applied to real-world problems in healthcare and manufacturing. 
Type Of Material Improvements to research infrastructure 
Year Produced 2018 
Provided To Others? No  
Impact Some of the technology underlying WorkflowFM is now part of Digiflow, a system for the modelling and deployment of industrial workflows used to track shop floor assets and workforce. Digiflow has been used as part of two real-world pilots and is now further developed to become a commercial solution. 
URL http://www.workflowfm.com/
 
Title New Coalgebraic Logic Programming implementation 
Description New, advanced, implementation of CoALP interpreter, By E.Komendantskaya and M.Schmidt 
Type Of Technology Software 
Year Produced 2017 
Open Source License? Yes  
Impact The tool is applied in abstract compilation in Java, bu collaborators D.Ancona and L.Franceschini, Genova University, Italy 
URL http://www.macs.hw.ac.uk/~ek19/CoALP/
 
Company Name THEORYMINE LIMITED 
Description TheoryMine is a company dedicated to automated theory exploration. New mathematical theories are automatically generated followed by new theorems within each of these theories. Customers are able to name these new theorems. They get a certificate containing the definition of the theory plus a statement of the new theorem and a brief overview of its proof. In addition, they can purchase mugs, mouse mats or tee-shirts with the theorem written on it. People typically buy the naming rights to these theorems as a gift for a friend or family member. The computer system behind TheoryMine is the product of decades of research on the automation of mathematical reasoning at the University of Edinburgh. This consists of the proof planning system IsaPlanner for inductive proofs, which was based on the interactive proof system Isabelle; the theory exploration system IsaCoSy, which identifies and proves interesting theorems in a recursive theory and IsaWannaTheorem, which invents new recursive theories for IsaCoSy. A paper describing this theory can be downloaded by customers (see doi below). 
Year Established 2010 
Impact TheoryMine was the first company in the World to offer such a theorem naming service.
Website https://theorymine.co.uk
 
Description ALCOP Invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Structural Resolution and Universal Productivity. Invited talk at the 4th Workshop Algebra and Coalgebra meet
Proof Theory, Delft, 6-8 May 2015. About 30 people were present.
Year(s) Of Engagement Activity 2015
URL http://www.appliedlogictudelft.nl/alcop-2015/
 
Description BCS Panel 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Invited speaker at the Panel "Turing: Soluble and Insoluble" at the British Logic Colloquium, Edinburgh, September
2016. About 50 participants.
Year(s) Of Engagement Activity 2016
URL https://www.ed.ac.uk/informatics/news-events/stories/2016/british-logic-colloquium-2016
 
Description Dagstuhl talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact I gave an invited talk at Dagstuhl Seminar ``AI meets formal methods". There were ~50 participants, including industrial participants and research students.
Year(s) Of Engagement Activity 2012
URL http://drops.dagstuhl.de/opus/volltexte/2012/3731/pdf/dagrep_v002_i007_p001_s12271.pdf
 
Description FLOC'18 invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Invited talk "Coalgebra and Automated Reasoning" at Coalgebra, Now! - a FLOC 2018 workshop, Oxford, UK, 8 July 2018.
Year(s) Of Engagement Activity 2018
URL https://www.coalg.org/coalgebra-now-floc18/
 
Description IFIP2.8 invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Coinduction in horn Clause Logic. Invited participant at IFIP Working Group 2.8 on Functional Programming,
Edinburgh, 11-16 June 2017.
Year(s) Of Engagement Activity 2017
 
Description Invited talk at ALCOP17. 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Horn Clause logic: the knowns and the unknowns. Invited talk at the 8th international workshop Algebra and
Coalgebra meets Proof Theory (ALCOP), Glasgow, 10-12 April 2017. About 50 people present.
Year(s) Of Engagement Activity 2017
URL https://personal.cis.strath.ac.uk/clemens.kupke/ALCOP2017/
 
Description Invited talk at ARW'18 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Invited talk "Machine learning for mining, understanding and automating computer proofs" at Automated Reasoning
Workshop, Cambridge, UK, 12-13 April 2018. About 50 attendees, including PG students.
Year(s) Of Engagement Activity 2018
 
Description Invited talk at Bath and Swansea 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Structural Automated Proving. Invited talk at School of Computer Science, Universities of Swansea and Bath (by on-line conferencing), 11 December 2014.
About 20 people participated.
Year(s) Of Engagement Activity 2014
 
Description Invited talk at Birmingham and Oxford 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Structural Resolution Meets Curry Howard. Invited talk at Birmingham University, 06 November 2015 and Oxford
University, 23 October 2015.
About 40 people participated.
Year(s) Of Engagement Activity 2015
 
Description Invited talk at Cambridge 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Certified Automated Theorem Proving for Type Inference. Invited talk at University of Cambridge, 20 May 2016,
and University of Edinburgh (DREAM seminar), 10 May 2016.
About 30 participants.
Year(s) Of Engagement Activity 2016
 
Description Invited talk at Dagstuhl and Bath 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Automated Theorem Proving for Type Inference, Constructively . Invited talk at Dagstuhl Seminar 16131 Language
Based Verification Tools for Functional Programs, 28 March - 01 April 2016. Invited talk at University of Bath, 03 May 2016.
About 60 participants across both talks.
Year(s) Of Engagement Activity 2016
URL https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=16131
 
Description Invited talk at Leeds 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Untyped recursion and corecursion in logic programming: computational and semantic perspective. Invited talk,
Logic group in the School of Mathematics, Leeds University, 8 October 2014.
About 20 people participated.
Year(s) Of Engagement Activity 2014
 
Description Invited talk at Leicester 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Invited talk ``Statistical Machine Learning in Interactive Theorem Proving" at Leicester University. about 20 PG and UG students attended.
Year(s) Of Engagement Activity 2013
 
Description Invited talk at MGS 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Certified Automated Theorem Proving for Type Inference. Invited talk at Midlands Graduate School (MGS), Christmas meeting, Leicester, 13 December 2016. About 50 participants.
Year(s) Of Engagement Activity 2016
 
Description Invited talk at Newton Institute 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Invited talk "Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs" at the
Computer-Aided Mathematical Proof workshop, Isaac Newton Institute for Mathematical Sciences, Cambridge,
10-14 July 2017. The event had hundreds of participants.
Year(s) Of Engagement Activity 2017
 
Description Invited talk at Oxford 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Invited talk "Can statistical machine learning advance mechanised proof technology?" at Oxford university. About 10 research students attended.
Year(s) Of Engagement Activity 2013
 
Description Invited talk at Shonan 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Designing a small programming language, coalgebraically. Invited talk at Shonan'13, "Coinduction for Computation Structures and Programming Languages", 5-9 October 2013.
The audience was ~ 50 people including a dozen PG students.
Year(s) Of Engagement Activity 2013
URL http://shonan.nii.ac.jp/shonan/blog/2012/11/17/coinduction-for-computation-structures-and-programmin...
 
Description Invited talk in Rostov 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Certified Theorem Proving for Type Inference Invited talk at the Conference "Programming Languages and Com-
pilers", Rostov, Russia, 3-5 April 2017. About 70 participants
Year(s) Of Engagement Activity 2017
URL http://plc.sfedu.ru/
 
Description Invited talk on ML4PG 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Postgraduate students
Results and Impact Invited talk "ML4PG: Machine Learning for Proof General: interfacing interfaces" given at Universities of Edinburgh and Strathcyde. About 10-20 research students attended the talk.
Year(s) Of Engagement Activity 2012
 
Description Lyon talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Coalgebraic logic programming: corecursion and parallelism for untyped automated proof-search. Invited talk at
Laboratoire de l'Informatique du Parallelisme (LIP), ´ Ecole Normale Sup ´ erior de Lyon, France, 2 July 2014.
About a dozen people participated.
Year(s) Of Engagement Activity 2014
 
Description QMU invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Proof Carrying Plans - two invited talks at Queen Mary University (5 January 2019) and Birmingham University
(28 February 2019).
Year(s) Of Engagement Activity 2018
 
Description Shonan'17 invited talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Coinductive Uniform proofs. Invited talk at the Shonan meeting "Enhanced Coinduction", Shonan, Japan, 13-17
November 2017.
Year(s) Of Engagement Activity 2017
URL http://shonan.nii.ac.jp/shonan/blog/2016/09/07/4410/
 
Description Workshop on Coalgebra, Horn Clause Logic Programming and Types, 28-29 November 2016, Edinburgh, UK. 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact International workshop disseminating the grant findings. Attracted participants from major UK universities, industries (Microsoft, Google); as well as research students.
Year(s) Of Engagement Activity 2017
URL https://ff32.host.cs.st-andrews.ac.uk/coalpty16/