Workshop on

Reasoning about Space

Abstracts

North American Summer School in Logic, Language and Information

June 17-21, 2003
Bloomington, Indiana (USA)


Abstracts
G. Mints,T. Zhang
Propositional logic of continuous transformations

Dynamical topological logic studies models of the form (X,T), where is a topological space, T a transformation on X. Propositional formulas are constructed from variables (atomic formulas) by Boolean connectives, necessity \Box and a monadic operation o. Variables are interpreted by subset of X, Boolean connectives act in a natural way, \Box is the interior and o is the pre-image under operation T. Under this interpretation the axiom schema o\Box A->\Box oA called (C) expresses continuity of T. J. Davoren proved completeness of S4+C for arbitrary topological spaces, in particular for finite spaces derived from Kripke models. We prove completeness of S4+C for Cantor space. The proof uses a continuous and open map W from the Cantor space onto a suitable Kripke model (K,T) [with T continuous in order topology on K] and a continuous map S on Cantor space satisfying condition: WS=TW. P. Kremer pointed out that the real line is not complete for S4+C. A counterexample constructed by J. van Benthem will probably be presented at NASSLI.



Ian Pratt-Hartmann
Where Spatial Reasoning is (or should be) going

For most of the previous century, a small but tenacious band of authors argued that a parsimonious and conceptually elegant treatment of space can be obtained by taking the position that regions, not points, are the primitive spatial entities. These arguments resulted in the development of various calculi for qualitative spatial reasoning in which regions are taken as primary, an enterprise which we might reasonably call `mereogeometry'.

In the past decade, the Computer Science community in particular has produced a plethora of new technical results in mereogeometry, especially concerning the decidability and computational complexity of region-based geometrical representation languages. Unfortunately, this work has often lacked a coordinating sense of direction; and what has emerged is not so much a unified discipline as a motley of formal systems which are difficult to compare and to evaluate. Yet buried in the confusion lies much that is of value. The aim of this talk is to provide enough of an overview to assess where the field is (or perhaps, should be) going, and to identify its immediate future challenges.



Dave Randell
Occlusion Calculi: A Cognitive Robotics Perspective

This talk motivates and describes two first-order axiomatic theories originally developed to model viewpoint dependent (spatial) occlusion relations between arbitrary shaped bodies. Both calculi respectively assume a region-based ontology and embed the spatial theories: RCC-5 and RCC-8. The ontology and set of defined relations is sufficient for modelling domains where changing, but discrete, modes of overlap between images of objects coincide with changing lines of sight. When applied to mobile robots with machine vision, occlusion calculi can be used to model and assist reasoning about such tasks as: robot location, scene interpretation, navigation and route-planning, and general map-building. The talk concludes by highlighting the challenges faced when implementing such spatial logics on real world robots; and raises the interesting question of what, if anything, can Cognitive Robotics tell us about Spatial Reasoning?



Darko Sarenac
Modal Logics for Products of Topologies
Joint work with Johan van Benthem and Guram Bezhanishvili

Arguably the most basic logic for spatial reasoning is S4 interpreted over topological spaces. Our primary goal in this paper is to study a minimal augmentation of this logic. We will study multimodal languages of products of topologies where the modality of each component of the product is preserved into the product. This work generalizes some of the results of D.M. Gabbay and V.B. Shehtman on products of modal logics to the topological setting. Thus in the most general case, each component modality will have S4 as a complete axiomatization. The interesting question, of course, is how the modalities of various dimensions interact. The expansion of the language enables us to `track dimensions' in the product and this in turn will add some expressive power to the language.



Chris Steinsvold
Towards A Topology Of Knowledge And Belief

KD45 is often taken as a logic of justified belief. Interpreting the diamond of KD45 as the derived set operator (AKA set of limit points), a topological completeness result is available. Thus, the dual of the derived set operator acts like justified belief (given certain restrictions on the space). Also, if we take the interior operator to represent knowledge, we get a philosophically defensible logic of knowledge and belief. We'll discuss the possibility of using the topological semantics as an alternative semantics for a reasoner.