Dear all,

This is a reminder that our LIRa session with Jiatu Li today will take place at an UNUSUAL TIME, namely 15:00-16:30. You can find the details of the talk below. We will use our recurring zoom link: https://uva-live.zoom.us/j/92907704256?pwd=anY3WkFmQVhLZGhjT2JXMlhjQVl1dz09 (Meeting ID: 929 0770 4256, Passcode: 036024).

Speaker: Jiatu Li Date and Time: Thursday, June 10th 2021, 15:00-16:30, Amsterdam time. Venue: online. Title: Formalization of PAL in Lean.

Abstract.

Proof assistant (or theorem prover) is a useful tool to organize and check formal mathematical proofs. Despite of several impressive stories, it still seems hopeless for common mathematicians to use it for their daily work. However, it may be handy for logicians in some certain applications, for example, in developing proof systems. In this talk, we will demonstrate a formalization of public announcement logic (including syntax, semantics, a proof system and meta-theorems including soundness and completeness) in Lean theorem prover. We will also discuss in general the potential applications of proof assistant in logic research.

Hope to see you there!

The LIRa team