Document Open Access Logo

Axiomatizability of Alexandrov Dynamic Topological Logic

Authors Niels C. Vooijs , David Fernández-Duque

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.81.pdf
  • Filesize: 1.25 MB
  • 26 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • dynamic topological logic
  • Alexandrov spaces
  • computable enumerability
  • modal logic
  • temporal logic

Metrics

Abstract

Dynamical systems provide rigorous models of movement or evolution over time. Due to their abstract nature, they may be naturally employed for representing e.g. physical, biological, or financial phenomena. Specifically in the context of Computer Science, computational processes, machine learning algorithms, and multi-agent systems may be regarded as dynamical systems. This has sparked interest in designing formal specification languages for dynamical systems which could potentially be employed for automated or computer-assisted deduction, leading to the introduction of dynamic topological logic (DTL). When space is continuous but time is discrete, it is known that a sound and complete deductive calculus for DTL exists. However, discrete spaces are not uncommon in CS applications , and in this setting, whether such a calculus exists even in principle has been an open question for more than two decades. More precisely, it was unknown whether the DTL of Alexandrov spaces is computably enumerable. In this paper, we use model search techniques to provide an affirmative answer.

Cite As Get BibTex

Niels C. Vooijs and David Fernández-Duque. Axiomatizability of Alexandrov Dynamic Topological Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 81:1-81:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.81

Author Details

Niels C. Vooijs
  • Universität Bern, Switzerland
David Fernández-Duque
  • University of Barcelona, Spain

Funding

  • Vooijs, Niels C.: Supported by Swiss National Science Foundation (SNSF) grant No. 200021_215157.
  • Fernández-Duque, David: Supported by grants PID2023-149556NB-I00 and CEX2021-001169-M, funded by MICIU/AEI/10.13039/501100011033, as well as grant 2025 ICREA 00084, funded by the Generalitat de Catalunya.

Acknowledgements

We would like to thank the anonymous referees for their careful reading of our paper and the many suggestions which have improved the presentation of this paper.

