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.
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.
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.
Organisations
- Heriot-Watt University (Lead Research Organisation)
- Altran (United Kingdom) (Project Partner)
- National Aeronautics and Space Administration (Project Partner)
- D-RisQ (United Kingdom) (Project Partner)
- Spanish National Research Council (Project Partner)
- Scottish Government (Project Partner)
- University of Trento (Project Partner)
- NHS GREATER GLASGOW AND CLYDE (Project Partner)
- Aristotle University of Thessaloniki (Project Partner)
- Osnabrück University (Project Partner)
- Intel (United Kingdom) (Project Partner)
- University of Bristol (Project Partner)
- BAE Systems (United Kingdom) (Project Partner)
Publications
A. Ireland
(2018)
The Use of Automated Theory Formation in Support of Hazard Analysis
Alexandru CA
(2017)
A Step Towards the Standardisation of HIV Care Practices
Andriana Gkaniatsou
(2016)
Getting to know your card: Reverse-Engineering the Smart-Card Application Protocol Data Unit
Bella G
(2017)
Language and domain aware lightweight ontology matching
in Journal of Web Semantics
Bella G.
(2015)
A multilingual ontology matcher
in CEUR Workshop Proceedings
Bella G.
(2020)
A major wordnet for a minority language: Scottish gaelic
in LREC 2020 - 12th International Conference on Language Resources and Evaluation, Conference Proceedings
Bella, G.
(2015)
Multilingual Ontology Matching
Bella, G.
(2015)
A multi-lingual Ontology Matcher
| Description | The Platform Grant scheme provided infrastructural funding for internationally leading research groups within the UK. As a consequence, the objectives of a Platform Grant are relatively general compared to more 'standard' EPSRC grants. A key objective of our Platform Grant was to pump-prime new projects and retain key researchers. We achieved this through a mechanism that we called our Flexibility Fund (FF). Our 'Narrative Impact' illustrates the benefits that our Platform Grant FF had on advancing our fundamental research agenda, as well as the broad range of associated applications that it facilitated. |
| Exploitation Route | Outcomes of this research continue to make an impact, as illustrated in our 'Narrative Impact'. |
| Sectors | Aerospace Defence and Marine Creative Economy Digital/Communication/Information Technologies (including Software) Healthcare Security and Diplomacy |
| 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, video games, creative language and visual art. 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. Our Platform Grant FF assisted Dr Komendantskaya in securing funding in the emerging area of Verifiable and Explainable AI (i.e. within the context of Neural Networks): this includes NCSC/VETSS-funded project CONVENER: Continuous Verification of Neural Networks (2020-2021), EPSRC grant AISEC: AI Secure and Explainable by Construction (2020-2025), DSTL-funded project Neural Network Verification: in Search of the Missing Spec (2021-2022); and ultimately this line of research contributed to shaping the recently won CDT on Dependable and Deployable Artificial Intelligence for Robotics, jointly held by Edinburgh university and HWU (2024-2032). The FF also enabled us to develop our security theme. One strand of work investigated as security type systems for JavaScript which enables reasoning about code to ensure freedom from security flaws; this is important for JavaScript which is used pervasively for client and server-side web applications. Another strand investigated reasoning methods for cloud security scenarios, in particular including a case study on side-channel attacks in multi-organisational cloud settings. We showed effective ways to thwart deliberate data leakage, using verification and probabilistic modelling. Research on Cyber Security has seen significant development in recent years to counter the cyber threat, and verification and reasoning techniques have been central in many areas. For example, alongside and as a result of work supported by the Platform Grant, team members worked on projects in the Turing Institute (on theorem prover formalisation of cryptographic protocols) and in the National Cyber Security Centre (reasoning about data anonymisation and release procedures). There has also been a strong interaction with (including funded projects within) the UKRI funded Research Institute in Verified Trustworthy Software Systems (VeTSS). During the Platform Grant, Co-Investigator Aspinall was promoted to a Personal Chair in Software Safety and Security at the University of Edinburgh. 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. Prof. Bundy, through his work on representational change led to the development the ABC theory repair system, i.e., a system which automatically repairs the representation of a logical theory. ABC was developed by Dr Xui Lin as part of her PhD studies. ABC is powerful because its repairs combine the deleting and/or adding of axiom(s), thus changing the language through which a theory is represented. In addition, it can also modify the preconditions of logical rules. These rich repairs allow ABC to be applicable across a range of domains, including modelling virtual bargaining games, the root cause analysis based on system logs and the formalisation of laws for autonomous vehicles. The Platform Grant FF provided vital bridge funding between the completion of Dr Kobby Nuamah's PhD and the start of PDRA funding. During this time, Kobby explored the use of templates for the interface of the Rich Inference Framework (RIF). The ideas generated while on the bridge funding were useful in subsequent work on the user interface of the FRANK question-answering system, resulting in three industry-funded projects (with Huawei) at the University of Edinburgh. In 2023, Kobby's work on the FRANK system led to a spin-out opportunity which included getting accepted into the Innovate UK-funded ICURe programme. He is now in the process of applying for funding from Scottish Enterprises to launch a spin-out. Prof. Bundy and Prof. Ireland contributed to a UKRI funded Trustworthy Autonomous Systems Node in Governance and Regulation grant (EP/V026607/1). Their contributions focused on the management of representational change and the use of formal modelling in anticipating accidents. The development of the ideas that underpinned these contributions can be traced back directly to the Platform Grant funding. Through the 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 termination of the Platform Grant funding scheme ended 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. The history and impact of the DReaM Group is described in research monograph entitled: "Mathematical Reasoning: The History and Impact of the DReaM Group", which was published in 2021 by Springer. |
| First Year Of Impact | 2020 |
| 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 | 08/2020 |
| End | 08/2023 |
| Description | Carnegie Trust Research Internship |
| Amount | £1,400 (GBP) |
| Organisation | Carnegie Trust |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 05/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 | 03/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 | 03/2020 |
| End | 03/2021 |
| 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 | 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 | 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 | 07/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 | 08/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 | 06/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 | 04/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 | 09/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 | |
| Year Established | 2010 |
| Impact | TheoryMine was the first company in the World to offer such a theorem naming service. |
| Website | http://www.theorymine.com |
| 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/ |