On January 11, 2024 at 14:00 EET, Alexandru Oltean (University of Bucharest) will give a talk in the Logic Seminar.
Title: Formalizing Hybrid Modal Logic in Lean
Abstract:
Following a paper by Blackburn and Tzakova (1998), I formalized a variant of hybrid modal logic in Lean 4, together with a proof of soundness and a (work-in-progress, but close-to-finished) proof of completeness. I will focus on the practical challenges that this effort entailed and my proposed solutions; for example, regarding some properties of infinite sets to which I could devise no immediate Lean counterpart.
The code is available here. The implementation is more closely explained in my B.Sc. thesis, available here.
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.