Following the Summer School, we are really proud to host the 2nd Proof Society Workshop. The workshop was an opportunity to listen to a lot of interesting invited and contributed talks on proof theory and various areas of its application: Adam Wyner: Computational Law – The Case of Autonomous Vehicles Yong Cheng: Exploring the incompleteness phenomenon Matthias Baaz: Towards a Proof Theory for Henkin Quantifiers Sonia Marin: On cut-elimination for non-wellfounded proofs: the case of PDL Gilles Dowek: Logical frameworks, reverse mathematics, and formal proofs translation Benjamin Ralph: What is a combinatorial proof system? William Stirton: Ordinal assignments correlated with notions of reduction Oliver Kullmann: Practical proof theory: practical versions of Extended Resolution Anton Setzer and Ulrich Berger on behalf of Ralph Matthes: Martin Hofmann’s case for non-strictly positive data types – reloaded Laura Crosilla: Philosophy of mathematics and proof theory Takako Nemoto: Recursion Theory in Constructive Mathematics Arno Pauly: Combinatorial principles equivalent to weak induction Antonina Kolokolova: The proof complexity of reasoning over richer domains Joost Joosten: The reduction property revisited Helmut Schwichtenberg: Computational content of proofs Thanks to all the speaker and participants and we hope to see you all again soon.
The Proof Theory Summer School will be followed by the Workshop on September 11-13, 2019. For more information click below:
Today as a part of the 2nd World Logic Day our Theory group commemorated the work of Erik Palmgren (1963-2019), who sadly passed away last year. Anton Setzer presented Erik’s most influential papers, which had a big impact on Anton’s own research.
We meet to remember the great logician Erik Palmgren who sadly passed away in November 2019 . To honor Erik Palmgren’s work, Anton Setzer will give a talk with the title: Palmgren’s interpretation of inductive definitions in type theory and development of higher type universes in type theory. The meeting also marks the 2nd World Logic Day. Venue: Theory Lab (CoFo 209) Time: 14th of January 2020, 2-3 pm
We are glad to welcome Hideki Tsuiki in Swansea again. This Thursday we really enjoyed his talk on “Imaginary Cubes — Mathematics, Puzzle, Art and Education”. Abstract: Imaginary cubes are three-dimensional objects with square projections in three orthogonal ways just as a cube has. How many different kinds of imaginary cubes can you imagine? In this talk we show that there are 16 kinds of minimal convex imaginary cubes which includes regular tetrahedron, cuboctahedron, and two objects that we call H and T. As we will explain, H and T have a lot of beautiful mathematical properties related to tiling, fractal, and higher-dimensional geometry, and based on these properties, the speaker has designed a puzzle, constructed three-dimensional math-art objects, and used them for educations at various levels from elemental school to graduate schools. In this talk, I will explain mathematics of imaginary cubes and show the activities I have been engaged in. I will carry a couple of copies of the puzzle and some of the math-art objects so that the audience can enjoy them while I am staying in Swansea.
Congratulations to Iris van der Giessen for winning the best poster competition and special thanks to Andreas Weiermann for the beautiful picture of Wales that serves as our main prize. Big thanks to all the speakers and the participants for joining our Summer School. We hope to see you again during the future events by the Proof Society.
We are very glad to welcome all the participants of the 2nd International Summer School on Proof Theory. The first day began with a lecture on Universal Proof Theory by Rosalie Iemhoff, followed by Wolfram Pohlers‘ talk on Ordinal Analysis, Bounded Arithmetic lecture from our own Arnold Beckmann, introduction to Proof Mining by Paulo Oliva, Paola Bruscoli’s talk on Structural Proof Theory and Anton Setzer’s lecture on MLTT. We were lucky with both the lovely weather and the fact that Bay Campus is located right at the seafront, so the evening brought a nice treat for everyone in a form of a BBQ at the beach. Big thanks to Arnold, Faron for their grilling and Ulrich, Rosalie, Monika, Arved, Aled, Anton, Olga and everyone else who helped with the organisation.
Proof Society Summer School is going to take place at our Computational Foundry this September. For more information and to apply, please click on the image below:
Philipp Schlicht is visiting us today from Bristol. He’ll give us an introduction to automatic structures in the theory seminar today (2pm, CoFo 201). Abstract: Automatic structures were first studied by Khoussainov and Nerode in 1995. I will first give an introduction with a focus on automatic ordinals and groups and then talk about tree-automatic structures. In particular, I will mention some recent partial results with Jain, Khoussainov and Stephan on the isomorphism problem for tree-automatic ordinals.
This week we are glad to welcome two visitors here at Swansea, namely Hideki Tsuiki from Kyoto University and Kristijonas Čyra from the Imperial College of London. Hideki will give a talk on “Infinite Adequacy Theorem through Coinductive Definitions” today at 14:00 as a part of our Theory seminar series and Kristijonas will speak on “Argumentation-enabled Explainable AI Applications” this Thursday at 15:00 at the CoFo.