AIAI Seminar - 26/04/21 - Jake Palmer & Lukas Schafer

Speaker: Jake Palmer

Title: Mechanisation of an axiom system for Minkowski spacetime in Isabelle/HOL

Abstract:

In an effort to establish verified foundations for relativistic physics, we mechanise Minkowski spacetime from a system of axioms devised by John W Schutz in "Independent axioms for Minkowski space-time". This enterprise occurs in the interactive theorem prover Isabelle/HOL, which facilitates trusted certification of proofs, and provides automated tools for assistance. We have completed the mechanisation of the 15 axioms (of order, incidence, symmetry, and continuity), and -- with some asterisks -- the first chapter of Schutz "Temporal order on a path". In this presentation we present an overview of this work to date and some ideas about where we go from here.

Bio: I am a third year PhD student supervised by Jacques Fleuriot. My main project is using the interactive theorem prover Isabelle/HOL to represent and reason about Single Transferable Vote systems, but I will be talking about my masters project which has since been continued by Richard Schmoetten and soon Mathis Gerdes, and which I have continued to be involved in.

Speaker: Lukas Schafer

Title: Multi-Agent Reinforcement Learning for Real-World Warehouse Optimisation

Abstract:

Real-world warehouse systems often include dozens of actors managing the collection and delivery of items. Such systems often contain hundreds of shelves containing various items. Most such work is still completed by humans due to their reliability and adaptability. However, significant research and innovation efforts are done to enable the automation of such systems. In this talk, I will present the challenges of warehouse automation, multi-agent reinforcement learning approaches to address these challenges and show results of applying such methods in a warehouse simulation. We find that parameter sharing multi-agent reinforcement learning methods are able to outperform manually defined heuristics and present future work to address the significant challenge of scalability. This work has been conducted as part of an internship and consultancy project with Dematic GmbH.

Bio: I am a PhD student, supervised by Dr. Stefano Albrecht, working on multi-agent reinforcement learning. In particular, I am interested in exploration research and generalisation of multi-agent reinforcement learning to make these approaches more applicable to real-world problems.

Apr 26 2021 14.00 - 15.00

AIAI Seminar - 26/04/21 - Jake Palmer & Lukas Schafer

AIAI Seminar talk hosted by Jake Palmer & Lukas Schafer

Online