Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-26T05:46:22.071Z Has data issue: false hasContentIssue false

A logic for metric and topology

Published online by Cambridge University Press:  12 March 2014

Frank Wolter
Affiliation:
Department of Computer Science, University of Liverpool, Liverpool L69 7ZF, UKE-mail:, [email protected] URL: http://www.csc.liv.ac.uk/~frank
Michael Zakharyaschev
Affiliation:
Department of Computer Science, King's College London, Strand, London WC2R 2LS, UKE-mail:, [email protected] URL: http://www.dcs.kcl.ac.uk/staff/mz

Abstract

We propose a logic for reasoning about metric spaces with the induced topologies. It combines the ‘qualitative’ interior and closure operators with ‘quantitative’ operators ‘somewhere in the sphere of radius r’ including or excluding the boundary. We supply the logic with both the intended metric space semantics and a natural relational semantics, and show that the latter (i) provides finite partial representations of (in general) infinite metric models and (ii) reduces the standard ‘ε-definitions’ of closure and interior to simple constraints on relations. These features of the relational semantics suggest a finite axiomatisation of the logic and provide means to prove its EXPTIME-completeness (even if the rational numerical parameters are coded in binary). An extension with metric variables satisfying linear rational (in)equalities is proved to be decidable as well. Our logic can be regarded as a ‘well-behaved’ common denominator of logical systems constructed in temporal, spatial, and similarity-based quantitative and qualitative representation and reasoning. Interpreted on the real line (with its Euclidean metric), it is a natural fragment of decidable temporal logics for specification and verification of real-time systems. On the real plane, it is closely related to quantitative and qualitative formalisms for spatial representation and reasoning, but this time the logic becomes undecidable.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Aiello, M., van Benthem, J., and Bezhanishvili, G., Reasoning about space: the modal way, Journal of Logic and Computation, vol. 6 (2003), pp. 889920.CrossRefGoogle Scholar
[2]Alexandroff, P. S., Diskrete Räume, Matematicheskii Sbornlk, vol. 2 (44) (1937), pp. 501518.Google Scholar
[3]Alur, R., Feder, T., and Henzinger, T., The benefits of relaxing punctuality, Journal of the ACM, vol. 43 (1996), pp. 116146.CrossRefGoogle Scholar
[4]Alur, R. and Henzinger, T.A., A really temporal logic, Journal of the ACM, vol. 41 (1994), pp. 181204.CrossRefGoogle Scholar
[5]Areces, C., Blackburn, P., and Marx, M., The computational complexity of hybrid temporal logics, Logic Journal of the IGPL, vol. 8 (2000), pp. 653679.CrossRefGoogle Scholar
[6]Artemov, S., Davoren, J., and Nerode, A., Modal logics and topological semantics for hybrid systems, Technical Report MSI 97-05, Cornell University, 1997.Google Scholar
[7]Bennett, B., Modal logics for qualitative spatial reasoning, Logic Journal of the IGPL, vol. 4 (1996), pp. 2345.CrossRefGoogle Scholar
[8]Bezhanishvili, G. and Gehrke, M., A new proof of completeness of S4 with respect to the real line, 2002, Preprint PP-2002-06 of ILLC, University of Amsterdam.Google Scholar
[9]Blackburn, P., de Rijke, M., and Venema, Y., Modal logic, Cambridge University Press, 2001.CrossRefGoogle Scholar
[10]Börger, E., Grädel, E., and Gurevich, Yu., The classical decision problem, Perspectives in Mathematical Logic, Springer, 1997.CrossRefGoogle Scholar
[11]Bourbaki, N., General topology, part 1, Hermann, Paris and Addison-Wesley, 1966.Google Scholar
[12]Chagrov, A. and Zakharyaschev, M., Modal logic, Oxford Logic Guides, vol. 35, Clarendon Press, Oxford, 1997.CrossRefGoogle Scholar
[13]Clote, P. and Backofen, R., Computational molecular biology, John Wiley & Sons, 2000.Google Scholar
[14]Cohn, A. and Hazarika, S., Qualitative spatial representation and reasoning: an overview, Fundamenta Informaticae, vol. 46 (2001), pp. 129.Google Scholar
[15]Dubois, D., Prade, H., Esteva, F., Garcia, P., and Godo, L., A logical approach to interpolation based on similarity relations, International Journal of Approximate Reasoning, vol. 17 (1997), pp. 136.CrossRefGoogle Scholar
[16]Egenhofer, M. and Franzosa, R., Point-set topological spatial relations, International Journal of Geographical Information Systems, vol. 5 (1991), pp. 161174.CrossRefGoogle Scholar
[17]Esteva, F., Garcia, P., Godo, L., and Rodriguez, R., A modal account of similarity-based reasoning, International Journal of Approximate Reasoning, vol. 16 (1997), pp. 235260.CrossRefGoogle Scholar
[18]Gärdenfors, P., Conceptual spaces, The MIT Press, 2000.CrossRefGoogle Scholar
[19]Gärdenfors, P. and Williams, M. A., Reasoning about categories in conceptual spaces, Proceedings of the 7th international joint conference on artificial intelligence (IJCAI), Morgan Kaufmann, 2001, pp. 385392.Google Scholar
[20]Goldblatt, R., Mathematics of modality, CSLI Lecture Notes, no. 43, CSLI Publications, Stanford, 1993.Google Scholar
[21]Grigni, M., Papadias, D., and Papadimitriou, Ch., Topological inference, Proceedings of the 14th international joint conference on artificial intelligence (IJCAI), Morgan Kaufmann, 1995, pp. 901906.Google Scholar
[22]Harel, D., Kozen, D., and Tiuryn, J., Dynamic logic, MIT Press, 2000.CrossRefGoogle Scholar
[23]Hirshfeld, Y. and Rabinovich, A., Quantitative temporal logic, Proceedings of computer science logic 1999, Springer, 1999, pp. 172187.Google Scholar
[24]Huttenlocher, D., Klanderman, G., and Rucklidge, W., Comparing images using the Hausdorff distance, IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 15 (1993), pp. 850863.CrossRefGoogle Scholar
[25]Kremer, P., Mints, G., and Rybakov, V., Axiomatizing the next-interior fragment of dynamic topological logic, The Bulletin of Symbolic Logic, vol. 3 (1997), pp. 376377.Google Scholar
[26]Kutz, O., Sturm, H., Suzuki, N.-Y., Wolter, F., and Zakharyaschev, M., Logics of metric spaces, ACM Transactions on Computational Logic, vol. 4 (2003), pp. 260294.CrossRefGoogle Scholar
[27]Ladner, R., The computational complexity of provability in systems of modal logic, SIAM Journal on Computing, vol. 6 (1977), pp. 467480.CrossRefGoogle Scholar
[28]Lutz, C., Wolter, F., and Zakharyaschev, M., A tableau algorithm for reasoning about concepts and similarity, Automated reasoning with analytic tableaux and related methods (Mayer, M. C. and Pirri, F., editors), LNCS, vol. 2796, Springer, 2003.CrossRefGoogle Scholar
[29]McKinsey, J.C.C. and Tarski, A., The algebra of topology, Annals of Mathematics, vol. 45 (1944), pp. 141191.CrossRefGoogle Scholar
[30]Mints, G., A completeness proof for propositional S4 in Cantor space, Logic at work (Orlowska, E., editor), Springer, 1999, pp. 7988.Google Scholar
[31]Renz, J. and Nebel, B., On the complexity of qualitative spatial reasoning, Artificial Intelligence, vol. 108 (1999), pp. 69123.CrossRefGoogle Scholar
[32]Shehtman, V., “Everywhere” and “Here”, Journal of Applied Non-classical logic, vol. 9 (1999), pp. 369379.CrossRefGoogle Scholar
[33]Spaan, E., Complexity of modal logics, Ph.D. thesis, Department of Mathematics and Computer Science, University of Amsterdam, 1993.Google Scholar
[34]Tarski, A., Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae, vol. 31 (1938), pp. 103134.CrossRefGoogle Scholar
[35]Wolter, F. and Zakharyaschev, M., Reasoning about distances, Proceedings of the 18th international joint conference on artificial intelligence (IJCAI), Morgan Kaufmann, 2003, pp. 12751280.Google Scholar
[36]Worboys, M., GIS: A computational perspective, Taylor & Francis, 1995.Google Scholar