The Integration and Interaction of Multiple Mathematical Reasoning Processes

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


The proposed Platform Grant renewal will be used to provide essential
infrastructure and exploratory activities that will support a portfolio of
projects that focus on the automation of mathematical reasoning processes,
including their analysis, development and interaction. We can be broadly
classified by our "holistic" perspective of automated reasoning. Central to
this theme is the interplay between representation and reasoning. Discovering
the "right" representation can often dramatically simplify the reasoning
required in solving a problem. Conversely, meta-level reasoning, and in
particular proof-failure analysis, can often provide guidance in evolving
the "right" representation.

The renewal of the Platform Grant will enable us to maintain and strengthen the momentum
that has been build up around this theme -- both in terms of basic research as
well as applications: The former covers a spectrum of topics, including:
cognitive aspects of theory formulation and reformulation;
mathematical discovery and automatic theorem generation; ontology creation,
repair and evolution; proof procedures; proof planning; AI problem reformulation;
quantum computation; computational creativity; visualisation of reasoning processes.
The latter covers wide ranging applications such as: software verification; formal
modelling of software intensive systems; graphics design; games design;
disaster recovery planning.

Our work is a unique blend of the techniques of artificial intelligence
and theoretical computer science -- we also believe we are unique in our
holistic perspective of automated reasoning and mathematical discovery.

Planned Impact

Issues of representation and reasoning are fundamental to the digital age
in which we live. Our research agenda therefore has potential wide ranging
impact as highlighted below:

* Academia: Our research results are published across a wide spectrum of
venues, i.e. journals, conferences, workshops that focus on automated software
engineering, formal methods, automated reasoning, ontologies, logic and
computation, software verification, artificial intelligence, computational creativity,
theoretical computer science, knowledge management. This diversity underlines
the fundamental nature of our work. We also take lead roles in the Scottish Theorem
Proving and Scottish Programming Languages networks, as well as the
Scottish Informatics and Computer Science Alliance. We also collaborate
with over ten international leading research groups.

* Public sector: A major challenge for local and central government
is how to effectively deal with the transparency of public data.
That is, large volumes of public data need to be made available in
linked forms, with the intent of making the data intelligible and
reusable. Our ontology creation, repair and evolution work has
significant potential in this area of data transparency.

* Business and industry: A key differentiator in commercial products is
embedded software, e.g. automotives and mobile technologies. The
dependability of such software remains a major challenge.
Whoever can cost effectively crack the dependability challenge
will have a major commercial advantage. Our group is well placed
to help UK companies address this challenge. In particular, the
tools and techniques we aim to develop to support automated reasoning
and representational change.

In terms of the Digital Economy, we have a track-record within the
creative industries, i.e. games design and graphics design.
More broadly, unreliable software will increasingly impact negatively
on the viability of the Digital Economy, e.g. critical infrastructure
and e-commerce. Again the knowledge, tools and techniques that our
group are exploring will potentially impact on the next generation of
design and verification technologies.

* Security: 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.
Combating Cyber Security threats will call for more scientific methods
in designing software intensive systems than is currently the case.
We believe that our research agenda has the potential to influence
such a change: a change that calls for new methods of representing and
and reasoning about systems; a change that calls for engineers with new skill sets.

* Environmental: Our ontology evolution work has significant potential
in the area of disaster recovery planning. Disparate agencies without
the aid of a shared ontology, need to be able to cooperate and
react dynamically when faced with volatile disaster scenarios and
incomplete data. Our ongoing ontology evolution research will be of
potential benefit to various emergency response services (a UK
spending review priority).

* Education: We are influencing educational policy by responding to
Government papers on educational reform. Furthermore, we are named in
a proposal for funding under the European Cooperation in the field
of Scientific and Technical Research (COST) programme, which,
if successful, will work on mathematical practice and pedagogy.
Our work on automated reasoning and theory formation, in
particular that which models theories of how humans perform
mathematical reasoning, has the potential to deliver a new generation
of computer-aided teaching assistants for mathematics, thus greatly
enhancing the educational process.


10 25 50
Description Our 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, poetry and art. Healthcare, emergency response and security are 3 new areas which have grown significantly because of the current Platform Grant. 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 3 sites.

Central to the Platform Grant is what we call the Flexibility Fund (FF) which has given us a real strategic advantage. However, the influence of the Platform Grant on our wider research agenda has been much more subtle and deeper than can be seen in reviews of our activities in isolation. Examples of complementarity that Platform Grant funding has afforded are:

• The flexibility afforded by the FF enabled Dr Grov to secure EPSRC Impact Acceleration Account funding to use PSGraph in work with D-RisQ, an SME with an international track-record in applying formal methods to the verification of safety critical systems. Moreover, this work has also led to cooperation with Strathclyde and Southampton on a new EPSRC proposal.
• The FF has enabled Dr Fleuriot to move into healthcare research, by supporting new research on the application of formal methods to healthcare, and helping to develop a network of collaborators including St Mary's Hospital (London) and the NHS (Lothian and Greater Glasgow & Clyde). This resulted in a workflow modelling tool (with embedded formal methods) which is now being commercialized.
• Early in the current platform grant period, Prof Ireland secured an EPSRC iCASE Award with BAE Systems (Warton) who specialise in Unmanned Aerial Systems. The TF supported a number of visits to BAE by Ireland and Grov, which helped in progressing the work of the iCASE student, Murali, and in developing a longer-term research agenda with BAE. Of particular interest to BAE is the embedding of formal methods in their existing informal processes for early design.
Exploitation Route Tools: PSGraph; WorkflowFM; UC-B; Victor; CHAIn; HR3.
Sectors Aerospace, Defence and Marine,Creative Economy,Digital/Communication/Information Technologies (including Software),Healthcare,Government, Democracy and Justice,Security and Diplomacy

Description The Platform Grant Flex Fund has enabled Dr Fleuriot to move into healthcare research, by supporting new research on the application of formal methods to healthcare, and helping to develop a network of collaborators including St Mary's Hospital (London) and the NHS (Lothian and Greater Glasgow & Clyde). This resulted in: a workflow modelling tool (with embedded formal methods); a multi-disciplinary research proposal submitted to the NHS Chief Scientist Office (Scotland); and a MRC fellowship application for Dr Manataki (FF RA). Dr Fleuriot's team are having an impact both nationally - work on modelling HIV ICPs led to a joint paper and poster at the Health Informatics Scotland Conference in 2014 and is now part of an ongoing effort to develop such ICPs for the NHS - and internationally, with papers at the IEEE Computer-Based Medical Systems Symposium in 2012 and 2014.
First Year Of Impact 2013
Sector Healthcare
Impact Types Societal

Title Tacny 
Description We have a prototype integration of the techniques developed with the Dafny program verifier. This implements the techniques described in the publications. 
Type Of Material Improvements to research infrastructure 
Provided To Others? No  
Impact The tool is still under development, so beyond the research we have conducted no further impact has been made. 
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. 
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. 
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.