A Many-sorted Polyadic Modal Logic

Issue title: Special Issue on The Working Formal Methods Symposium (FROM 2018)

Guest editors: Jetty Kleijn, Laurenţiu Leuştean and Dorel Lucanu

Article type: Research Article

Authors: Leuştean, Ioana | Moangă, Natalia^{; *} | Şerbănuţă, Traian Florin

Affiliations: Faculty of Mathematics and Computer Science, University of Bucharest, Bucharest, Romania. [email protected], [email protected], [email protected]

Correspondence: [*] Address for correspondence: Faculty of Mathematics and Computer Science, University of Bucharest, Bucharest, Romania

Abstract: 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 connections between modal logic and program verification, while also testing the expressiveness of our system by defining a small imperative language and its operational semantics.

Keywords: Polyadic modal logic, many-sorted logic, boolean algebras with operators, many-sorted algebras, Jónsson-Tarski theorem, operational semantics

DOI: 10.3233/FI-2020-1921

Journal: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 191-215, 2020