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.
 
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 Public
Country United States
Start 04/2017 
End 04/2020
 
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 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
 
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 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/
 
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/