Stream: new members
Topic: Modal logic
Pedro Minicz (Jun 06 2020 at 05:06):
Has any modal logic been formalized in Lean?
Johan Commelin (Jun 06 2020 at 05:28):
@Simon Hudon did some stuff a while ago. Maybe his talk at Lean Together 2019 is online somewhere?
Pedro Minicz (Jun 06 2020 at 05:34):
Just found the slides here and it looks very promising.
Pedro Minicz (Jun 06 2020 at 05:35):
A quick search didn't reveal a video, however. If it was recorded I would love to see it.
Bryan Gin-ge Chen (Jun 06 2020 at 05:36):
Patrick Massot (Jun 06 2020 at 08:33):
Yes, it's there, at 2:05. Don't get confused by the fact that Simon is so great that he gave two talks in the same morning.
Simon Hudon (Jun 06 2020 at 14:50):
The repo is not in a great state right now but I'm going to fix it in the near future. Also, it's a shallow embedding of temporal logic with an accompanying proof mode. For a deep embedding, I believe @Minchao Wu presented interesting results about decision procedures in modal logic at the same workshop
Jeremy Avigad (Jun 06 2020 at 18:19):
Minchao's paper is here: https://drops.dagstuhl.de/opus/volltexte/2019/11086/.
Minchao Wu (Jun 10 2020 at 09:49):
And here is the slides: https://itp19.cecs.pdx.edu/wp-content/uploads/2019/09/wu_slides.pdf
Donald Sebastian Leung (Jun 10 2020 at 13:37):
Alexandre Rademaker (Apr 04 2021 at 00:44):
The repo is https://github.com/minchaowu/ModalTab
Last updated: May 17 2021 at 23:14 UTC