A many-sorted polyadic modal logic

TL;DR

This paper introduces a many-sorted polyadic modal logic that extends existing frameworks, providing algebraic semantics and connecting to program verification through Matching logic.

Contribution

It develops a new many-sorted modal logic with algebraic semantics and proves a Jf3nsson-Tarski-like theorem, bridging modal logic and program verification.

Findings

Established algebraic semantics for the logic

Proved a Jf3nsson-Tarski-like theorem

Connected the logic to Matching logic for program reasoning

Abstract

This paper presents a many-sorted polyadic modal logic that generalizes some of the existing approaches. The algebraic semantics has led us to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the J\'onsson-Tarski theorem. While the transition from the mono-sorted logic to many-sorted one is a smooth process, we see our system as a step towards deepening the connection between modal logic and program verification, since our system can be seen as the propositional fragment of Matching logic, a first-order logic for specifying and reasoning about programs.