Modal logic

Stream: new members

[Pedro Minicz]

Has any modal logic been formalized in Lean?

[Johan Commelin]

@Simon Hudon did some stuff a while ago. Maybe his talk at Lean Together 2019 is online somewhere?

[Pedro Minicz]

Just found the slides here and it looks very promising.

[Pedro Minicz]

A quick search didn't reveal a video, however. If it was recorded I would love to see it.

[Bryan Gin-ge Chen]

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

[Patrick Massot]

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]

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]

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

[Minchao Wu]

And here is the slides: https://itp19.cecs.pdx.edu/wp-content/uploads/2019/09/wu_slides.pdf

[Donald Sebastian Leung]

(deleted)

[Alexandre Rademaker]

The repo is https://github.com/minchaowu/ModalTab