A spatio-temporal ontology for geographic information integration

Bittner, T., Donnelly, M. & Smith, B. Journal for Geographical Information Science. 2009: 23 (6), 765-798.

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.