Talks

Title: L'Hopital's Theorems and Euler's Notions of Orders of Infinity in Isabelle/HOL
Speaker: Kyriakos Katsamaktsis
Abstract:
In his paper on "Orders of Infinity" Euler writes, without rigorous proofs, about "infinitely large" and "infinitely small" quantities and how they relate to one another. For example, he writes that if x is infinite, then its logarithm is also infinite, and the ratio of the logarithm of x divided by x is infinitely small. Such statements can be put on a rigorous footing using nonstandard analysis, which treats infinity as a number (or more than one) without using limits. We will describe the formalisation of parts of Euler's paper in Isabelle using nonstandard analysis. We will shed light on a few vague statements and show how fairly standard modern mathematics plus some nonstandard analysis can resolve them.

Title: Hybrid Process Mining: Combining Imperative & Declarative Paradigms
Speaker: Christoffer Olling Back (PhD Fellow, Department of Computer Science, University of Copenhagen)
Abstract:

Modern organisations generate enormous amounts of data related to their business processes via IT systems such as Enterprise Resource Planning (ERP) systems. Mining process related data presents the opportunity for a truly data-driven approach to streamlining operations and building an intelligent enterprise. Depending on the use case, process mining may be employed with the aim of detecting deviations from a well-defined process, identifying areas for process enhancement (detecting bottlenecks, unnecessary rework), and in the case of pure process discovery – where the underlying process is not known – the task essentially becomes comparable to unsupervised learning.

In this talk, I will begin with a brief introduction to process mining generally, positioning the field in relation to data mining and machine learning. Afterwards, I will discuss different process modelling paradigms in more detail, and their strengths and weaknesses. In particular, the distinction between declarative (constraint-based) and imperative (flow-based) languages, and how they can be combined to form hybrid process models which combine the strengths of both. Time permitting, I will discuss my ongoing work on developing process mining algorithms which generate hybrid models by identifying pockets of regularity using an information theoretic approach, as well as challenges in empirically evaluating process mining algorithms.

Title: Predicting graft and patient survival following liver transplantation
Speaker: Simon Thorogood
Abstract:
I'll aim to cover a bit of the medical background (Why do people need liver transplants? What are the challenges when allocating livers?). I'll also talk about the NHSBT dataset I am using and some of the traditional statistical approaches to survival prediction (specifically, the field of Survival Analysis). Finally I'll discuss some of the machine learning approaches that I will be applying to the problem.

Title: Formal Resource Flow Composition
Speaker: Petros Papapanagiotou
Abstract:
Resource flows are models of how resources travel across connected processes. They offer a different perspective to more typical workflow models (e.g. flow charts) where the focus is on control flow (the order of execution). Formal composition involves the rigorous, logic-based combination of processes to build resource flows with guaranteed properties, particularly systematic resource accounting (so that resources do no appear from/disappear into thin air). I will describe the problem in the context of the WorkflowFM system developed over the past 11 years. This relies on the HOL Light theorem prover to perform compositions via proof in Classical Linear Logic. In this particular talk I will focus on practical examples to demonstrate the conceptual challenges. Describing this work has been a challenge in itself, as WorkflowFM can fit may different contexts and paradigms (program synthesis, scientific workflows, Business Process Management, data streams handling, etc.). I am hoping to gather some feedback after the talk on your understanding and perspective, towards improving how these concepts can be better presented.

Title: Nonstandard analysis for Euler’s proof of the Basel Problem
Speaker: Imogen Morris
Abstract: I will describe the background theory of nonstandard analysis which I am using to formalise the proof of the Basel problem from Euler's `Introduction to the Analysis of the Infinite'. Euler's arguments using infinity and his theory of infinitesimals are not considered rigorous by present-day mathematicians. However, there is a modern theory of infinities and infinitesimals called nonstandard analysis, which captures many of the properties that 18th century mathematicians ascribed to infinite and infinitesimal numbers. I will explain some of the properties of these numbers and how they can be constructed. I will also explain hyperfinite sums and internal functions, which are both necessary to for my theory of 'infinite polynomials'. I will describe some of the relevant theorems which I have formalised in the proof assistant Isabelle.

Title: Learning over Isabelle's Dependency Graphs
Speaker: James Vaughn

Title: Formalising the correct convergence of Meek's method of STV in Isabelle/HOL
Speaker: Jake Palmer
Abstract: I will present an overview of my work so far on formalising a representation of the surplus transfer phase of Meek's method of STV. I have represented the assumptions characterising the way in which the quota, excess, and votes update given a single update to a candidate's weight, where the weights represent the current state. I will present some convergence and ordering theorems on weights as well as the theorem in Isabelle characterising the first part of Theorem 1 in the paper "Algorithm 123: Single transferable vote by Meek's method". I will briefly present some ideas on the work which will make up the rest of the PhD such as implementing Meek's method in Isabelle, situating the method within the framework of social choice theory, showing that the method is not susceptible to the butterfly effect in voting, and producing Meek's method automatically as the output of generating a method/policy for minimising wasted votes in the context of STV.

Title: Reinforcement Learning Applied to Natural Deduction
Speaker: Mark Chevallier
Abstract: Reinforcement learning is a set of methods for an agent to learn how to act in a given environment using "rewards" to encourage correct action. Natural deduction is a method to prove statements based on "natural" reasoning with limited axioms and a small set of logical rules that can be applied to a set of statements to deduce further statements.

I discuss how to apply the tools of reinforcement learning to natural deduction applied to propositional logic. I present a simple python based example and discuss its implementation. Early problems included how to limit the assumptions the reinforcement learning engine could make, related to what it could add to an OR statement, and finding a reasonable sense of "state" for the agent. I demonstrate the theoretical effectiveness of the approach by showing limited success in proving simple deductions.

Title: Applications of Explainable AI in Healthcare
Speaker: Jorge Gaete