References

  1. Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, and Brett McLean. Gödel-Dummett linear temporal logic. Artificial Intelligence, 338, 2025. URL: https://doi.org/10.1016/j.artint.2024.104236.
  2. Pavel Sergeyevich Alexandrov. Diskrete Räume. Recueil Mathématique. Nouvelle Série, 2:501-518, 1937. Google Scholar
  3. Sergei Nikolaevich Artemov, Jennifer M. Davoren, and Anil Nerode. Modal logics and topological semantics for hybrid systems. Technical Report MSI 97-05, Cornell University, 1997. Google Scholar
  4. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. Google Scholar
  5. Alexander Chagrov and Michael Zakharyaschev. Modal Logic, volume 35 of Oxford Logic Guides. Oxford University Press, 1997. Google Scholar
  6. Somayeh Chopoghloo and Morteza Moniri. An infinitary axiomatization of dynamic topological logic. Logic Journal of the IGPL, 30(1):124-142, 2022. URL: https://doi.org/10.1093/JIGPAL/JZAA055.
  7. A.G. Cohn and J. Renz. Qualitative spatial representation and reasoning. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, volume 3 of Foundations of Artificial Intelligence, pages 551-596. Elsevier, 2008. URL: https://doi.org/10.1016/S1574-6526(07)03013-1.
  8. William Craig. On axiomatizability within a system. The Journal of Symbolic Logic, 18(1):30-32, 1953. URL: https://doi.org/10.2307/2266324.
  9. Anuj Dawar and Martin Otto. Modal characterisation theorems over special classes of frames. Annals of Pure and Applied Logic, 161(1):1-42, 2009. URL: https://doi.org/10.1016/j.apal.2009.04.002.
  10. Ernst D. Dickmanns, B. D. Mysliwetz, and T. Christians. An integrated spatio-temporal approach to automatic visual guidance of autonomous vehicles. IEEE Transactions on Systems, Man, and Cybernetics, 20(6):1273-1284, 1990. URL: https://doi.org/10.1109/21.61200.
  11. Herbert Edelsbrunner and John Harer. Persistent homology - a survey. In Jacob Eli Goodman, János Pach, and Richard Pollack, editors, Surveys on Discrete and Computational Geometry: Twenty Years Later, volume 453 of Contemporary mathematics, pages 257-282. American Mathematical Society, 2008. Google Scholar
  12. Max J. Egenhofer and Robert D. Franzosa. Point-set topological spatial relations. International Journal of Geographical Information Systems, 5(2):161-174, 1991. URL: https://doi.org/10.1080/02693799108927841.
  13. David Fernández-Duque. Dynamic topological completeness for r^2. Logic Journal of the IGPL, 15(1):77-107, 2007. URL: https://doi.org/10.1093/JIGPAL/JZL036.
  14. David Fernández-Duque. Non-deterministic semantics for dynamic topological logic. Annals of Pure and Applied Logic, 157(2):110-121, 2009. Kurt Gödel Centenary Research Prize Fellowships. URL: https://doi.org/10.1016/j.apal.2008.09.015.
  15. David Fernández-Duque. Dynamic topological logic interpreted over minimal systems. Journal of Philosophical Logic, 40(6):767-804, 2011. URL: https://doi.org/10.1007/S10992-010-9160-4.
  16. David Fernández-Duque. Tangled modal logic for spatial reasoning. In Toby Walsh, editor, IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 857-862. IJCAI/AAAI, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-149.
  17. David Fernández-Duque. Dynamic topological logic of metric spaces. Journal of Symbolic Logic, 77(1):308-328, 2012. URL: https://doi.org/10.2178/JSL/1327068705.
  18. David Fernández-Duque. Non-finite axiomatizability of dynamic topological logic. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence Moss, editors, Advances in Modal Logic, volume 9, pages 200-216. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Fernandez-Duque.pdf.
  19. David Fernández-Duque. A sound and complete axiomatization for dynamic topological logic. The Journal of Symbolic Logic, 77(3):947-969, 2012. URL: https://doi.org/10.2178/jsl/1344862169.
  20. David Fernández-Duque. The intuitionistic temporal logic of dynamical systems. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:3)2018.
  21. David Fernández-Duque, Brett McLean, and Lukas Zenger. A sound and complete axiomatisation for intuitionistic linear temporal logic. In Pierre Marquis, Magdalena Ortiz, and Maurice Pagnucco, editors, Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, Hanoi, Vietnam. November 2-8, 2024, 2024. URL: https://doi.org/10.24963/KR.2024/33.
  22. Kit Fine. Logics containing K4. part II. The Journal of Symbolic Logic, 50(3), 1985. URL: https://doi.org/10.2307/2274318.
  23. David Gabelaia, Roman Kontchakov, Ágnes Kurucz, Frank Wolter, and Michael Zakharyaschev. Combining spatial and temporal logics: Expressiveness vs. complexity. Journal of Artificial Intelligence Research, 23:167-243, 2005. URL: https://doi.org/10.1613/jair.1537.
  24. David Gabelaia, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Non-primitive recursive decidability of products of modal logics with expanding domains. Annals of Pure and Applied Logic, 142(1-3):245-268, 2006. URL: https://doi.org/10.1016/j.apal.2006.01.001.
  25. Hua Hua, Dongxu Li, Ruiqi Li, Peng Zhang, Jochen Renz, and Anthony Cohn. Towards explainable action recognition by salient qualitative spatial object relation chains. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5):5710-5718, June 2022. URL: https://doi.org/10.1609/aaai.v36i5.20513.
  26. Boris Konev, Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev. Dynamic topological logics over spaces with continuous functions. In Guido Governatori, Ian Hodkinson, and Yde Venema, editors, Advances in Modal Logic, volume 6, pages 299-318. College Publications, 2006. URL: http://www.aiml.net/volumes/volume6/Konev-Kontchakov-Wolter-Zakharyaschev.ps.
  27. Boris Konev, Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev. On dynamic topological and metric logics. Studia Logica, 84(1):129-160, 2006. URL: https://doi.org/10.1007/s11225-006-9005-x.
  28. Philip Kremer and Grigori Mints. Dynamic topological logic. Annals of Pure and Applied Logic, 131(1):133-158, 2005. URL: https://doi.org/10.1016/j.apal.2004.06.004.
  29. Fred Kröger. First-Order Temporal Logic, pages 43-53. Springer Berlin Heidelberg, Berlin, Heidelberg, 1987. URL: https://doi.org/10.1007/978-3-642-71549-5_4.
  30. Joseph Bernard Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture. Transactions of the American Mathematical Society, 95(2):210-225, 1960. URL: https://doi.org/10.1090/s0002-9947-1960-0111704-1.
  31. John Charles Chenoweth McKinsey and Alfred Tarski. The algebra of topology. Annals of Mathematics, 45(1):141-191, 1944. URL: https://doi.org/10.2307/1969080.
  32. Colin Ashley Naturman. Interior Algebras and Topology. PhD thesis, University of Cape Town, 1990. URL: http://hdl.handle.net/11427/18244.
  33. Maria Nogin and Aleksey Nogin. On Dynamic Topological Logic of the Real Line. Journal of Logic and Computation, 18(6):1029-1045, August 2008. URL: https://doi.org/10.1093/logcom/exn034.
  34. D.A. Randell, Z. Cui, and A.G. Cohn. A spatial logic based on regions and connection. In Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning, KR'92, pages 165-176, San Francisco, CA, USA, 1992. Morgan Kaufmann Publishers Inc. Google Scholar
  35. Dana Scott. Continuous lattices. In Francis William Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97-136. Springer Berlin Heidelberg, 1972. URL: https://doi.org/10.1007/BFb0073967.
  36. Dana Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522-587, 1976. URL: https://doi.org/10.1137/0205037.
  37. Sergey Slavnov. On completeness of dynamic topological logic. Moscow Mathematical Journal, 5:477-492, 2005. Google Scholar
  38. John G. Stell. Qualitative spatial representation for the humanities. International Journal of Humanities and Arts Computing, 13(1-2):2-27, 2019. URL: https://doi.org/10.3366/ijhac.2019.0228.
  39. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Inf. Comput., 157(1-2):142-182, 2000. URL: https://doi.org/10.1006/INCO.1999.2836.
  40. Frank Wolter and Michael Zakharyaschev. Spatio-temporal representation and reasoning based on RCC-8. In Anthony G. Cohn, Fausto Giunchiglia, and Bart Selman, editors, KR 2000, Principles of Knowledge Representation and Reasoning Proceedings of the Seventh International Conference, Breckenridge, Colorado, USA, April 11-15, 2000, pages 3-14. Morgan Kaufmann, 2000. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact