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.
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.
Federico Cerutti from Cardiff University is visiting us this Thursday. He will give a talk on Probabilistic Logic Programming with Beta-Distributed Random Variables.
Abstract: We enable aProbLog—a probabilistic logical programming approach—to reason in presence of uncertain probabilities represented as Beta-distributed random variables. We achieve the same performance of state-of-the-art algorithms for highly specified and engineered domains, while simultaneously we maintain the flexibility offered by aProbLog in handling complex relational domains. Our motivation is that faithfully capturing the distribution of probabilities is necessary to compute an expected utility for effective decision making under uncertainty: unfortunately, these probability distributions can be highly uncertain due to sparse data. To understand and accurately manipulate such probability distributions we need a well-defined theoretical framework that is provided by the Beta distribution, which specifies a distribution of probabilities representing all the possible values of a probability when the exact value is unknown.
Federico Cerutti's research activity is focused mainly on nonmonotonic reasoning (in particular argumentation theory), and on decision support with uncertainty and trust.
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.
My research focus is set theory -- in particular, descriptive set theory, forcing, large cardinals -- and computability. I work as a Marie Curie Research Fellow on the project 'Inner models and infinite computations' together with Prof. Philip Welch.
Abstract: Robotic systems are multi-dimensional entities, combining both hardware and software, that are heavily dependent on, and influenced by, interactions with the real world. They can be variously categorised as embedded, cyberphysical, real-time, hybrid, adaptive and even autonomous systems, with a typical robotic system being likely to contain all of these aspects. The techniques for developing and verifying each of these system varieties are often quite distinct. This, together with the sheer complexity of robotic systems, leads us to argue that diverse formal techniques must be integrated in order to develop, verify, and provide certification evidence for, robotic systems. Furthermore, we propose the fast evolving field of robotics as an ideal catalyst for the advancement of integrated formal methods research, helping to drive the field in new and exciting directions and shedding light on the development of large-scale, dynamic, complex systems.
Research Assistant in the Department of Computer Science at the University of Liverpool, working on the Autonomous Robots in Hazardous Environments project.
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.
Professor (Course of Mathematical Science, Graduate School of Human and Environmental Studies, Kyoto University). Ressearch Interests: Computation over Real numbers and Topological spaces, Domains and their topologies, Fractals and their models, Semantics of Programming Languages, Object Oriented Programming, Mathematical Logic, Lambda Calculus.
Postdoctoral Researcher in AI at the Department of Computing, Imperial College London. I manage researchers, enthusiastically supervise and teach students, present my work at top tier international conferences, review and assess the works of others and give highest quality feedback, organise research events, represent and speak on behalf of my colleagues and fellow AI researchers during institutional and public engagement opportunities.
Today Martin Caminada (Cardiff University) is visiting Swansea. He will give a talk about “A Logical Account of Dishonesty” as a part of out Theory seminar series.
Abstract: Although formal logic is usually applied to reason about truth, in the current resentation we apply it to reason about dishonesty. Based on work in philosophy, we provide a formalisation of different forms of dishonesty, including lies, half-truth and bullshit, and discuss their formal properties. We also provide maxims for dishonest communication, that agents should ideally try to satisfy, both for moral and self-interested reasons.
Martin Caminada has as main research interests formal models of human argument and argumentation as a form of nonmonotonic reasoning. In 2004 he obtained a Ph.D. in computer science with his thesis “For the Sake of the Argument; explorations into argument-based reasoning”. From 2004 to 2007 he w…
Dongseong Seon (선동성) from KAIST, Korea is visiting Swansea. This Thursday he will give a talk on computing Haar averages as a part of our Theory seminar series. For more infromation on this topic, please click here.