Topic: Geometries and Models of Movement
Current participants:
Jean-François Condotta,
Vincent Dugat,
Luis Fariñas del Cerro,
Yannick Larvor
in collaboration with
Philippe Balbiani
from the University Paris-Nord
We study the mathematical models of space
(geometries) and the models of movement.
We concentrate on the definition of logical formalisms
and automated deduction methods allowing to
reason about space and movement.
Spatial relations between events appear in a huge number of human
activities such as describing an itinerary or playing chess.
They are the raison d'être of several domains of computer science,
e.g. the representation of geographical and topological knowledge,
plan generation, or natural language understanding.
In comparison with temporal logics,
their formalization in intensional
logics has not been developped at all up to now,
although the spatial modalities such as `somewhere' or `left of'
appear as often as temporal modalities.
It is our aim to develop such modal logics of space.
We have defined several logical systems whose models are well-known
geometries, such as affine or projective geometry.
(in collaboration with
Tinko Tinchev and Dimiter Vakarelov from the
Mathematical Logic
Department of Sofia University)
We have defined conditional rewriting systems for
a family of incidence and ordering geometries.
These systems allow to establish under which conditions two terms
(i.e. two figures) are equal.
The reduction relations of these systems are noetherian, decidable, and
confluent.
The results are of interest in the case of planar projective geometry
(which is equivalent to the algebraic theory of ternary rings).
Such an approach to algebraic reasoning is new, and indicates hope
for a solution to the problem of unification in the algebraic theory of
fields.
For that a rewriting system corresponding to projective geometry in space
must be defined.
In contrast with algebraic methods,
the ours allow for a better readability of proofs,
because to each deduction step we can associate a geometrical transformation.
Traditionally, movement is defined as a function associating
to each instant a point (position) in space.
In our approach we consider movement in a relational framework.
We define the primitive relations
(e.g. that a mobile is approaching another mobile),
and associate properties to these relations in a way such that
an isomorphism between the two approaches is obtained.
We have characterised such a type of relationship
for the case of mobiles moving at constant speed in euclidean space.
These models are a first step towards a qualitative definition
of movement.
A first application of our method concerns conflict management
in air traffic control.
In collaboration with
CENA
we have defined particular relations between aircraft trajectories.
last update: june 1998
Andreas.Herzig@irit.fr / http://www.irit.fr/~Andreas.Herzig