2018/03/26 by Leustean, Ioana, Moanga, Natalia, Serbanuta, Traian Florin
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1803.09709
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ónsson-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.