Skip to content


Formalising the correct termination, fairness, and tractability of Meek’s method of STV in Isabelle/HOL

    Date: 27th September 2019
    Time: 15:00 - 16:00

    Title: Formalising the correct termination, fairness, and tractability of Meek's method of STV in Isabelle/HOL
    Speaker: Jake Palmer

    I will present my work on formalising various properties of Meek's method of STV. So far I have represented and proved the quantities, assumptions, and theorems in the paper "Algorithm 123: Single transferable vote by Meek's method", wherein they provide a proof that when some number of candidates are elected at some stage of the process, they remain elected and their votes converge on the quota (i.e. what a candidate needs to be elected) and this converged-to state is unique. I will briefly present some ideas on a more complete proof of correct termination which takes into account filling seats, and some ideas on how to go beyond that to making the notions of fairness and "wasted votes" in Meek rigorous and formally proving they are satisfied by the method. Finally, I will finish off the work by proving the tractability of the method in terms of its time complexity, and extract the verified algorithm.

    L’Hopital’s Theorems and Euler’s Notions of Orders of Infinity in Isabelle/HOL

      Date: 8th August 2019
      Time: 14:00 - 16:00

      Title: L'Hopital's Theorems and Euler's Notions of Orders of Infinity in Isabelle/HOL
      Speaker: Kyriakos Katsamaktsis
      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.

      Hybrid Process Mining

        Date: 5th July 2019
        Time: 14:00 - 16:00

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

        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.

        Predicting graft and patient survival following liver transplantation

          Date: 28th June 2019
          Time: 14:00 - 16:00

          Title: Predicting graft and patient survival following liver transplantation
          Speaker: Simon Thorogood
          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.

          Formal Resource Flow Composition

            Date: 14th June 2019
            Time: 14:00 - 16:00

            Title: Formal Resource Flow Composition
            Speaker: Petros Papapanagiotou
            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.

            Nonstandard Analysis for Euler’s Proof of the Basel Problem

              Date: 31st May 2019
              Time: 14:00 - 16:00

              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.

              Formalising the correct convergence of Meek’s method of STV in Isabelle/HOL

                Date: 3rd May 2019
                Time: 14:00 - 16:00

                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.

                Reinforcement Learning Applied to Natural Deduction

                  Date: 19th April 2019
                  Time: 14:00 - 16:00

                  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.