Abstract
In this paper, we investigate dynamic modal logics with global and local dynamic operations, which update the accessibility relation of a graph model. We introduce the hybrid logic \(\textsf{GLV}\) of global link variations, which involves dynamic operators of global link cutting, adding and rotating simultaneously. We provide the Hilbert-style calculus \(\mathsf {C_{GLV}}\) and prove that it is sound and strongly complete with respect to \(\textsf{GLV}\) by constructing a family of canonical models inductively. We study the hybrid extensions of the logic \(\textsf{LLD}\) of definable link deletion introduced by Li (2020). We provide a sound and complete tableau calculus \(\mathcal {T}(\textsf{LLD}(@))\) for the logic \(\textsf{LLD}(@)\). Then we extend \(\textsf{LLD}(@)\) to the logics \(\textsf{LLV}(@,X)\) of local link variations and provide them with sound and complete tableau calculi. Furthermore, we extend the logic \(\textsf{LLV}\) to \(\textsf{LLV}(\downarrow \hspace{-.3em}\, ,\textsf{E})\) by adding the hybrid operator \(\downarrow \hspace{-.3em}a.\) and existential modality \(\textsf{E}\). By defining local named dynamic operators and providing recursion axioms for them, we obtain a sound and strongly complete calculus \(\mathsf {C_{LLV}}\) for \(\textsf{LLV}(\downarrow \hspace{-.3em}\, ,\textsf{E})\). Finally, we show that for any set X of global or local operators, the calculus \(\mathsf {C_{GLV}}(X)\) and \(\mathsf {C_{LLV}}(X)\) are still sound and strongly complete w.r.t the logic \(\textsf{GLV}(X)\) and \(\textsf{LLV}(\downarrow \hspace{-.3em}\, ,\textsf{E},X)\), respectively.
Similar content being viewed by others
Notes
In this paper, we do not distinguish the types of relationships. We could always consider logics of link variations based on poly-modal logics, where we can easily have different types of relations between worlds.
We write IH for induction hypothesis.
\(\llbracket {\psi }\rrbracket =\{ u\in W:\mathfrak {M},u\models \psi \}\)
We define \(R(w,\psi )=\{ w\}\times (\llbracket {\psi }\rrbracket \cap R(w))\) and \(R^{-1}(w,\psi )=\{ {\langle u,w\rangle }:{\langle w,u\rangle }\in R(w,\psi )\}\).
If \((u, v) \in E\), then \( u \) is called the parent of \( v \), and \( v \) is called the child of \( u \).
References
Areces, C., Fervari, R., & Hoffmann, G. (2012). Moving arrows and four model checking results. In L. Ong & R. Queiroz (Eds.), Logic, Language, Information and Computation, 142–153. Berlin, Heidelberg: Springer.
Areces, C., Fervari, R., & Hoffmann, G. (2013). Tableaux for relation-changing modal logics. Springer.
Areces, C., Fervari, R., & Hoffmann, G. (2015). Relation-changing modal operators. Logic Journal of the IGPL, 23(4), 601–627.
Areces, C., Fervari, R., Hoffmann, G., & Martel, M. (2018). Satisfiability for relation-changing logics. Journal of Logic and Computation, 7, 1443–1470.
Aucher, G., van Benthem, J., & Grossi, D. (2015) Sabotage modal logic: Some model and proof theoretic aspects. In: Hoek, W., Holliday, W., Wang, W. (eds.) Proceedings of LORI 2015. LNCS, 9394, 1–13.
Baltag, A., Li, D., & Pedersen, M. Y. (2022). A modal logic for supervised learning. Journal of Logic, Language and Information, 213–234.
Baltag, A., Moss, L. S., & Solecki, S. (1998). The logic of public announcements. Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge
Belardinelli, F., Ditmarsch, H. V., & Hoek, W. (2017). A logic for global and local announcements. Electronic Proceedings in Theoretical Computer Science (pp. 28–42)
Du, P., & Chen, Q. (2024). Axiomatization of hybrid logic of link variations. In N. Gierasimczuk & F. R. Velázquez-Quesada (Eds.), Dynamic Logic. New Trends and Applications (pp. 35–51). Cham: Springer.
Gierasimczuk, N., Kurzen, L., & Velázquez-Quesada, F. R. (2009). Learning and teaching as a game: A sabotage approach. In X. He, J. Horty, & E. Pacuit (Eds.), Logic, Rationality, and Interaction, 119–132. Berlin, Heidelberg: Springer.
Hogan, A., Gutierrez, C., & Cochez, M., (2022). Knowledge Graphs. Cham: Springer.
Li, D. (2020). Losing connection: the modal logic of definable link deletion. Journal of Logic and Computation, 30(3), 715–743.
Löding, C., & Rohde, P. (2003a). Solving the sabotage game is Pspace-hard. LNCSIn B. Rovan & P. Vojtáš (Eds.), MFCS ’2003 (Vol. 2747, pp. 531–540)
Löding, C., & Rohde, P. (2003b). Model checking and satisfiability for sabotage modal logic. In P. K. Pandya & J. Radhakrishnan (Eds.), FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 302–313. Berlin, Heidelberg: Springer.
Pedersen, M. Y., Smets, S., & Ågotnes, T. (2021). Modal logics and group polarization. Journal of Logic and Computation, 31(8), 2240–2269.
Rohde, P. (2005). On games and logics over dynamically changing structures. PhD thesis, Department of Informatics, Technische Hochschule Aachen (RWTH).
Seligman, J., Liu, F., & Girard, P. (2011). Logic in the community. In M. Banerjee & A. Seth (Eds.), Logic and Its Applications, 178–188. Berlin, Heidelberg: Springer.
Seligman, J., Liu, F., & Girard, P. (2013). Facebook and the Epistemic Logic of Friendship. https://arxiv.org/abs/1310.6440
ten Cate, B.: Model theory for extended modal languages. PhD thesis, University of Amsterdam (2005)
van Benthem, J. (2005). An essay on sabotage and obstruction. Berlin Heidelberg: Springer.
van Benthem, J. (2014). Logic in games. University of Amsterdam
van Benthem, J., Li, L., Shi, C., & Yin, H. (2022a). Hybrid sabotage modal logic. Journal of Logic and Computation.
van Benthem, J., Mierzewski, K., & Blando, F. Z. (2022b). The modal logic of stepwise removal. The Review of Symbolic Logic,15(1), 36–63.
Wasserman, S., & Faust, K. (1994). Social Network Analysis: Methods and Applications. Cambridge: Structural Analysis in the Social Sciences. Cambridge University Press.
Acknowledgements
We thank Johan van Benthem, Fenrong Liu, Junhua Yu and Dazhu Li for their very helpful suggestions. Thanks to the anonymous reviewers for their insightful comments for improvements. Penghao Du is supported by the National Social Science Fund of China (Grant No. 24&ZD227). Qian Chen is supported by Tsinghua University’s Initiative for Advancing First-Class and World-Leading Disciplines in the Humanities and Social Sciences.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Du, P., Chen, Q. Hilbert-Style Calculus and Tableau Calculus for Logics of Link Variations. J of Log Lang and Inf (2026). https://doi.org/10.1007/s10849-026-09475-x
Received:
Accepted:
Published:
Version of record:
DOI: https://doi.org/10.1007/s10849-026-09475-x