| Reasoning about spatial knowledge is an important aspect of computational intelligence. Humans easily switch between high-level and low-level spatial knowledge, while computers have traditionally relied only on low-level spatial information. Qualitative spatial representation and reasoning is concerned with devising high-level, qualitative, representations of certain aspects of space using small sets of intuitive spatial relations that lend themselves to efficient reasoning. Many such representations have been developed over the years, but their use in practical applications seems to be inhibited.;One reason preventing more widespread adoption of qualitative spatial representations may be the gap between simple but inexpressive qualitative representations at one end and geometric or quantitative representations with the expressivity of Euclidean geometry at the other end. Another factor may be the lack of semantic integration between the various spatial representations ranging from qualitative to geometric ontologies. We will address both issues in this thesis with a focus on spatial ontologies that involve some kind of mereotopological relations such as contact and parthood.;We design a family of spatial ontologies with varying restrictiveness and increasingly more expressive nonlogical languages, organized into hierarchies of ontologies of equal expressivity. As the most foundational spatial ontology we propose a multidimensional mereotopology based only on 'containment' and 'relative dimension' as undefined concepts. By adding either 'boundary containment' or 'betweenness' as new concepts, we further extend the expressivity without impairing the qualitative character.;Tools from mathematical logic, such as interpretability and definability, are used to semantically integrate other spatial ontologies into our hierarchies. Moreover, we show how mereotopological theories, incidence geometries, and ordered incidence geometries are formally related to our theories. We thereby better understand differences in expressivity, restrictiveness, and ontological assumptions between a broad range of spatial ontologies. Throughout the thesis, we utilize automated theorem provers to assist with the verification of all ontologies by constructing nontrivial models and by proving key properties about the axiomatized relations and functions. Theorem provers are also utilized to obtain some of the integration results. |
