It is argued that rigorous formal theories are a necessity if proper use is to be made of computers' ability to store and manipulate spatial and spatiotemporal information. A qualitative spatial calculus constructed within rst-order logic is described. This calculus treats extended regions rather than points as fundamental, and is based on primitive concepts of`connection' between regions, and of convexity. A sorted logic, and subsumption lattices of spatial relations and of spatial and temporal entities, are used to implement the calculus. Inference mechanisms used to reason about both static and dynamic sets of relations between regions are described, and the notion of`conceptual neighbourhoods' within sets of relations is explored. We discuss an example drawn from the domain of biology, and suggest possible applications within geography and related areas. The paper concludes with a description of current and projected work based on our qualitative spatial calculus.