A Many-sorted Polyadic Modal Logic
Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă · Fundamenta Informaticae · 2020
We propose a general system that combines the powerful features of modal logic and many-sorted reasoning. Its algebraic semantics leads to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the Jónsson-Tarski theorem. Our goal was to deepen the conne ctions between modal logic and program verification, while also testing the expressiveness of our system by defining a small imperative language and its operational semantics.