In spite of the COVID-19 outbreak, we are glad to host BCTCS 2020 starting today, even if virtually. For more information on invited and contributed talks, check the official BCTCS 2020 website.

# Category Archives: Invited talk

# 25th International Workshop on Algebraic Development Techniques 2020

Today Swansea is hosting the first virtual WADT, and you are gently invited to participate.

The virtual WADT is part of the 25th International Workshop on Algebraic Development Techniques 2020, which hopefully will still happen as a physical meeting in autumn this year. The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems).

The workshop takes place under the auspices of IFIP WG 1.3.

Please see below for the programme.

# Yoruki Yamagata’s talk on Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning

**Due to COVID-19 outbreak across the world, we need to move our theory seminars online to ZOOM.** We are staying on track with the schedule and **Yoriyuki Yamagata** will give his talk tomorrow at 2pm.

Topic:* Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning.*

Abstract: “Falsification” is a method to find a system input or parameter (counter-example) which causes a behavior violating a given specification (usually given by metric or signal temporal logic). Because the correctness of a complex CPS is difficult to be proven, falsification is more practical approach than full verification. A counter-example found by falsification can be used for debugging and testing. Failure of falsification does not generally mean the correctness of the system, but suggests it in some degree. “Robustness guided falsification” is an approach of falsification. “Robustness” is a numerical measure of how robustly a formula holds. If robustness becomes negative, the formula is false. Therefore, minimizing robustness can lead falsification of a formula.

In this talk, we introduce a method to recast robustness guided falsification to a “reinforcement learning problem”. Reinforcement learning is a machine learning technique in which an agent finds a law of an interacting environment and maximizes a reward. We implement our method using “deep reinforcement leaning”, in which deep neural networks are used, and present a case study to explore its effectiveness. (This work is a collaboration with Shuang Liu, Takumi Akazaki, Yihai Duan, Jianye Hao)

# Paul Shafer is coming to Swansea

# Hideki Tsuiki is back in Swansea

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.

# 2nd Proof Society Workshop on Proof Theory and its Applications

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.

# Summer School: Day 4

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.

# Proof Society Summer School

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.

# Workshop on Proof Theory and its Application

# Federico Cerutti visiting

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.*