A spatio-temporal ontology for geographic information integration

Abstract

Abstract This paper presents an axiomatic formalization of a theory of top-level relations between three categories of entities: individuals, universals, and collections. We deal with a variety of relations between entities in these categories, including the sub-universal relation among universals and the parthood relation among individuals, as well as cross-categorial relations such as instantiation and membership. We show that an adequate understanding of the formal properties of such relations – in particular their behavior with respect to time – is critical for geographic information processing. The axiomatic theory is developed using Isabelle, a computational system for implementing logical formalisms. All proofs are computer verified and the computational representation of the theory is available online. Keywords: Geospatial ontologySpatio-temporal ontologyQualitative spatio-temporal reasoningInteroperabilityAxiomatic theories Acknowledgments Smith's work on this paper was funded in part by the National Institutes of Health through the NIH Roadmap for Medical Research, Grant 1 U 54 HG004028. Information on the National Centers for Biomedical Computing can be found at http://nihroadmap.nih.gov/bioinformatics. Notes 1. For discussions of perdurants (processes) and dependent endurants (qualities, roles, etc.), see Simons (Citation1987), Sider (Citation2001), Grenon and Smith (Citation2004), Bittner et al. (2004a), Galton and Worboys (Citation2005), Grenon and Smith (Citation2004), and Smith and Grenon (Citation2004). 2. Notice that parthood in this most general sense is transitive (Simons Citation1987; Varzi Citation1996). There are, however, more specific parthood relations, for example, part-of-the-same-scale (Bittner and Donnelly Citation2006) or functional-part-of, that are not transitive (Varzi Citation2006). 3. All theorems are computer verified. For details see Section 7. 4. Thus in contrast to Bittner et al. (2004b) we require here that collections have at least two members. For a more comprehensive version of this theory of collections, see Bittner and Donnelly (Citation2006). 5. We here ignore the fact that in Louisiana counties are called 'parishes' and in Alaska 'boroughs'. 6. As an example consider the universals socio-economic unit and human settlement. If we mix the classifications of socio-economic units and human settlements into a single classification structure, then the resulting structure will not be a tree, since neither socio-economic unit is a sub-universal of human settlement nor vice versa, though both have the universal city as a (proper) sub-universal. 7. Those who insist that the hierarchical structure imposed by the sub-universal relation is indeed a lattice can fall back to the version of the theory presented in Bittner et al. (2004b). In that theory lattice structures are permitted as long as what we call the no-partial-overlap principle (NPO) is not added to the theory. 8. TU0 seems to be violated in classification systems in which universals with a single sub-universal are postulated. Sorokine and Bittner (Citation2005) investigated this phenomenon in the context of ecoregion classifications and showed that in classification systems that violate TU0 either the sub-universal relation is confused with the instantiation relation, or universals that do not have instances in a given spatial location are neglected. 9. Note that we here do not add an axiom requiring that two universals that have the same instances at all times are identical. Thus, in contrast to Bittner et al. (2004b), we leave open the possibility that two distinct universals may have exactly the same instances at all times. In a modal framework one usually demands that two universals are identical if and only if they have the same instances at all times and in all possible worlds (Oliver Citation1996).