Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean

Andrei-Alexandru Oltean, Bogdan Macovei, Ioana Leuştean

We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification…