Zulip Chat Archive

Stream: new members

Topic: Modal logic


view this post on Zulip Pedro Minicz (Jun 06 2020 at 05:06):

Has any modal logic been formalized in Lean?

view this post on Zulip 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?

view this post on Zulip Pedro Minicz (Jun 06 2020 at 05:34):

Just found the slides here and it looks very promising.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jun 06 2020 at 05:36):

The Lean Together 2019 page suggests that his talk might be in the Wednesday morning recording.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jeremy Avigad (Jun 06 2020 at 18:19):

Minchao's paper is here: https://drops.dagstuhl.de/opus/volltexte/2019/11086/.

view this post on Zulip 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

view this post on Zulip Donald Sebastian Leung (Jun 10 2020 at 13:37):

(deleted)

view this post on Zulip 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