Skip to content

Talks

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.