Unification and Finite Model Property for Linear Step-Like Temporal Multi-Agent Logic with the Universal Modality

Stepan I. Bashmakov; Tatyana Yu. Zvereva

doi:10.18778/0138-0680.2022.16

Authors

Stepan I. Bashmakov Siberian Federal University, Department of Algebra and Mathematical Logic, 660041, Svobodny #79, Krasnoyarsk, Russia https://orcid.org/0000-0002-3354-0383
Tatyana Yu. Zvereva Siberian Federal University, Department of Algebra and Mathematical Logic, 660041, Svobodny #79, Krasnoyarsk, Russia https://orcid.org/0000-0002-9222-1331

DOI:

https://doi.org/10.18778/0138-0680.2022.16

Keywords:

multi-agent system, Kripke semantic, unification, modal logic, non-transitive time, step-like, universal modality, finite model property, p-morphism

Abstract

This paper proposes a semantic description of the linear step-like temporal multi-agent logic with the universal modality \(\mathcal{LTK}.sl_U\) based on the idea of non-reflexive non-transitive nature of time. We proved a finite model property and projective unification for this logic.

References

S. I. Bashmakov, Unification and inference rules in the multi-modal logic of knowledge and linear time LTK, Journal of Siberian Federal University. Mathematics & Physics, vol. 9(2) (2016), pp. 149–157, DOI: https://doi.org/10.17516/1997-1397-2016-9-2-149-157
Google Scholar DOI: https://doi.org/10.17516/1997-1397-2016-9-2-149-157

S. I. Bashmakov, Unification in linear modal logic on non-transitive time with the universal modality, Journal of Siberian Federal University. Mathematics & Physics, vol. 11(1) (2018), pp. 3–9, DOI: https://doi.org/10.17516/1997-1397-2018-11-1-3-9
Google Scholar DOI: https://doi.org/10.17516/1997-1397-2018-11-1-3-9

S. I. Bashmakov, Unification in linear multi-modal logic of knowledge and non-transitive time, [in:] Handbook of the 6th World Congress and School on Universal Logic, Vichy, France, Université Clermont Auvergne (2018), pp. 229–231, URL: https://hal-centralesupelec.archives-ouvertes.fr/hal-01812182/file/handbook-unilog2018-web_19-6-2018.pdf
Google Scholar

S. I. Bashmakov, Unification in pretabular extensions of S4, Logica Universalis, vol. 15 (2021), pp. 381–397, DOI: https://doi.org/10.1007/s11787-021-00287-0
Google Scholar DOI: https://doi.org/10.1007/s11787-021-00287-0

S. I. Bashmakov, A. V. Kosheleva, V. V. Rybakov, Non-unifiability in linear temporal logic of knowledge with multi-agent relations, Siberian Electronic Mathematical Reports, vol. 13 (2016), pp. 656–663, DOI: https://doi.org/10.17377/semi.2016.13.052
Google Scholar

S. I. Bashmakov, A. V. Kosheleva, V. V. Rybakov, Unification for multi-agent temporal logics with universal modality, Journal of Applied Logics — IfCoLog Journal of Logics and their Application, vol. 4(4) (2017), pp. 939–954.
Google Scholar

B. Bennett, C. Dixon, M. Fisher, U. Hustadt, E. Franconi, I. Horrocks, M. de Rijke, Combinations of Modal Logics, Artificial Intelligence Review, vol. 17 (2002), pp. 1–20, DOI: https://doi.org/10.1023/A:1015057926707
Google Scholar DOI: https://doi.org/10.1023/A:1015057926707

S. Borgo, Quantificational modal logic with sequential Kripke semantics, Journal of Applied Non-Classical Logics, vol. 15(2) (2005), pp. 137–188, DOI: https://doi.org/10.3166/jancl.15.137-188
Google Scholar DOI: https://doi.org/10.3166/jancl.15.137-188

E. Calardo, V. V. Rybakov, An axiomatisation for the multi-modal logic of knowledge and linear time LTK, Logic Journal of the IGPL, vol. 15(3) (2007), pp. 239–254, DOI: https://doi.org/10.1093/jigpal/jzm010
Google Scholar DOI: https://doi.org/10.1093/jigpal/jzm010

E. Clarke, O. Grumberg, K. Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, vol. 10 (1997), pp. 47–71, DOI: https://doi.org/10.1023/A:1008615614281
Google Scholar DOI: https://doi.org/10.1023/A:1008615614281

W. Dzik, Unitary unification of S5 modal logic and its extensions, Bulletin of the Section of Logic, vol. 32(1–2) (2003), pp. 19–26.
Google Scholar

S. Ghilardi, Unification through projectivity, Journal of Logic Computation, vol. 7(6) (1997), pp. 733–752, DOI: https://doi.org/10.1093/logcom/7.6.733
Google Scholar DOI: https://doi.org/10.1093/logcom/7.6.733

S. Ghilardi, Unification in intuitionistic logic, Journal of Symbolic Logic, vol. 64(2) (1999), pp. 859–880, DOI: https://doi.org/10.2307/2586506
Google Scholar DOI: https://doi.org/10.2307/2586506

V. Goranko, S. Passy, Using the universal modality: Gains and questions, Journal of Logic and Computation, vol. 2(1) (1992), pp. 5–30, DOI: https://doi.org/10.1093/logcom/2.1.5
Google Scholar DOI: https://doi.org/10.1093/logcom/2.1.5

Y. Liu, X. Liu, Application of Mathematics in Computer Field, [in:] Z. Xu, R. Parizi, M. Hammoudeh, O. Loyola-González (eds.), Cyber Security Intelligence and Analytics. CSIA 2020, vol. 1147 of Advances in Intelligent Systems and Computing, Springer, Cham (2020), pp. 413–419, DOI: https://doi.org/10.1007/978-3-030-43309-3_57
Google Scholar DOI: https://doi.org/10.1007/978-3-030-43309-3_57

A. N. Luk’yanchuk, V. V. Rimatskii, An axiomatization for the linear logic of knowledge and time LTKr with intransitive time relation, Siberian Mathematical Journal, vol. 54 (2013), pp. 1037–1045, DOI: https://doi.org/10.1134/S0037446613060104
Google Scholar DOI: https://doi.org/10.1134/S0037446613060104

W. A. Pogorzelski, P. Wojtylak, Completeness theory for propositional logics, Studies in Universal Logic, Birkhäuser Basel (2008).
Google Scholar

V. V. Rybakov, An essay on unification and inference rules for modal logics, Bulletin of the Section of Logic, vol. 28 (1999), pp. 145–157.
Google Scholar

V. V. Rybakov, Best unifiers in transitive modal logics, Studia Logica, vol. 99 (2011), pp. 321–336, DOI: https://doi.org/10.1007/s11225-011-9354-y
Google Scholar DOI: https://doi.org/10.1007/s11225-011-9354-y

V. F. Yun, Polymodal logic of the class of inductive linear time frames, Siberian Electronic Mathematical Reports, vol. 12 (2015), pp. 421–431, DOI: https://doi.org/10.17377/semi.2015.12.035
Google Scholar