Spatial Temporal Logic In Many-sorted Logic

'Space and time'means space, time and the combination of the two in broad sense; while, narrowly speaking, it is only the combination of space and time. 'Spatio-temporal reasoning'contains not only the theorem in domain of space and time, but includes researches in representation and model construction as well. There have been two separate methods on the way of Spatio-temporal reasoning. 'Temporal reasoning'originates from temporal logic in the end of nineteen fifties, and becomes one of the most active fields in the nineteen eighties. There are still many studies devoted to this area today. As for space, the model and theorem goes back to the very beginning of the birth of artificial intelligence. Ever since eighteen nineties, developments have been made in this field, and now spatial theorem is still one of the main areas in artificial intelligence. Researches on space or time separately have been made fairly abundant, how to combine the two has become key problem in space and time theorem research. There are mainly two types of research nowadays: logic method and algebra method. What we did in our research is mainly from the former, to propose a new system of representation and reasoning about space and time. In the year of 1993, K. Meinke and J. V. Tucher proposed the idea of domain classification in their works 'Many-sorted Logic and its Applications'. And the idea of many-sorted makes the discussion of objects in different granularity possible, such as to represent points, lines, surface (even body) and time meanwhile. Considering the shortage of classical RCC theory in representing point and line, and the disability for traditional reasoning system to combine time...