Talks

Title: Composing Processes in Isabelle
Speaker: Filip Smola
Abstract: 

In many domains we are confronted with complex processes, from manufacturing workflows to administrative tasks. When analysing such processes, the formal representations involved can quickly get too large for a human to correctly and efficiently manipulate. My PhD project is on mechanising the notion of process compositions, verifying correctness-preserving methods for constructing them, and demonstrating the applications of the resulting formalism. In this talk I will give an overview of my project and my progress so far. I will present the highlights of my mechanisation in Isabelle and note some of the more interesting choices I made along the way. I will also outline the path forward in the coming months.

Title: Productive use of uncertain events in Business Process Management
Speaker: Jiawei Zheng
Abstract: 

Complex event processing (CEP) and Business Process Management (BPM) have traditionally been researching on distinct application areas, but some novel scenarios would allow to involve the combination of both aspects. Particularly, in the context of Internet of Things (IoT),  CEP is often concerned with low-level events that may related to a specific activity in a business process. Specifically, the events are most often under uncertainty, ranging from erroneous or incomplete data streams to incomplete event detection patterns. There are great challenges and opportunities to integrate CEP into BPM to predict the potential disruptive events and estimate the duration of the process under the uncertainty.

Title: Summarising Care Home COVID-19 Outbreak Data
Speaker: James Vaughan
Abstract: 

The COVID-19 pandemic has disproportionately affected those living in care homes globally and, in Scotland, residents of care homes account for 47% of fatalities between March and June last year. These deaths primarily occurred in the care homes that experienced an outbreak and left a large population of vulnerable residents. I  will present how we automatically summarise and visualise this outbreak data to assist care providers, including the technical details of processing it in Excel.

Title: Formal Verification of Reinforcement Learning
Speaker:  Mark Chevallier
Abstract: 

This talk is in preparation for the one I will give at FMAI 21. I will discuss my work formalising reinforcement learning and the progress I have made in doing so. My methods used to model Markov Decision Processes with rewards, the main results achieved with those methods, and my recent work on vector translation of functions on MDPs will all be featured.

Title: An overview of the ACRC New Technologies of Care Research plans
Speaker: Jacques Fleuriot and Petros Papapanagiotou
Abstract: The Advanced Care Research Centre (ACRC) is an ambitious £20m research programme funded by Legal and General to look at how care for the person in later life can be improved. It consists of 6 large research workpackages (WP) spanning the social sciences, health and care, artificial intelligence, engineering and much more, and of a PhD academy that will recruit and train 36 students over the next 7 years. The New Technologies of Care WP for its part will aim to develop practical, care-driven technologies that are fit for people in later life. In particular, this will mean exploring and developing sensor-specific data-driven IoT platforms that can produce accurate data about instant events (e.g. vital signs and serious incidents such as falls), short- term activities (e.g. those of daily living) and long-term pursuits (e.g. physical and mental activities over weeks and months) in order to extract (predictive) information and patterns that can be used, among other things, for the prevention of adverse events, adherence to care pathways and effective interventions.

Title: Integrating machine learning and symbolic AI to improve predictive models in healthcare
Speaker: Jorge Gaete
Abstract: The critical nature of medical tasks makes explainability an essential quality of any support system for this domain. Various techniques have been developed to provide explainable ML models for healthcare, nevertheless challenges still exist. Issues such as the integration of multiple sources of information or user interaction with the models are important areas of research to achieve more understandable models. In this talk we introduce our approach to tackling some of these issues by combining current explainable machine learning techniques and symbolic AI. As part of my second-year review, I will present a research pipeline and current work on its implementation and plans for future work. Special attention will be placed on the extraction of clusters as an approach to explain patterns of multimorbidity in patients and also the usage of logic programming to create a simple diabetes risk-predictor.

Title: Computerising Euler's Foundations of Differential Calculus using Nonstandard Analysis
Speaker: Richard Stansfield
Abstract: I will discuss my progress using nonstandard analysis in Isabelle to rigorously formalise of a handful of Euler’s proofs from his Foundations of Differential Calculus. I will walk through an example of this process, highlighting the challenges that Euler's reasoning and Isabelle present and where I am in my project.

Title: Exploring Euler's Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis
Speaker: Alice Johansen
Abstract: In 1755, Euler published 'Foundations of Differential Calculus' which presented and defined theories of differential calculus. While influential, Euler's text has been criticized by many for lacking rigour, particularily when it comes to his treatment of infinitesimal numbers. For my project, I've attempted to formulate Euler’s reasoning in a rigourous setting, using Isabelle with nonstandard analysis. Isabelle with nonstandard analysis has been a powerful tool for this project, where my goal is to understand how Euler's proofs must be adapted and elaborated upon in order to maintain rigour and consistency. My project focuses on Euler's proofs of the differentials of trigonometric functions, which require consideration when replicated in Isabelle due to their domains and relationships.

Title: Detection of time needed to find study space in the Main Library using Wi-Fi data
Speaker: Dimitris Christodoulou
Abstract: Finding empty space to study in the Main Library can be challenging, particularly in busy periods such as during exams. The aim of this project is to analyse Wi-Fi data in an effort to detect movement patterns in the Library and identify users that eventually settle down in a particular study space. I will describe the progress made on the project so far and outline what remains to be done for the completion of the project.

Title: Developing a New Web Application for the Archive of Formal Proofs
Speaker: Carlin Mackenzie
Abstract:

The Archive of Formal Proofs is functional, however it has not visually changed in almost twenty years. My project aims to rectify this and bring the AFP into the modern day. Previously, I have recreated the website in a more robust static site generator.

Since my last presentation, I have redesigned the user interface, improved discoverability and enhanced code browsing. For each of these, I will explain my approach and demonstrate the latest iteration. Finally, I will present a timeline for the remaining work.