Speaker: Jiatu Li
Date and Time: Thursday, June 10th 2021, 15:00-16:30, Amsterdam time.
Venue: online. Click here for the recording.
Title: Formalization of PAL in Lean.
Abstract. A 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 the Lean theorem prover. We will also discuss in general the potential applications of proof assistants in logic research.
See also https://arxiv.org/abs/2012.09388