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 Author https://orcid.org/0000-0002-3354-0383
Tatyana Yu. Zvereva Siberian Federal University, Department of Algebra and Mathematical Logic, 660041, Svobodny #79, Krasnoyarsk, Russia Author 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 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 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

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 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

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.

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 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 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 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 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.

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 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 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 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 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 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).

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.

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 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