A Many-sorted Polyadic Modal Logic

• Autorzy: Leuştean Ioana , Moangă Natalia , Şerbănuţă Traian Florin

Identyfikatory

DOI

10.3233/FI-2020-1921

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

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

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 173, nr 2-3
• Strony: 191--215
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Leuştean Ioana

• Faculty of Mathematics and Computer Science, University of Bucharest, Bucharest, Romania

autor

Moangă Natalia

• Faculty of Mathematics and Computer Science, University of Bucharest, Bucharest, Romania

autor

Şerbănuţă Traian Florin

• Faculty of Mathematics and Computer Science, University of Bucharest, Bucharest, Romania

Bibliografia

• [1] Blackburn P, Venema Y, de Rijke M. Modal Logic, Cambridge University Press, 2002. ISBN:9780521527149.
• [2] Calcagno C, Gardner P, Zarfaty U. Context logic as modal logic: completeness and parametric inex-pressivity, in: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’07), ACM, New York, NY, USA, 2007 pp. 123-134. doi:10.1145/1190215.1190236.
• [3] Floyd RW. Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics. 1967. 19:19-31.
• [4] Frittella S, Greco G, Kurz A, and Palmigiano A. Multi-type display calculus for propositional dynamic logic. Journal of Logic and Computation 2016. 26(6):2067-2104. doi:10.1093/logcom/exu064.
• [5] Frittella S, Greco G, Kurz A, Palmigiano A, and Sikimić V. Multi-type sequent calculi. Proc. Trends in Logic XIII, A. Indrzejczak et al. eds, 2014 pp. 81-93.
• [6] Gehrke M, and Harding J. Bounded lattice expansions. Journal of Algebra 2001. 238(1):345-371. URL https://doi.org/10.1006/jabr.2000.8622.
• [7] Gehrke M, and Jónsson B. Bounded distributive lattice expansions. Mathematica Scandinavica, 2004. 94(1):13-45. URL https://www.jstor.org/stable/24493402.
• [8] Harel D, Kozen D, Tiuryn J. Dynamic logic, MIT Press Cambridge, 2000. ISBN: 9780262082891.
• [9] Heering J, Hendriks PRH, Klint P, Rekers J. The syntax definition formalism SDF — reference manual —, ACM Sigplan Notices 1989. 24(11):43-75. doi:10.1145/71605.71607.
• [10] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM. 1969. 12(10):576-580. doi:10.1145/363235.363259.
• [11] Jacobs B. Many-sorted coalgebraic modal logic: a model-theoretic study, in: Theoretical Informatics and Applications Theoret. Informatics Appl. 2001. 35(1):31-59. URL http://www.numdam.org/item/ITA_2001_35_1_31_0.
• [12] Kracht M. Tools and Techniques in Modal Logic, Studies in logic and the foundations of mathematics, vol. 142, Elsevier, 1999. ISBN: 9780444500557.
• [13] Leuştean I, Moangă N, and Şerbănuţă T. Operational semantics and program verification using many-sorted hybrid modal logic, arXiv:1905.05036.
• [14] Plotkin GD. A Structural Approach to Operational Semantics. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61), 2004 pp. 17-139. doi:10.1016/j.jlap.2004.05.001.
• [15] Reynolds JC. Separation logic: A logic for shared mutable data structures, in: Logic in Computer Science Proceedings. 17th Annual IEEE Symposium on. IEEE, 2002 pp. 55-74. doi:10.1109/LICS.2002.1029817.
• [16] Roşu G. Matching logic in: Logical Methods in Computer Science 2017. 13(4):1-61. doi:10.23638/LMCS-13(4:28)2017.
• [17] Rößiger M. From modal logic to terminal coalgebras, in: Electronic Notes in Theoretical Computer Science 2000. 33:1-22.
• [18] Schröder L, Pattinson D. Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra, in: Mathematical Structures in Computer Science. 2011. 21(2):235-266. URL https://doi.org/10.1017/S0960129510000563.
• [19] van Benthem J. A Note on Dynamic Arrow Logic, in: Tech Report, July 1992, Institute for Logic, Language and Computation,. University of Amsterdam; published in Jan van Eyck & Albert Visser, eds., Logic and Information Flow, The MIT Press, Cambridge (Mass.), 1994 pp. 15-29.
• [20] Venema Y. Points, lines and diamonds: a two-sorted modal logic for projective planes, in: Journal of Logic and Computation. 1999. 9(5):601-621. doi:10.1093/logcom/9.5.601.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).